Simplify Makefiles after F* changes

[mtzguido]

Mostly:

1. For extracting, we can just pass the path of the checked file to
   F* instead of doing the hacky substitution and rely on F* to find the
   source module.
2. no need to pass --extract when we want to extract a single file
   (except for --codegen krml, separate PR incoming for that).
3. Using -o instead of (the now deprecated) --output_deps_to and
   --krmloutput.
4. Using -c instead of --cache_checked_modules, and only passing it
   when we are actually trying to create a checked file.

Also added some explicit -o flags to make sure F* writes to the desired
target.

(Previous text:

Mostly no need to pass --extract when we want to extract a single file, and we can just pass the path of the checked file to F* instead of doing the substitution.

Also added some explicit --krmloutput flags to make sure F* writes to the desired target.)

[mtzguido]

Wondering if
1- We should just add -o option that subsumes --krmloutput and --output_deps_to, and could even be used for the location of the generated checked file.
2- Is the default behavior for krml (extracting all modules) desirable, or should we make it just extract the module given in the command line, and possibly override with --extract *? This would remove the remaining $(subst..) calls.

[msprotz]

1- yeah I was just about to suggest the same thing it's weird to have specific options for specific purposes -- most tools use -o regardless of the type of file produced (e.g. gcc -E, gcc -MD, gcc -c, gcc -shared, produce .c, .d, .o, .so but all are controlled by -o)
2- it's historical, and makes it easy to have krml invoke F* to produce a single out.krml file, but it's really bad because there are differences in behavior, and the mode where F* processes multiple files all at once is not really supported anymore -- I'd be in favor of getting rid of it, but then krml would have to output build stubs and defer extraction and compilation to make, which I'm 100% happy about, it's just a fair amount of implementation work

[mtzguido]

For 2) yes I don't think we're testing the multi-file invocations... not sure if they work reliably. But not sure I understand what you mean about the stubs, can't krml just pass --extract * when invoking F* to retain the current behavior?

[msprotz]

I guess? Like krml would invoke F* with fstar --extract '*' MyFile.fst -o out.krml? I think the WASM backend needs WasmSupport.fst passed to F* too, and perhaps even FStar.UInt128 passed to F* too -- I don't remember. I don't really use this mode either.

[mtzguido]

Yeah exactly, that should make F* behave just as it does now. I'll give it a go and update here, it'd be nice to make this consistent.

[mtzguido]

Updated after implementing -o in F*. For changing the behavior of krml extraction, I'll post a separate PR since I expect I may need to go through many projects to get it to work, this bit was backwards-compatible.

[msprotz]

why does this one need extract_module but not the one above?

[mtzguido]

--codegen krml still has the default extracting everything (instead of just the module in cmdline). I'll change that soon in a separate PR as it'd be a breaking change for many projects (I think)

[msprotz]

ok sounds good -- uniformity is great

[msprotz]

Looks good to me minus my comments. Thanks for this!

[msprotz]

then should this extract_module go? (per your comment)

[mtzguido]

Indeed, updated.