MetaCoq 1.3.4 for Rocq 9.0

MetaCoq 1.3.4 for Rocq 9.0 (including rc1).

What's Changed

• Remove unused Require Even (Even has been removed from stdlib in 8.19) by @SkySkimmer in #1041
• Update main by @mattam82 in #1044
• Main fixes deprecations by @mattam82 in #1049
• Adapt to coq/coq#18590 by @proux01 in #1055
• Adapt to Coq PR#18397: Declare.declare_variable now takes a "variable_declaration" by @herbelin in #1029
• Adapt to coq/coq#18038 (rewrite rules) by @yannl35133 in #1060
• Adapt to coq/coq#18224 by @proux01 in #1035
• Adapt to coq/coq#18422 (indirect accessor handled through vernactypes) by @SkySkimmer in #1074
• Adapt to coq/coq#18852 (interp_red_expr can be done without ltac) by @SkySkimmer in #1071
• Adapt w.r.t. coq/coq#18910. by @ppedrot in #1076
• Adapt w.r.t. coq/coq#18909. by @ppedrot in #1077
• Adapt to coq PR #18921 fixing bugs of the inference of the return clause for Program-style pattern-matching by @herbelin in #1078
• Adapt to coq/coq#18867 (inductive_sort_family doesn't exist) by @SkySkimmer in #1073
• Adapt to coq/coq#18938 (EConstr.ERelevance) by @SkySkimmer in #1080
• Fixes for funelim by @mattam82 in #1085
• Adapt to Coq PR #18795 (more uniform API for declare.ml) by @herbelin in #1083
• Remove useless calls to Eval vm_compute. by @silene in #1079
• faster PCUICSR by @mrhaandi in #1081
• Adapt to coq/coq#18973. by @rlepigre in #1088
• Remove generated files from archive and ignore them now by @mattam82 in #1092
• Adapt to coq/coq#19384 (add_global_univ -> add_forgotten_univ) by @SkySkimmer in #1096
• Typecheck the result of term unquotation. by @ppedrot in #1098
• Adapt to coq/coq#19310 by @proux01 in #1093
• Correcting the definition of noccur_between in Template – main branch by @MevenBertrand in #1087
• Adapt to coq/coq#19620 (Global.push_context_set no strict argument) by @SkySkimmer in #1104
• Fix quoting and unquoting of primitive strings by @MathisBD in #1109
• Fix quoting and unquoting of primitive strings (#1109) for 8.20 by @yforster in #1110
• Mention 8.20 in DOC.md and INSTALL.md by @yforster in #1121
• metaprogramming library (8.20 version) by @MathisBD in #1122
• Remove bugged option MetaCoq Template Monad Debug. by @SkySkimmer in #1123
• Remove bugged option MetaCoq Template Monad Debug. by @MathisBD in #1126
• Adapt to coq/coq#19530 by @proux01 in #1102
• Update documentation in common/Environment.ml for inductive and constant declarations by @MathisBD in #1128
• Update documentation in common/Environment.ml for inductive and constant declarations by @MathisBD in #1131
• Adapt to coq/coq#19981 (Set Warnings is synterp phase) by @SkySkimmer in #1132
• Adapt w.r.t. coq/coq#19995. by @ppedrot in #1133
• Adapt w.r.t. coq/coq#20060. by @ppedrot in #1134
• Adapt to coq/coq#20095 (record.ml API changes) by @SkySkimmer in #1135
• Adapt to coq/coq#20069 (set_leq_sort doesn't need an env) by @SkySkimmer in #1136
• Adapt to coq/coq#20102 (template poly api change) by @SkySkimmer in #1137
• Merge 8.19 into 8.20 by @yforster in #1138
• Rocq renaming by @mattam82 in #1139

New Contributors

• @silene made their first contribution in #1079
• @rlepigre made their first contribution in #1088
• @MathisBD made their first contribution in #1109

Full Changelog: v1.3.3-8.19...v1.3.4-9.0

MetaCoq 1.3.4 for Coq 8.20

This release subsumes MetaCoq 1.3.3 for Coq 8.19. It fixes some bugs and provides a rudimentary meta-programming library.

What's Changed

• Fix quoting and unquoting of primitive strings (#1109) for 8.20 by @yforster in #1110
• metaprogramming library (8.20 version) by @MathisBD in #1122
• Remove bugged option MetaCoq Template Monad Debug. by @MathisBD in #1126
• Update documentation in common/Environment.ml for inductive and constant declarations by @MathisBD in #1131

Full Changelog: v1.3.2-8.20...v1.3.4-8.20

MetaCoq 1.3.3 for Coq 8.19

Bugfix release.

What's Changed

• Point 'index' in CoqDocJS header to index.html by @SwampertX in #1094
• Correct noccur for Template by @MevenBertrand in #1086
• Fix substitution during eta expansion of partial application by @4ever2 in #1117

New Contributors

• @SwampertX made their first contribution in #1094

Full Changelog: v1.3.2-8.19...v1.3.3-8.19

MetaCoq 1.3.2 for Coq 8.20

Release 1.3.2 of the MetaCoq project for Coq 8.20 is available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations, and the release notes for 1.3.1 for a summary of the changes w.r.t. previous versions.

The main changes in this new version w.r.t. v1.3.1 are:

What's Changed

• Proof that reordering of constructors is correct by @mattam82 in #1095
  This allows in particular to switch the representation of Coq booleans so that extracted code matches the ocaml representation of booleans, making interoperability with existing OCaml code easier.

• Add the force (lazy t) evaluation rule to LambdaBox by @mattam82 in #1089
  We verify that the evaluation rule is preserved by the verified transformations. In particular, this allows the coq-verified-extraction package and certicoq to support coinductive types and cofixpoints by interpreting lazy/force. The verification of the translation from cofixpoints to fixpoints + lazy/force is however still a work in progress.

Full Changelog: v1.3.1-8.19...v1.3.2-8.19

MetaCoq 1.3.2 for Coq 8.19

Release 1.3.2 of the MetaCoq project for Coq 8.19 is available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations, and the release notes for 1.3.1 for a summary of the changes w.r.t. previous versions.

The main changes in this new version w.r.t. v1.3.1 are:

What's Changed

• Proof that reordering of constructors is correct by @mattam82 in #1095
  This allows in particular to switch the representation of Coq booleans so that extracted code matches the ocaml representation of booleans, making interoperability with existing OCaml code easier.

• Add the force (lazy t) evaluation rule to LambdaBox by @mattam82 in #1089
  We verify that the evaluation rule is preserved by the verified transformations. In particular, this allows the coq-verified-extraction package and certicoq to support coinductive types and cofixpoints by interpreting lazy/force. The verification of the translation from cofixpoints to fixpoints + lazy/force is however still a work in progress.

Full Changelog: v1.3.1-8.19...v1.3.2-8.19

MetaCoq 1.3.1 for Coq 8.19

We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.19, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.

The main changes in this new version w.r.t. v1.2.1 are:

• A full integration of the typed erasure phase from the ConCert project in the erasure pipeline, with a complete correctness proof, by @mattam82. Use option MetaCoq Erase -typed to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v)
• Generalizations of the correctness and simulation lemmas by @yforster @mattam82 and @tabareau, showing in particular that erasure of applications of functions from firstorder types to firstorder types is compiled to applications, justifying separate compilation of functions and their arguments.
• Using standardization and canonicity, we also show that erased values of programs of firstorder inductive types (non-erasable inductives types for which all constructor argument types are themselves firstorder) are in direct correspondence with their Coq counterparts, allowing sound readback of these values. In other words, evaluating the erased terms under these assumptions faithfully simulates evaluation in Coq. Based on this, CertiCoq and coq-malfunction both implement an Eval variant that reads back Coq values and can be trusted.
• Support for primitive ints, floats and array literal values. Primitive operations are still treated as axioms to be realized in target languages and the correctness theorems do not apply in their presence yet.
• Optional passes have been added that replicate the Coq Extraction plugin's functionality, without proof (yet):
  • Inlining of defined constants (e.g. Extract Inline).
  • Reordering of constructors (e.g. part of Extract Inductive). This allows to target different representations in target languages (typically bool in OCaml).
  • Unboxing of singleton unary constructors. For example, exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 } becomes exist 1 after typed erasure and removal of constructor parameters, which can be further unboxed to just 1.
  • CoFixpoints/CoInductives to Lazy/Inductives: cofixpoints and (co)-constructors get translated to fixpoints + lazy/force constructs in lambda-box, allowing efficient evaluation of coinductive terms in target languages (supported only in coq-malfunction/ocaml extraction for now).
  • Beta-reduction. This reduces manifest beta-redexes in the erased terms, especially useful after inlining.

