helix
helix copied to clipboard
vzaliva
Formally verified operator language and rewriting engine for high-performance computing
If -j not specified, make defaults to 4. However this flag is not passed further down build chain and it looks like everything is compiled without paralleleization.
Makefile `test` goal is intended to success even if some proofs (non-executable code) fails. Specifically `ReifyProofs.v` and `Correctness.v`. However, it does not properly track dependencies and sometimes fails, for example,...
We instantiate FMap with natural numbers as a key several time: ``` $ ag FMapAVL.Make 12:41:16 ml/extracted/Memory.ml 438: module IM = FMapAVL.Make(Z_as_OT) coq/SigmaHCOL/SigmaHCOLRewriting.v 41:Module NM := FMapAVL.Make(Nat_as_OT). coq/DSigmaHCOL/TypeSig.v 45:Module TM...