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. 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 https://github.com/MetaCoq/metacoq/pull/774 Bring back ReflectEq instances in ReflectAst by @JasonGross in https://github.com/MetaCoq/metacoq/pull/782 Add some template monad mapping utils by @JasonGross in https://github.com/MetaCoq/metacoq/pull/783 Add Module Type DeclarationTypingSig by @JasonGross in https://github.com/MetaCoq/metacoq/pull/781 isSort and isArity return bool now by @JasonGross in https://github.com/MetaCoq/metacoq/pull/785 Move Template.TypingWf.on_option to Template.utils.MCOption.on_some_or_none by @JasonGross in https://github.com/MetaCoq/metacoq/pull/786 Remove trailing whitespace by @JasonGross in https://github.com/MetaCoq/metacoq/pull/773 Use match in on_ind_body by @JasonGross in https://github.com/MetaCoq/metacoq/pull/778 Automatically trim whitespace in vscode by @yforster in https://github.com/MetaCoq/metacoq/pull/788 Helper combinators and lemmas to typecheck pattern matches by @kyoDralliam in https://github.com/MetaCoq/metacoq/pull/787 remove direct access to the environment and more compact interface by @tabareau in https://github.com/MetaCoq/metacoq/pull/793 add abstract_env_leqb_level_n by @tabareau in https://github.com/MetaCoq/metacoq/pull/799 remove need for abstract_env_ext_wf_universeb by @tabareau in https://github.com/MetaCoq/metacoq/pull/800 Add weakening_env_cored by @JasonGross in https://github.com/MetaCoq/metacoq/pull/801 Add hd_error_skipn_iff_In by @JasonGross in https://github.com/MetaCoq/metacoq/pull/803 make -C erasure/ uninstall no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/805 simplify abstract_env_is_consistent_correct by @tabareau in https://github.com/MetaCoq/metacoq/pull/807 notation <# _ #> for quoting programs (global_env + term) by @kyoDralliam in https://github.com/MetaCoq/metacoq/pull/796 remove the need for leqb_level_n_spec0_gen by @tabareau in https://github.com/MetaCoq/metacoq/pull/814 make -C safechecker/ uninstall no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/810 make uninstall no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/811 make -C pcuic/ uninstall no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/812 Minor reorganization around extends, fresh_global by @JasonGross in https://github.com/MetaCoq/metacoq/pull/802 tmFixpoint combinator (without unsetting Guard Checking) by @JasonGross in https://github.com/MetaCoq/metacoq/pull/790 Turn normalisation into a typeclass by @JasonGross in https://github.com/MetaCoq/metacoq/pull/792 Add trans_one_inductive_entry by @JasonGross in https://github.com/MetaCoq/metacoq/pull/789 Trim trailing whitespace, this time enabled instead of disabled by @yforster in https://github.com/MetaCoq/metacoq/pull/795 use In instead of mem in abstract_env_level_mem_correct by @tabareau in https://github.com/MetaCoq/metacoq/pull/817 Add (only parsing) to <# x #> notation by @JasonGross in https://github.com/MetaCoq/metacoq/pull/819 better spec for abstract_env_lookup_correct by @tabareau in https://github.com/MetaCoq/metacoq/pull/820 Add PCUIC versions of tmQuote and related template monad definitions by @JasonGross in https://github.com/MetaCoq/metacoq/pull/776 Change specification of declared constant and co by @tabareau in https://github.com/MetaCoq/metacoq/pull/822 Allow environment weakening to reorder declarations by @JasonGross in https://github.com/MetaCoq/metacoq/pull/816 Fail if a patch is not applicable by @yforster in https://github.com/MetaCoq/metacoq/pull/818 Add some more utility lemmas in All_Forall by @JasonGross in https://github.com/MetaCoq/metacoq/pull/821 Add consistency and normalization and reorganize by @tabareau in https://github.com/MetaCoq/metacoq/pull/825 add PCUICCasesHelper to be compiled by @kyoDralliam in https://github.com/MetaCoq/metacoq/pull/826 the main change is reordering of context in urenaming by @tabareau in https://github.com/MetaCoq/metacoq/pull/828 Add utils and common initial folders and reorganize code and plugins by @tabareau in https://github.com/MetaCoq/metacoq/pull/829 Named semantics with environments for lambda box by @yforster in https://github.com/MetaCoq/metacoq/pull/832 Don't use Type inductives for Props by @JasonGross in https://github.com/MetaCoq/metacoq/pull/836 Allow weakening of typing across different checker configs by @JasonGross in https://github.com/MetaCoq/metacoq/pull/848 Add some Proof using annotations by @JasonGross in https://github.com/MetaCoq/metacoq/pull/849 Add WeightedGraphSig by @JasonGross in https://github.com/MetaCoq/metacoq/pull/854 Add tmLocateModule and tmLocateModType by @JasonGross in https://github.com/MetaCoq/metacoq/pull/855 Generalize tmExistingInstance across localities by @JasonGross in https://github.com/MetaCoq/metacoq/pull/857 Fix and generalize module quotation by @JasonGross in https://github.com/MetaCoq/metacoq/pull/856 Add LevelSetOrdProp by @JasonGross in https://github.com/MetaCoq/metacoq/pull/858 Add KernameSetOrdProp by @JasonGross in https://github.com/MetaCoq/metacoq/pull/859 Fix safechecker plugin install by @4ever2 in https://github.com/MetaCoq/metacoq/pull/868 Bump install-nix-action by @JasonGross in https://github.com/MetaCoq/metacoq/pull/866 Add .github/dependabot.yml by @JasonGross in https://github.com/MetaCoq/metacoq/pull/867 fix CI issue by running chown -R coq:coq earlier by @yforster in https://github.com/MetaCoq/metacoq/pull/870 Rework Progress, Standardization, Canonicity and Consistency by @tabareau in https://github.com/MetaCoq/metacoq/pull/872 Bump actions/checkout from 2 to 3 by @dependabot in https://github.com/MetaCoq/metacoq/pull/869 Typed erasure integration by @mattam82 in https://github.com/MetaCoq/metacoq/pull/834 Add DeclarationTypingSig by @JasonGross in https://github.com/MetaCoq/metacoq/pull/873 Add {LevelExpr,Constraint}SetOrdProp, LevelExprSetDecide by @JasonGross in https://github.com/MetaCoq/metacoq/pull/863 Add some utility tactics and decidability properties by @JasonGross in https://github.com/MetaCoq/metacoq/pull/837 Fix nix CI: erasure needs to come after template-pcuic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/877 Actually fix dependency order of packages on nix by @JasonGross in https://github.com/MetaCoq/metacoq/pull/891 Add target to update template-coq _PluginProject.in by @JasonGross in https://github.com/MetaCoq/metacoq/pull/892 Add modules for the eq decision routines for term and associated constants by @JasonGross in https://github.com/MetaCoq/metacoq/pull/887 Fix ordering of template-pcuic in cachedMake by @JasonGross in https://github.com/MetaCoq/metacoq/pull/885 Add template-pcuic as dep of erasure by @JasonGross in https://github.com/MetaCoq/metacoq/pull/884 Make Monad a cumulative inductive type by @JasonGross in https://github.com/MetaCoq/metacoq/pull/883 Add Monad instance for identity monad by @JasonGross in https://github.com/MetaCoq/metacoq/pull/881 Generalize Monad{Basic,}Ast to work in any monad by @JasonGross in https://github.com/MetaCoq/metacoq/pull/880 Add Set MetaCoq Template Monad Debug by @JasonGross in https://github.com/MetaCoq/metacoq/pull/879 Also run nix ci on the coq-8.16 branch by @JasonGross in https://github.com/MetaCoq/metacoq/pull/890 Rename Informative to Subsingleton by @yforster in https://github.com/MetaCoq/metacoq/pull/889 Decidability of consistent_extension_on by @JasonGross in https://github.com/MetaCoq/metacoq/pull/838 Add UniverseMap, UniverseMapFact by @JasonGross in https://github.com/MetaCoq/metacoq/pull/882 Make option_instance universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/893 Make on_some{,_or_none} universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/896 Make MonadAst universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/897 Disambiguate Requires among the MetaCoq modules by @JasonGross in https://github.com/MetaCoq/metacoq/pull/899 Add MCMSets by @JasonGross in https://github.com/MetaCoq/metacoq/pull/900 Add Utils.MCFSets for FSets.FMap* utils by @JasonGross in https://github.com/MetaCoq/metacoq/pull/901 Gallina quotation functions for Template by @JasonGross in https://github.com/MetaCoq/metacoq/pull/894 rework extraction by @tabareau in https://github.com/MetaCoq/metacoq/pull/902 Make proofs more robust for eventually making All_Forall polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/903 Update descriptions and dependencies of the quotation module by @JasonGross in https://github.com/MetaCoq/metacoq/pull/904 Populate some early MSets and FSets modules by @JasonGross in https://github.com/MetaCoq/metacoq/pull/905 Remove some duplicate code in quotation by @JasonGross in https://github.com/MetaCoq/metacoq/pull/906 Refactor quotation of MSets,FMaps to use MC{MSets,FSets} by @JasonGross in https://github.com/MetaCoq/metacoq/pull/907 Use a more systematic mangling of universe names by @JasonGro