The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.

The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.

MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.

You can install MetaCoq directly from sources or using opam install coq-metacoq.
This release will be included in an upcoming Coq Platform.

The current release includes several subpackages, which can be compiled and installed separately if desired:

• the utils library contains extensions to the standard library (notably for reasoning with All/All-n type-valued predicates) (in directory utils, and as coq-metacoq-utils).
• the common libraries of basic definitions for the abstract syntax trees shared by multiple languages (common, coq-metacoq-common)
• the Template-Coq quoting library and plugin (template-coq / coq-metacoq-template)
• a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (pcuic / coq-metacoq-pcuic)
• a verified equivalence between Template-Coq and PCUIC typing (in directory template-pcuic and as coq-metacoq-template-pcuic)
• a total verified type-checker for Coq (safechecker / coq-metacoq-safechecker), usable inside Coq.
• a plugin interfacing with the extracted type-checker in OCaml, providing the MetaCoq SafeCheck <term> command (safechecker-plugin, coq-metacoq-safechecker-plugin)
• a verified type and proof erasure function for Coq (erasure / coq-metacoq-erasure), usable inside Coq.
• a plugin interfacing with the extracted erasure pipeline in OCaml, providing the MetaCoq Erase <term> command (erasure-plugin, coq-metacoq-erasure-plugin)
• a quoting library, allowing the quotation of terms and type derivations along with associated data structures as ASTs/terms (quotation / coq-metacoq-quotation).
• a set of example translations from Type Theory to Type Theory (translation/ coq-metacoq-translations).

