search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

Basic support for build with dune. #81

Closed kape1395 closed 1 year ago

kape1395 commented 1 year ago

Closes https://github.com/tlaplus/tlapm/issues/80

This build is useful at least to have the vscode IDE working for the tlapm codebase.

Additionally, for some reason, the dune build was failing on src/backend/fpfile.ml while make build passed. Looking at the code, it seems to me like the mistake actually exists. The fixed version compiles with the make build as well. Would be glad if someone would take a look at this and explain, why the original build was not failing.

damiendoligez commented 1 year ago

Additionally, for some reason, the dune build was failing on src/backend/fpfile.ml while make build passed.

This is because dune adds the -strict-sequence compiler flag. Without it, the function iter_file is too polymorphic, and the bug doesn't trigger a type error. Instead, the function translate does nothing, which means that fingerprints are not loaded. (I think)