FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Add a --krmloutput option to chose filename for krml extraction #3371

Closed mtzguido closed 3 months ago

mtzguido commented 3 months ago

Currently, when F* is extracting a file into krml, it will choose a filename based on the module name (e.g. A.B.C.fst -> A_B_C.krml), or, if there are several modules, just use out.krml. This heuristic makes some sense, but can be confusing and hard to work with especially when writing makefiles.

This PR adds a --krmloutput option to explicitly choose the output filename. The path will not be tweaked at all (no prepending odir, no adding .krml extension).

Wondering if @msprotz thinks this is sensible.

msprotz commented 3 months ago

Overall, this is a good idea, except that for historical reasons, krml assumes that the filename determines the name of the module, so krml assumes that A_B_C.krml corresponds to A.B.C (module name).

So you'd have to change a few things, or be willing to live with that fact.

Generally, this is a desirable change, as this mapping breaks if the original module name contains an _ -- A.B_C.fst extracts to A_B_C.krml which is then understood to be A.B.C.

mtzguido commented 3 months ago

Indeed, that's another quirk I noticed recently but I was fine with avoiding underscores in my F* sources. I don't think it's too bad...

But, does the filename really make a difference? If I rename a .krml file to anything (keeping the extension) it does extract to the correct module name, which seems to be recorded in the file (by Extraction.Krml.translate_module).

Breaking the mapping is still somewhat of a concern, in my case I want to extract everything under a namespace A.B into a single file, so I need to pass --bundle "A.B=A.B.*", and in the makefile I need to reconstruct A.B from A_B. Arguably more of a problem about makefiles...

mtzguido commented 3 months ago

I'll merge this.. please let me know if you'd like this tweaked somehow.