A good place to start are the files demo.v, safechecker_test.v, erasure_test.v in the test-suite directory.

This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.

The MetaCoq Team

What's Changed

• Merge 8.16 into 8.17 by @yforster in #992
• Merge 8.16, 8.17 and 8.18 into main by @yforster in #993
• Replace elimtype False by exfalso by @yforster in #995
• use names in EAst.t by @tabareau in #997
• Add a let in front of case in implement_box by @yforster in #999
• Qualify imports to disable race condition for opam builds by @yforster in #1001
• Adapt to coq/coq#17576 (declare_variable takes typing flags argument) by @SkySkimmer in #1005
• Adapt to coq/coq#17836 (sort poly) by @SkySkimmer in #984
• Adapt w.r.t. coq/coq#18294. by @ppedrot in #1010
• Adapt to coq/coq#18280 (case relevance outside case info) by @SkySkimmer in #1009
• Compile pipeline app by @mattam82 in #1013
• Transform extends split by @tabareau in #1014
• Adapt wrt coq/coq#18164 by @Villetaneuse in #1011
• Adapt to coq/coq#18331 (mind_kelim -> mind_squashed) by @SkySkimmer in #1015
• Support primitive array terms by @mattam82 in #998
• squash typing hypothesis in precond by @tabareau in #1025
• Fix quotation after primitive array support by @JasonGross in #1024
• LSP Support by @yannl35133 in #1006
• Primitive evaluation by @mattam82 in #1027
• Fix breakage from coq/coq#18374 by @proux01 in #1028
• Typed extraction integration by @mattam82 in #1030
• More unified judgment type and All_local_env by @yannl35133 in #1007
• Primitive flags by @mattam82 in #1033
• Add some debugging suggestions for quotation by @JasonGross in #1031
• Restore compatibility with OCaml < 4.13 by @JasonGross in #1023
• Strengthen In_size lemma by @mattam82 in #1043
• Fix remaining warnings, minor fixups by @mattam82 in #1045
• Generalize lemmas for coq malfunction by @tabareau in #1046
• 8.18 warnings and deprecations fixes by @mattam82 in #1047
• 8.19 warnings deprecations by @mattam82 in #1048
• CI: multiple OCaml versions by @liyishuai in #1040
• erasure_pipeline_extends_app with todo irrel by @tabareau in #1050
• generalize verified_erasure_pipeline_lookup_env_in by @tabareau in #1054
• Fix typed erasure calls by @mattam82 in #1052
• Erase function lemma by @mattam82 in #1053
• Resurrect the cofix transform, adding a new axiom for the admitted pr… by @mattam82 in #1056
• Avoid Ee := EWcbvEval mo...

MetaCoq 1.3.1 for Coq 8.18

