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

[markulf]

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

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:

[fournet]

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]

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.