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. rocq-prover/rocq#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 rocq-prover/rocq#16890 (Classes.existing_instance takes globref not qualid) by @SkySkimmer in #959
• Remove bugkncst by @SkySkimmer in #963
• Adapt to rocq-prover/rocq#17633 (decompose_app returns array not list) by @SkySkimmer in #965
• Adapt to rocq-prover/rocq#17585 (revised warning API) by @SkySkimmer in #964
• Adapt to rocq-prover/rocq#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. rocq-prover/rocq#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. rocq-prover/rocq#16004. by @ppedrot in #721
• Adapt w.r.t. rocq-prover/rocq#16004. by @ppedrot in #724
• prepare for rocq-prover/rocq#16289 by @mrhaandi in #734
• improved auto goal selection by @mrhaandi in #737
• Adapt w.r.t. rocq-prover/rocq#16442. by @ppedrot in #755
• Master cherry picks by @mattam82 in #759
• Adapt w.r.t. rocq-prover/rocq#16933. by @ppedrot in #797
• Adapt w.r.t. rocq-prover/rocq#16904. by @ppedrot in #798
• Adapt to rocq-prover/rocq#16938 (staged options) by @SkySkimmer in #804
• Don't force references at linking time by @SkySkimmer in #809
• Adapt w.r.t. rocq-prover/rocq#16903. by @ppedrot in #806
• Adapt w.r.t. rocq-prover/rocq#17049. by @ppedrot in #824
• Adapt w.r.t. rocq-prover/rocq#17091. by @ppedrot in #827
• Adapt w.r.t rocq-prover/rocq#17021 by @andres-erbsen in #823
• Adapt to rocq-prover/rocq#17220 (genargs are not holes) by @SkySkimmer in #835
• Adapt to rocq-prover/rocq#17283 (more careful handling of univ mono term constructors) by @SkySkimmer in #861
• Adapt to rocq-prover/rocq#17331 by @maximedenes in #895
• Adapt to rocq-prover/rocq#17293 (wit_red_expr moved) by @SkySkimmer in #860

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

MetaCoq 1.2.1 for Coq 8.17

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
• 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
• Add a merge operation for the global env by @JasonGross in #955
• improve strengthening to get cumul info on type by @tabareau in #985
• remove parameters in firstorder inductive types by @tabareau in #986
• 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
• 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

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

MetaCoq 1.2 for Coq 8.17

We are happy to announce release 1.2 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.1.1):

• A cleaned-up abstract environment structure for the implementation of the verified type-checker and cleaned-up canonicity and consistency theorems by @tabareau.
• A new quotation library with a work-in-progress proof of Löb's theorem by @JasonGross.
• An integration of the typed erasure phase of the ConCert project by @annenkov and @mattam82.
  Beware, adaptation of the correctness proof is not finished and it is not integrated in the extracted pipeline of MetaCoq Erase yet.
• Reorganization of the packages, separating plugins from theories by @tabareau.

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.

MetaCoq is developed by Abhishek Anand, Danil Annenkov, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Jason Gross, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.

The MetaCoq Team

What's Changed