We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.18, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.

The main changes in this new version w.r.t. v1.2.1 are:

• A full integration of the typed erasure phase from the ConCert project in the erasure pipeline, with a complete correctness proof, by @mattam82. Use option MetaCoq Erase -typed to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v)
• Generalizations of the correctness and simulation lemmas by @yforster @mattam82 and @tabareau, showing in particular that erasure of applications of functions from firstorder types to firstorder types is compiled to applications, justifying separate compilation of functions and their arguments.
• Using standardization and canonicity, we also show that erased values of programs of firstorder inductive types (non-erasable inductives types for which all constructor argument types are themselves firstorder) are in direct correspondence with their Coq counterparts, allowing sound readback of these values. In other words, evaluating the erased terms under these assumptions faithfully simulates evaluation in Coq. Based on this, CertiCoq and coq-malfunction both implement an Eval variant that reads back Coq values and can be trusted.
• Support for primitive ints, floats and array literal values. Primitive operations are still treated as axioms to be realized in target languages and the correctness theorems do not apply in their presence yet.
• Optional passes have been added that replicate the Coq Extraction plugin's functionality, without proof (yet):
  • Inlining of defined constants (e.g. Extract Inline).
  • Reordering of constructors (e.g. part of Extract Inductive). This allows to target different representations in target languages (typically bool in OCaml).
  • Unboxing of singleton unary constructors. For example, exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 } becomes exist 1 after typed erasure and removal of constructor parameters, which can be further unboxed to just 1.
  • CoFixpoints/CoInductives to Lazy/Inductives: cofixpoints and (co)-constructors get translated to fixpoints + lazy/force constructs in lambda-box, allowing efficient evaluation of coinductive terms in target languages (supported only in coq-malfunction/ocaml extraction for now).
  • Beta-reduction. This reduces manifest beta-redexes in the erased terms, especially useful after inlining.

The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.

The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.

MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.

You can install MetaCoq directly from sources or using opam install coq-metacoq.
This release will be included in an upcoming Coq Platform.

The current release includes several subpackages, which can be compiled and installed separately if desired:

• the utils library contains extensions to the standard library (notably for reasoning with All/All-n type-valued predicates) (in directory utils, and as coq-metacoq-utils).
• the common libraries of basic definitions for the abstract syntax trees shared by multiple languages (common, coq-metacoq-common)
• the Template-Coq quoting library and plugin (template-coq / coq-metacoq-template)
• a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (pcuic / coq-metacoq-pcuic)
• a verified equivalence between Template-Coq and PCUIC typing (in directory template-pcuic and as coq-metacoq-template-pcuic)
• a total verified type-checker for Coq (safechecker / coq-metacoq-safechecker), usable inside Coq.
• a plugin interfacing with the extracted type-checker in OCaml, providing the MetaCoq SafeCheck <term> command (safechecker-plugin, coq-metacoq-safechecker-plugin)
• a verified type and proof erasure function for Coq (erasure / coq-metacoq-erasure), usable inside Coq.
• a plugin interfacing with the extracted erasure pipeline in OCaml, providing the MetaCoq Erase <term> command (erasure-plugin, coq-metacoq-erasure-plugin)
• a quoting library, allowing the quotation of terms and type derivations along with associated data structures as ASTs/terms (quotation / coq-metacoq-quotation).
• a set of example translations from Type Theory to Type Theory (translation/ coq-metacoq-translations).

A good place to start are the files demo.v, safechecker_test.v, erasure_test.v in the test-suite directory.

This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.

The MetaCoq Team

What's Changed

