Generate single binary for all synthesis
JasonGross opened this issue · 0 comments
JasonGross commented
It would be nice to be able to call something like synthesize word-by-word-montgomery args
or fiat-cryptography word-by-word-montgomery args
or whatever, instead of having separate binaries for each synthesis pipeline. To do this, I think we should add another module below
Lines 1333 to 1339 in dcd5678
that contains a
main
function that reads argv
into prog::kind::args
, checks to see if kind
is one of the recognized kinds and delegates to the relevant main method if so, and otherwise printing out USAGE: $0 <possible options>
. Presumably we can reuse the infrastructure for parsing output languages to parse the possible kinds. parse_argv
might need to be generalized to take an implicit argument of how many arguments to ignore for the program name, or else we'll have to adjust the quoting at https://github.com/mit-plv/fiat-crypto/blob/dcd567854191ad4e1abd293ddecd2a8df1048d8d/src/CLI.v#L1015C19-L1015C19
We can then replace
fiat-crypto/src/StandaloneHaskellMain.v
Lines 104 to 114 in dcd5678
and
fiat-crypto/src/StandaloneOCamlMain.v
Lines 196 to 203 in dcd5678
with a single main function (for #1720 we'll probably want first a function that specializes to all of the language-specific calls, and then finally something that passes in
Sys.argv
? Or we can just have a separate StandaloneJSofOCaml
that implements all the language-specific stuff separately?).