search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
367 stars 79 forks source link

Resurrect the cofix transform, adding a new axiom for the admitted pr… #1056

Closed mattam82 closed 6 months ago

mattam82 commented 6 months ago

…oofs.

Generalize MetaCoq Erase to take options allowing to optionally run this pass, a la CertiCoq. This gives the following options:

Usage:
To erase a Gallina definition named <gid> type:
MetaCoq Erase <options> <gid>.

To show this help message type:
MetaCoq Erase -help.

Valid options:
-typed     :  Run the typed erasure pipeline including a dearging phase. By default we run the pipeline without this phase.
-unsafe      :  Run also partially verified passes of the pipeline. This includes the cofix to fix translation.
-time        :  Time each compilation phase
-bypass-qeds :  Bypass the use of Qed and quote opaque proofs. Beware, this can result in large memory
consumption due to reification of large proof terms.
By default, we use the (trusted) Template-Coq quoting optimization that quotes every opaque term as an axiom.
All these axioms should live in Prop so that erasure is not affected by the absence of their bodies.
-fast        : Enables an alternative implementation of the parameter stripping phase that uses accumulators
instead of a view (see Erasure.ERemoveParams).

See https://metacoq.github.io for more detailed information.