• Merge 8.16 into 8.17 by @yforster in #992
• use names in EAst.t by @tabareau in #997
• Add a let in front of case in implement_box by @yforster in #999
• Qualify imports to disable race condition for opam builds by @yforster in #1001
• Compile pipeline app by @mattam82 in #1013
• Transform extends split by @tabareau in #1014
• Support primitive array terms by @mattam82 in #998
• squash typing hypothesis in precond by @tabareau in #1025
• Fix quotation after primitive array support by @JasonGross in #1024
• LSP Support by @yannl35133 in #1006
• Primitive evaluation by @mattam82 in #1027
• Typed extraction integration by @mattam82 in #1030
• More unified judgment type and All_local_env by @yannl35133 in #1007
• Primitive flags by @mattam82 in #1033
• Add some debugging suggestions for quotation by @JasonGross in #1031
• Restore compatibility with OCaml < 4.13 by @JasonGross in #1023
• Strengthen In_size lemma by @mattam82 in #1043
• Fix remaining warnings, minor fixups by @mattam82 in #1045
• Generalize lemmas for coq malfunction by @tabareau in #1046
• 8.18 warnings and deprecations fixes by @mattam82 in #1047
• CI: multiple OCaml versions by @liyishuai in #1040
• erasure_pipeline_extends_app with todo irrel by @tabareau in #1050
• generalize verified_erasure_pipeline_lookup_env_in by @tabareau in #1054
• Fix typed erasure calls by @mattam82 in #1052
• Erase function lemma by @mattam82 in #1053
• Resurrect the cofix transform, adding a new axiom for the admitted pr… by @mattam82 in #1056
• Avoid Ee := EWcbvEval module aliases which result in ugly extraction … by @mattam82 in #1057
• Implement tLazy and tForce in EAst by @mattam82 in #1058
• Reorder constructors by @mattam82 in #1059
• Unsafe inline beta and unboxing transforms by @mattam82 in #1061
• Implement a general Show typeclass in MetaCoq.Utils by @mattam82 in #1063
• Unsafe and ewcbvevalnamed by @mattam82 in #1064
• Fix typo by @mattam82 in #1065
• Fix inlining and reorder constructors which were not translating let … by @mattam82 in #1066

New Contributors

• @liyishuai made their first contribution in #1040

Full Changelog: v1.2.1-8.18...v1.3.1-8.18

MetaCoq 1.3.1 for Coq 8.17

We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.17, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.

The main changes in this new version w.r.t. v1.2.1 are:

• A full integration of the typed erasure phase from the ConCert project in the erasure pipeline, with a complete correctness proof, by @mattam82. Use option MetaCoq Erase -typed to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v)
• Generalizations of the correctness and simulation lemmas by @yforster @mattam82 and @tabareau, showing in particular that erasure of applications of functions from firstorder types to firstorder types is compiled to applications, justifying separate compilation of functions and their arguments.
• Using standardization and canonicity, we also show that erased values of programs of firstorder inductive types (non-erasable inductives types for which all constructor argument types are themselves firstorder) are in direct correspondence with their Coq counterparts, allowing sound readback of these values. In other words, evaluating the erased terms under these assumptions faithfully simulates evaluation in Coq. Based on this, CertiCoq and coq-malfunction both implement an Eval variant that reads back Coq values and can be trusted.
• Support for primitive ints, floats and array literal values. Primitive operations are still treated as axioms to be realized in target languages and the correctness theorems do not apply in their presence yet.
• Optional passes have been added that replicate the Coq Extraction plugin's functionality, without proof (yet):
  • Inlining of defined constants (e.g. Extract Inline).
  • Reordering of constructors (e.g. part of Extract Inductive). This allows to target different representations in target languages (typically bool in OCaml).
  • Unboxing of singleton unary constructors. For example, exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 } becomes exist 1 after typed erasure and removal of constructor parameters, which can be further unboxed to just 1.
  • CoFixpoints/CoInductives to Lazy/Inductives: cofixpoints and (co)-constructors get translated to fixpoints + lazy/force constructs in lambda-box, allowing efficient evaluation of coinductive terms in target languages (supported only in coq-malfunction/ocaml extraction for now).
  • Beta-reduction. This reduces manifest beta-redexes in the erased terms, especially useful after inlining.

The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.

The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.

MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.

You can install MetaCoq directly from sources or using opam install coq-metacoq.
This release will be included in an upcoming Coq Platform.

The current release includes several subpackages, which can be compiled and installed separately if desired:

