CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
947 stars 83 forks source link

Use a file-based I/O interface to the compiler #355

Open xrchz opened 6 years ago

xrchz commented 6 years ago

Make the top-level interface to the compiler accept the names of input file(s) on the command line, including a way to specify stdin, and an optional output file instead of stdout. (See comment in #319.) Probably depends on #248 and #354.

xrchz commented 6 years ago

Amongst other things, the .file directive in our .S file template should reflect the actual name of the output file.

oskarabrahamsson commented 1 year ago

The most annoying issue is that command-line arguments are dealt with in two places:

I suggest moving all options parsing to the main function in compiler64ProgScript.sml, remove the command-line and file-system model arguments from compile_{32,64} and pass the compiler configuration records created from options parsing instead.

Alternatively, one can:

Finally, I don't think #248 is required anymore: it's probably easier to extend the existing ad-hoc options parsing code.