MetaCoq/metacoq v1.2-8.17

MetaCoq 1.2 for Coq 8.17

on GitHub

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 by running chown -R coq:coq earlier by @yforster in #870
• Rework Progress, Standardization, Canonicity and Consistency by @tabareau in #872
• Bump actions/checkout from 2 to 3 by @dependabot in #869
• Typed erasure integration by @mattam82 in #834
• Add DeclarationTypingSig by @JasonGross in #873
• Add {LevelExpr,Constraint}SetOrdProp, LevelExprSetDecide by @JasonGross in #863
• Add some utility tactics and decidability properties by @JasonGross in #837
• Fix nix CI: erasure needs to come after template-pcuic by @JasonGross in #877
• Actually fix dependency order of packages on nix by @JasonGross in #891
• Add target to update template-coq _PluginProject.in by @JasonGross in #892
• Add modules for the eq decision routines for term and associated constants by @JasonGross in #887
• Fix ordering of template-pcuic in cachedMake by @JasonGross in #885
• Add template-pcuic as dep of erasure by @JasonGross in #884
• Make Monad a cumulative inductive type by @JasonGross in #883
• Add Monad instance for identity monad by @JasonGross in #881
• Generalize Monad{Basic,}Ast to work in any monad by @JasonGross in #880
• Add Set MetaCoq Template Monad Debug by @JasonGross in #879
• Also run nix ci on the coq-8.16 branch by @JasonGross in #890
• Rename Informative to Subsingleton by @yforster in #889
• Decidability of consistent_extension_on by @JasonGross in #838
• Add UniverseMap, UniverseMapFact by @JasonGross in #882
• Make option_instance universe polymorphic by @JasonGross in #893
• Make on_some{,_or_none} universe polymorphic by @JasonGross in #896
• Make MonadAst universe polymorphic by @JasonGross in #897
• Disambiguate Requires among the MetaCoq modules by @JasonGross in #899
• Add MCMSets by @JasonGross in #900
• Add Utils.MCFSets for FSets.FMap* utils by @JasonGross in #901
• Gallina quotation functions for Template by @JasonGross in #894
• rework extraction by @tabareau in #902
• Make proofs more robust for eventually making All_Forall polymorphic by @JasonGross in #903
• Update descriptions and dependencies of the quotation module by @JasonGross in #904
• Populate some early MSets and FSets modules by @JasonGross in #905
• Remove some duplicate code in quotation by @JasonGross in #906
• Refactor quotation of MSets,FMaps to use MC{MSets,FSets} by @JasonGross in #907
• Use a more systematic mangling of universe names by @JasonGross in #908
• Finish Gallina quotation to Template, inlcuding TypingWf by @JasonGross in #898
• [quotation] Fuse Template Monad loops by @JasonGross in #909
• [CI] Add concurrency and cancel-in-progress: true by @JasonGross in #910
• [Quotation] Add quote_red by @JasonGross in #912
• Remove dead commented code in Quotation by @JasonGross in #914
• Add missing tests to test-suite/_CoqProject.in by @JasonGross in #915
• Move template-pcuic part of Loader where it belongs by @JasonGross in #917
• Add PCUIC.PCUICMonadAst by @JasonGross in #918
• [Quotation.ToTemplate] Minor adjustments by @JasonGross in #919
• [Quotation.ToTemplate] Remove dead imports by @JasonGross in #920
• [PCUIC] Add convenience notations for tInt, tFloat by @JasonGross in #921
• Improve performance of PCUIC Template Monad by @JasonGross in #922
• Add DirPath{Set,Map} by @JasonGross in #923
• [PCUIC] Have isArity return bool by @JasonGross in #924
• [Quotation.ToTemplate] Remove dead code by @JasonGross in #925
• Add an optimized version of tmBind by @JasonGross in #926
• Revert "CI:Add concurrency and cancel-in-progress:true" by @JasonGross in #929
• Add example for #926 to test-suite by @JasonGross in #927
• Add Trel_sig by @JasonGross in #931
• remove one hypothesis in erase_correct_strong by @tabareau in #911
• Adjust naming of optimized template monad by @JasonGross in #928
• Add conv_pb_leqb by @JasonGross in #932
• Fix update-_PluginProject.in target by @JasonGross in #934
• Rename level and var by @tabareau in #935
• Take 2: Revert "Revert "CI:Add concurrency and cancel-in-progress:true"" by @JasonGross in #937
• Add _dep versions of Forall2, All2, etc by @JasonGross in #930
• Fix tmOptimizedBind to avoid quadratic blowup by @JasonGross in #936
• [Quotation.ToTemplate] Add quote_{All,Forall}2_dep by @JasonGross in #938
• Typed Erasure depends on TemplatePCUIC by @JasonGross in #941
• Add support for dependency in cumulSpec0_ind_all by @JasonGross in #933
• Parameterize reduction in PCUIC quotation with a typeclass by @JasonGross in #939
• [Quotation] Swap ordering in quotation for performance by @JasonGross in #942
• Update _PluginProject by @JasonGross in #943
• [Quotation] Add quotation for some Equations defs by @JasonGross in #944
• Gallina Quotation for PCUIC terms and typing by @JasonGross in #940
• Update README and create Quotation README by @JasonGross in #945
• Change notation for wcbv eval by @yforster in #946
• prove canonicity by @tabareau in #947
• consistency makes use of canonicity by @tabareau in #948

New Contributors

• @JasonGross made their first contribution in #774
• @4ever2 made their first contribution in #868

Full Changelog: v1.1.1-8.16...v1.2-8.17