• the utils library contains extensions to the standard library (notably for reasoning with All/All-n type-valued predicates) (in directory utils, and as coq-metacoq-utils).
• the common libraries of basic definitions for the abstract syntax trees shared by multiple languages (common, coq-metacoq-common)
• the Template-Coq quoting library and plugin (template-coq / coq-metacoq-template)
• a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (pcuic / coq-metacoq-pcuic)
• a verified equivalence between Template-Coq and PCUIC typing (in directory template-pcuic and as coq-metacoq-template-pcuic)
• a total verified type-checker for Coq (safechecker / coq-metacoq-safechecker), usable inside Coq.
• a plugin interfacing with the extracted type-checker in OCaml, providing the MetaCoq SafeCheck <term> command (safechecker-plugin, coq-metacoq-safechecker-plugin)
• a verified type and proof erasure function for Coq (erasure / coq-metacoq-erasure), usable inside Coq.
• a plugin interfacing with the extracted erasure pipeline in OCaml, providing the MetaCoq Erase <term> command (erasure-plugin, coq-metacoq-erasure-plugin)
• a quoting library, allowing the quotation of terms and type derivations along with associated data structures as ASTs/terms (quotation / coq-metacoq-quotation).
• a set of example translations from Type Theory to Type Theory (translation/ coq-metacoq-translations).

A good place to start are the files demo.v, safechecker_test.v, erasure_test.v in the test-suite directory.

This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.

The MetaCoq Team

What's Changed

• Merge 8.16 into 8.17 by @yforster in #992
• use names in EAst.t by @tabareau in #997
• Add a let in front of case in implement_box by @yforster in #999
• Qualify imports to disable race condition for opam builds by @yforster in #1001
• Compile pipeline app by @mattam82 in #1013
• Transform extends split by @tabareau in #1014
• Support primitive array terms by @mattam82 in #998
• squash typing hypothesis in precond by @tabareau in #1025
• Fix quotation after primitive array support by @JasonGross in #1024
• LSP Support by @yannl35133 in #1006
• Primitive evaluation by @mattam82 in #1027
• Typed extraction integration by @mattam82 in #1030
• More unified judgment type and All_local_env by @yannl35133 in #1007
• Primitive flags by @mattam82 in #1033
• Add some debugging suggestions for quotation by @JasonGross in #1031
• Restore compatibility with OCaml < 4.13 by @JasonGross in #1023
• Strengthen In_size lemma by @mattam82 in #1043
• Fix remaining warnings, minor fixups by @mattam82 in #1045
• Generalize lemmas for coq malfunction by @tabareau in #1046
• 8.18 warnings and deprecations fixes by @mattam82 in #1047
• CI: multiple OCaml versions by @liyishuai in #1040
• erasure_pipeline_extends_app with todo irrel by @tabareau in #1050
• generalize verified_erasure_pipeline_lookup_env_in by @tabareau in #1054
• Fix typed erasure calls by @mattam82 in #1052
• Erase function lemma by @mattam82 in #1053
• Resurrect the cofix transform, adding a new axiom for the admitted pr… by @mattam82 in #1056
• Avoid Ee := EWcbvEval module aliases which result in ugly extraction … by @mattam82 in #1057
• Implement tLazy and tForce in EAst by @mattam82 in #1058
• Reorder constructors by @mattam82 in #1059
• Unsafe inline beta and unboxing transforms by @mattam82 in #1061
• Implement a general Show typeclass in MetaCoq.Utils by @mattam82 in #1063
• Unsafe and ewcbvevalnamed by @mattam82 in #1064
• Fix typo by @mattam82 in #1065
• Fix inlining and reorder constructors which were not translating let … by @mattam82 in #1066

New Contributors

• @liyishuai made their first contribution in #1040

Full Changelog: v1.2.1-8.18...v1.3.1-8.18

MetaCoq 1.3 for Coq 8.17

We are happy to announce release 1.3 of the MetaCoq project for Coq 8.17, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.

The main changes in this new version are (w.r.t. v1.2.1):

• A full integration of the typed erasure phase from the ConCert project in the erasure pipeline, with a complete correctness proof, by @mattam82. Use option MetaCoq Erase -typed to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v)
• Generalizations of the correctness and simulation lemmas by @yforster @mattam82 and @tabareau, showing in particular that erasure of applications of functions from firstorder types to firstorder types is compiled to applications, justifying separate compilation of functions and their arguments.
• Using standardization and canonicity, we also show that erased values of programs of firstorder inductive types (non-erasable inductives types for which all constructor argument types are themselves firstorder) are in direct correspondence with their Coq counterparts, allowing sound readback of these values. In other words, evaluating the erased terms under these assumptions faithfully simulates evaluation in Coq. Based on this, CertiCoq and coq-malfunction both implement an Eval variant that reads back Coq values and can be trusted.
• Support for primitive ints, floats and array literal values. Primitive operations are still treated as axioms to be realized in target languages and the correctness theorems do not apply in their presence yet.
• Optional passes have been added that replicate the Coq Extraction plugin's functionality, without proof (yet):
  • Inlining of defined constants (e.g. Extract Inline).
  • Reordering of constructors (e.g. part of Extract Inductive). This allows to target different representations in target languages (typically bool in OCaml).
  • Unboxing of singleton unary constructors. For example, exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 } becomes exist 1 after typed erasure and removal of constructor parameters, which can be further unboxed to just 1.
  • CoFixpoints/CoInductives to Lazy/Inductives: cofixpoints and (co)-constructors get translated to fixpoints + lazy/force constructs in lambda-box, allowing efficient evaluation of coinductive terms in target languages (supported only in coq-malfunction/ocaml extraction for now).
  • Beta-reduction. This reduces manifest beta-redexes in the erased terms, especially useful after inlining.

