search

FStarLang / fstar-interactive

An F* interactive mode for the atom editor
MIT License
7 stars 4 forks source link

atom-fstar-build.json needs --verify_module <Module checked> flag. #10

Open markulf opened 9 years ago

markulf commented 9 years ago

Contrary to what one would expect, the --verify_module flag needs to be manually set in atom-fstar-build.json, to verify individual files. image

Otherwise, verification is slow, and for miTLS reports way too many errors.

Moreover, if there is in addition a dangling space at the end of the JSON string, the following error is thrown: image

fournet commented 9 years ago

Can someone explain or document the json config files, and in particular how the file-local config is merged with the project config? We are getting too many conflict due to check ins of ad hoc atom-fstar-build.json files.

fournet commented 9 years ago

As mentioned by Markulf, I miss an automated --verify_module on the interactive module; editing the atom-fstar-build.json causes conflicts.

Note also that file-local (--build-config ... ) entirely override the build file; it is usually a bad idea to mix the two. Instead, use # pragmas.