• Add monad_option_map by @JasonGross in #774
• Bring back ReflectEq instances in ReflectAst by @JasonGross in #782
• Add some template monad mapping utils by @JasonGross in #783
• Add Module Type DeclarationTypingSig by @JasonGross in #781
• isSort and isArity return bool now by @JasonGross in #785
• Move Template.TypingWf.on_option to Template.utils.MCOption.on_some_or_none by @JasonGross in #786
• Remove trailing whitespace by @JasonGross in #773
• Use match in on_ind_body by @JasonGross in #778
• Automatically trim whitespace in vscode by @yforster in #788
• Helper combinators and lemmas to typecheck pattern matches by @kyoDralliam in #787
• remove direct access to the environment and more compact interface by @tabareau in #793
• add abstract_env_leqb_level_n by @tabareau in #799
• remove need for abstract_env_ext_wf_universeb by @tabareau in #800
• Add weakening_env_cored by @JasonGross in #801
• Add hd_error_skipn_iff_In by @JasonGross in #803
• make -C erasure/ uninstall no longer builds code first by @JasonGross in #805
• simplify abstract_env_is_consistent_correct by @tabareau in #807
• notation <# _ #> for quoting programs (global_env + term) by @kyoDralliam in #796
• remove the need for leqb_level_n_spec0_gen by @tabareau in #814
• make -C safechecker/ uninstall no longer builds code first by @JasonGross in #810
• make uninstall no longer builds code first by @JasonGross in #811
• make -C pcuic/ uninstall no longer builds code first by @JasonGross in #812
• Minor reorganization around extends, fresh_global by @JasonGross in #802
• tmFixpoint combinator (without unsetting Guard Checking) by @JasonGross in #790
• Turn normalisation into a typeclass by @JasonGross in #792
• Add trans_one_inductive_entry by @JasonGross in #789
• Trim trailing whitespace, this time enabled instead of disabled by @yforster in #795
• use In instead of mem in abstract_env_level_mem_correct by @tabareau in #817
• Add (only parsing) to <# x #> notation by @JasonGross in #819
• better spec for abstract_env_lookup_correct by @tabareau in #820
• Add PCUIC versions of tmQuote and related template monad definitions by @JasonGross in #776
• Change specification of declared constant and co by @tabareau in #822
• Allow environment weakening to reorder declarations by @JasonGross in #816
• Fail if a patch is not applicable by @yforster in #818
• Add some more utility lemmas in All_Forall by @JasonGross in #821
• Add consistency and normalization and reorganize by @tabareau in #825
• add PCUICCasesHelper to be compiled by @kyoDralliam in #826
• the main change is reordering of context in urenaming by @tabareau in #828
• Add utils and common initial folders and reorganize code and plugins by @tabareau in #829
• Named semantics with environments for lambda box by @yforster in #832
• Don't use Type inductives for Props by @JasonGross in #836
• Allow weakening of typing across different checker configs by @JasonGross in #848
• Add some Proof using annotations by @JasonGross in #849
• Add WeightedGraphSig by @JasonGross in #854
• Add tmLocateModule and tmLocateModType by @JasonGross in #855
• Generalize tmExistingInstance across localities by @JasonGross in #857
• Fix and generalize module quotation by @JasonGross in #856
• Add LevelSetOrdProp by @JasonGross in #858
• Add KernameSetOrdProp by @JasonGross in #859
• Fix safechecker plugin install by @4ever2 in #868
• Bump install-nix-action by @JasonGross in #866
• Add .github/dependabot.yml by @JasonGross in #867
• fix CI issue ...

MetaCoq 1.2 for Coq 8.16

We are happy to announce release 1.2 of the MetaCoq project for Coq 8.16, 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.1.1):

• A cleaned-up abstract environment structure for the implementation of the verified type-checker and cleaned-up canonicity and consistency theorems by @tabareau.
• A new quotation library with a work-in-progress proof of Löb's theorem by @JasonGross.
• An integration of the typed erasure phase of the ConCert project by @annenkov and @mattam82.
  Beware, adaptation of the correctness proof is not finished and it is not integrated in the extracted pipeline of MetaCoq Erase yet.
• Reorganization of the packages, separating plugins from theories by @tabareau.

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.

MetaCoq is developed by Abhishek Anand, Danil Annenkov, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Jason Gross, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.

The MetaCoq Team

What's Changed