The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.

The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.

MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.

You can install MetaCoq directly from sources or using opam install coq-metacoq.
This release will be included in an upcoming Coq Platform.

The current release includes several subpackages, which can be compiled and installed separately if desired:

• the utils library contains extensions to the standard library (notably for reasoning with All/All-n type-valued predicates) (in directory utils, and as coq-metacoq-utils).
• the common libraries of basic definitions for the abstract syntax trees shared by multiple languages (common, coq-metacoq-common)
• the Template-Coq quoting library and plugin (template-coq / coq-metacoq-template)
• a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (pcuic / coq-metacoq-pcuic)
• a verified equivalence between Template-Coq and PCUIC typing (in directory template-pcuic and as coq-metacoq-template-pcuic)
• a total verified type-checker for Coq (safechecker / coq-metacoq-safechecker), usable inside Coq.
• a plugin interfacing with the extracted type-checker in OCaml, providing the MetaCoq SafeCheck <term> command (safechecker-plugin, coq-metacoq-safechecker-plugin)
• a verified type and proof erasure function for Coq (erasure / coq-metacoq-erasure), usable inside Coq.
• a plugin interfacing with the extracted erasure pipeline in OCaml, providing the MetaCoq Erase <term> command (erasure-plugin, coq-metacoq-erasure-plugin)
• a quoting library, allowing the quotation of terms and type derivations along with associated data structures as ASTs/terms (quotation / coq-metacoq-quotation).
• a set of example translations from Type Theory to Type Theory (translation/ coq-metacoq-translations).

A good place to start are the files demo.v, safechecker_test.v, erasure_test.v in the test-suite directory.

This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.

The MetaCoq Team

What's Changed

• Compile pipeline app by @mattam82 in #1013
• Transform extends split by @tabareau in #1014
• Support primitive array terms by @mattam82 in #998
• squash typing hypothesis in precond by @tabareau in #1025
• Fix quotation after primitive array support by @JasonGross in #1024
• LSP Support by @yannl35133 in #1006
• Primitive evaluation by @mattam82 in #1027
• Typed extraction integration by @mattam82 in #1030
• More unified judgment type and All_local_env by @yannl35133 in #1007
• Primitive flags by @mattam82 in #1033
• Add some debugging suggestions for quotation by @JasonGross in #1031
• Restore compatibility with OCaml < 4.13 by @JasonGross in #1023
• Strengthen In_size lemma by @mattam82 in #1043
• Fix remaining warnings, minor fixups by @mattam82 in #1045
• Generalize lemmas for coq malfunction by @tabareau in #1046
• CI: multiple OCaml versions by @liyishuai in #1040
• erasure_pipeline_extends_app with todo irrel by @tabareau in #1050
• generalize verified_erasure_pipeline_lookup_env_in by @tabareau in #1054
• Fix typed erasure calls by @mattam82 in #1052
• Erase function lemma by @mattam82 in #1053
• Resurrect the cofix transform, adding a new axiom for the admitted pr… by @mattam82 in #1056
• Avoid Ee := EWcbvEval module aliases which result in ugly extraction … by @mattam82 in #1057
• Implement tLazy and tForce in EAst by @mattam82 in #1058
• Reorder constructors by @mattam82 in #1059
• Unsafe inline beta and unboxing transforms by @mattam82 in #1061
• Implement a general Show typeclass in MetaCoq.Utils by @mattam82 in #1063
• Unsafe and ewcbvevalnamed by @mattam82 in #1064
• Fix typo by @mattam82 in #1065

New Contributors

• @liyishuai made their first contribution in #1040

