raaz-crypto/verse-coq

Speeding up code generation

Closed this issue · 1 comments

piyush-kurur commented

The generation of code is slow. While this is not a problem yet, it can hinder fast compile and build cycle.

  • Improve the ocaml data structures used so that the extracted code runs fast. See #82
  • Separate out the proofs and tests.
  • Add a continuous building when developing.
piyush-kurur commented

Irrelevant now that we are using the Coq's notation system for code generation see pull request #112