• Add monad_option_map by @JasonGross in #774
• Bring back ReflectEq instances in ReflectAst by @JasonGross in #782
• Add some template monad mapping utils by @JasonGross in #783
• Add Module Type DeclarationTypingSig by @JasonGross in #781
• isSort and isArity return bool now by @JasonGross in #785
• Move Template.TypingWf.on_option to Template.utils.MCOption.on_some_or_none by @JasonGross in #786
• Remove trailing whitespace by @JasonGross in #773
• Use match in on_ind_body by @JasonGross in #778
• Automatically trim whitespace in vscode by @yforster in #788
• Helper combinators and lemmas to typecheck pattern matches by @kyoDralliam in #787
• remove direct access to the environment and more compact interface by @tabareau in #793
• add abstract_env_leqb_level_n by @tabareau in #799
• remove need for abstract_env_ext_wf_universeb by @tabareau in #800
• Add weakening_env_cored by @JasonGross in #801
• Add hd_error_skipn_iff_In by @JasonGross in #803
• make -C erasure/ uninstall no longer builds code first by @JasonGross in #805
• simplify abstract_env_is_consistent_correct by @tabareau in #807
• notation <# _ #> for quoting programs (global_env + term) by @kyoDralliam in #796
• remove the need for leqb_level_n_spec0_gen by @tabareau in #814
• make -C safechecker/ uninstall no longer builds code first by @JasonGross in #810
• make uninstall no longer builds code first by @JasonGross in #811
• make -C pcuic/ uninstall no longer builds code first by @JasonGross in #812
• Minor reorganization around extends, fresh_global by @JasonGross in #802
• tmFixpoint combinator (without unsetting Guard Checking) by @JasonGross in #790
• Turn normalisation into a typeclass by @JasonGross in #792
• Add trans_one_inductive_entry by @JasonGross in #789
• Trim trailing whitespace, this time enabled instead of disabled by @yforster in #795
• use In instead of mem in abstract_env_level_mem_correct by @tabareau in #817
• Add (only parsing) to <# x #> notation by @JasonGross in #819
• better spec for abstract_env_lookup_correct by @tabareau in #820
• Add PCUIC versions of tmQuote and related template monad definitions by @JasonGross in #776
• Change specification of declared constant and co by @tabareau in #822
• Allow environment weakening to reorder declarations by @JasonGross in #816
• Fail if a patch is not applicable by @yforster in #818
• Add some more utility lemmas in All_Forall by @JasonGross in #821
• Add consistency and normalization and reorganize by @tabareau in #825
• add PCUICCasesHelper to be compiled by @kyoDralliam in #826
• the main change is reordering of context in urenaming by @tabareau in #828
• Add utils and common initial folders and reorganize code and plugins by @tabareau in #829
• Named semantics with environments for lambda box by @yforster in #832
• Don't use Type inductives for Props by @JasonGross in #836
• Allow weakening of typing across different checker configs by @JasonGross in #848
• Add some Proof using annotations by @JasonGross in #849
• Add WeightedGraphSig by @JasonGross in #854
• Add tmLocateModule and tmLocateModType by @JasonGross in #855
• Generalize tmExistingInstance across localities by @JasonGross in #857
• Fix and generalize module quotation by @JasonGross in #856
• Add LevelSetOrdProp by @JasonGross in #858
• Add KernameSetOrdProp by @JasonGross in #859
• Fix safechecker plugin install by @4ever2 in #868
• Bump install-nix-action by @JasonGross in #866
• Add .github/dependabot.yml by @JasonGross in #867
• fix CI issue ...

MetaCoq 1.1.1 for Coq 8.16

MetaCoq 1.1.1 is a patch release of MetaCoq 1.1 removing unsafe extraction directives and with support for printing floating point values.

See https://github.com/MetaCoq/metacoq/releases/tag/v1.1-8.16 for the 1.1 release notes.

MetaCoq 1.1.1 for Coq 8.15

MetaCoq 1.1.1 is a patch release of MetaCoq 1.1 removing unsafe extraction directives and with support for printing floating point values.

See https://github.com/MetaCoq/metacoq/releases/tag/v1.1-8.15 for the 1.1 release notes.

MetaCoq 1.1.1 for Coq 8.14

MetaCoq 1.1.1 is a patch release of MetaCoq 1.1 removing unsafe extraction directives and with support for printing floating point values.

See https://github.com/MetaCoq/metacoq/releases/tag/v1.1-8.14 for the 1.1 release notes.