Full Changelog: v1.2.1-8.17...v1.3-8.17

MetaCoq 1.2.1 for Coq 8.18

This is a minor release synchronising the state of coq-8.17 and coq-8.18 to allow publishing an opam package for Coq 8.18. See https://github.com/MetaCoq/metacoq/releases/tag/v1.2-8.17 for detailed release notes.

What's Changed

• Fix monad_map_branches_k name by @JasonGross in #953
• Add boolean versions of the varieties of extends by @JasonGross in #954
• Add union and inter checker flags by @JasonGross in #957
• Adapt w.r.t. coq/coq#17564. by @ppedrot in #960
• Add MCListable class for enumerating finite types by @JasonGross in #962
• Close computational obligations with defined in erase_global_decls by @yforster in #961
• Invariants in named recursion rule by @yforster in #967
• Drastically speed up ByteCompareSpec by @JasonGross in #988
• Verified erasure pipeline by @mattam82 in #987
• add not_isErasable lemma in EArities by @tabareau in #990
• Add quotation API for context and global_env_ext by @JasonGross in #996

Additionally, the following adaptions were necessary to work with Coq 8.18:

Show

• Update coq 8.18 with commits from 8.17 by @yforster in #1000
• Update 8.18 again with Makefile and opam change by @yforster in #1003
• Merge 8.16 and 8.17 into 8.18 by @yforster in #991
• Adapt to coq/coq#16890 (Classes.existing_instance takes globref not qualid) by @SkySkimmer in #959
• Remove bugkncst by @SkySkimmer in #963
• Adapt to coq/coq#17633 (decompose_app returns array not list) by @SkySkimmer in #965
• Adapt to coq/coq#17585 (revised warning API) by @SkySkimmer in #964
• Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool) by @SkySkimmer in #968
• Bump cachix/install-nix-action from 20 to 21 by @dependabot in #966
• Add a merge operation for the global env by @JasonGross in #955
• Use : Set explicitly when needed by @SkySkimmer in #971
• Bump cachix/install-nix-action from 21 to 22 by @dependabot in #970
• Bump cachix/install-nix-action from 21 to 22 by @dependabot in #973
• Bump cachix/install-nix-action from 20 to 22 by @dependabot in #974
• Adapt w.r.t. coq/coq#17781. by @ppedrot in #972
• Adapt to coq PR #17991 which lets "simpl" refolds partial applications of fixpoints by @herbelin in #975
• Bump actions/checkout from 3 to 4 by @dependabot in #978
• Bump actions/checkout from 3 to 4 by @dependabot in #977
• Bump cachix/install-nix-action from 22 to 23 by @dependabot in #979
• Bump actions/checkout from 3 to 4 by @dependabot in #982
• improve strengthening to get cumul info on type by @tabareau in #985
• remove parameters in firstorder inductive types by @tabareau in #986
• Remove Int31 by @Villetaneuse in #983
• Adapt w.r.t. coq/coq#16004. by @ppedrot in #721
• Adapt w.r.t. coq/coq#16004. by @ppedrot in #724
• prepare for coq/coq#16289 by @mrhaandi in #734
• improved auto goal selection by @mrhaandi in #737
• Adapt w.r.t. coq/coq#16442. by @ppedrot in #755
• Master cherry picks by @mattam82 in #759
• Adapt w.r.t. coq/coq#16933. by @ppedrot in #797
• Adapt w.r.t. coq/coq#16904. by @ppedrot in #798
• Adapt to coq/coq#16938 (staged options) by @SkySkimmer in #804
• Don't force references at linking time by @SkySkimmer in #809
• Adapt w.r.t. coq/coq#16903. by @ppedrot in #806
• Adapt w.r.t. coq/coq#17049. by @ppedrot in #824
• Adapt w.r.t. coq/coq#17091. by @ppedrot in #827
• Adapt w.r.t coq/coq#17021 by @andres-erbsen in #823
• Adapt to coq/coq#17220 (genargs are not holes) by @SkySkimmer in #835
• Adapt to coq/coq#17283 (more careful handling of univ mono term constructors) by @SkySkimmer in #861
• Adapt to coq/coq#17331 by @maximedenes in #895
• Adapt to coq/coq#17293 (wit_red_expr moved) by @SkySkimmer in #860

Full Changelog: v1.2-8.17...v1.2.1-8.18