search

FStarLang / FStar

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

Extraction does not write .checked, this is a performance issue #3490

Closed briangmilnes closed 1 month ago

briangmilnes commented 2 months ago

I updated Forge (makefiles) to know that if it is going to do an extraction to OCaml or FSharp that it does not need to run the validation phase. This can be a significant developer time saver. Although I have a method, make prove, that puts expensive proofs in a separate phase (thank you Jonathon), you still don't want to run validation twice if it can be avoided.

But --codegen Ocaml with a cache dir complains about missing .checked files, claims to be creating them but is not.

1) Is it really the case that full validation is occuring in codegen? 2) If so then why is it not writing .checked files and should it?

briangmilnes commented 1 month ago

As per Nik today: validation is to be performed first to ensure that all dependent modules have been validated and the .checked file is used in the generation of extracted code.