Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12

Author: yforster

.gitignore

@@ -412,3 +412,9 @@ erasure/src/signature.ml
 erasure/src/signature.mli
 erasure/src/eOptimizePropDiscr.ml
 erasure/src/eOptimizePropDiscr.mli
+erasure/src/pCUICErrors.ml
+erasure/src/pCUICErrors.mli
+erasure/src/pCUICTypeChecker.ml
+erasure/src/pCUICTypeChecker.mli
+erasure/src/pCUICPrimitive.ml
+erasure/src/pCUICPrimitive.mli

INSTALL.md

@@ -25,7 +25,6 @@ MetaCoq is split into multiple packages that get all installed using the
 `coq-metacoq` meta-package:
 
  - `coq-metacoq-template` for the Template Monad and quoting plugin
- - `coq-metacoq-checker` for the UNverified checker of template-coq terms
  - `coq-metacoq-pcuic` for the PCUIC development and proof of the
    Template-Coq -> PCUIC translation
  - `coq-metacoq-safechecker` for the verified checker on PCUIC terms
@@ -103,7 +102,7 @@ the sources directory.
 
 Then use:
 
-- `make` to compile the `template-coq` plugin, the `checker`, the `pcuic`
+- `make` to compile the `template-coq` plugin, the `pcuic`
   development and the `safechecker` and `erasure` plugins.
   You can also selectively build each target.
 

Makefile

@@ -1,20 +1,18 @@
 TIMED ?=
 
-all: template-coq checker pcuic safechecker erasure examples
+all: template-coq pcuic safechecker erasure examples
 
-.PHONY: all template-coq checker pcuic erasure install html clean mrproper .merlin test-suite translations
+.PHONY: all template-coq pcuic erasure install html clean mrproper .merlin test-suite translations
 
 install: all
 	$(MAKE) -C template-coq install
-	$(MAKE) -C checker install
 	$(MAKE) -C pcuic install
 	$(MAKE) -C safechecker install
 	$(MAKE) -C erasure install
 	$(MAKE) -C translations install
 
 uninstall: all
 	$(MAKE) -C template-coq uninstall
-	$(MAKE) -C checker uninstall
 	$(MAKE) -C pcuic uninstall
 	$(MAKE) -C safechecker uninstall
 	$(MAKE) -C erasure uninstall
@@ -23,7 +21,6 @@ uninstall: all
 html: all
 	"coqdoc" -toc -utf8 -interpolate -l -html \
 		-R template-coq/theories MetaCoq.Template \
-		-R checker/theories MetaCoq.Checker \
 		-R pcuic/theories MetaCoq.PCUIC \
 		-R safechecker/theories MetaCoq.SafeChecker \
 		-R erasure/theories MetaCoq.Erasure \
@@ -32,7 +29,6 @@ html: all
 
 clean:
 	$(MAKE) -C template-coq clean
-	$(MAKE) -C checker clean
 	$(MAKE) -C pcuic clean
 	$(MAKE) -C safechecker clean
 	$(MAKE) -C erasure clean
@@ -45,7 +41,6 @@ mrproper:
 	$(MAKE) -C pcuic mrproper
 	$(MAKE) -C safechecker mrproper
 	$(MAKE) -C erasure mrproper
-	$(MAKE) -C checker mrproper
 	$(MAKE) -C examples mrproper
 	$(MAKE) -C test-suite mrproper
 	$(MAKE) -C translations mrproper
@@ -55,7 +50,6 @@ mrproper:
 	$(MAKE) -C pcuic .merlin
 	$(MAKE) -C safechecker .merlin
 	$(MAKE) -C erasure .merlin
-	$(MAKE) -C checker .merlin
 
 template-coq:
 	$(MAKE) -C template-coq
@@ -69,28 +63,23 @@ safechecker: template-coq pcuic
 erasure: template-coq safechecker pcuic
 	$(MAKE) -C erasure
 
-checker: template-coq
-	$(MAKE) -C checker
-
-examples: checker safechecker
+examples: checker safechecker erasure
 	$(MAKE) -C examples
 
-test-suite: template-coq checker safechecker erasure
+test-suite: template-coq safechecker erasure
 	$(MAKE) -C test-suite
 
-translations: template-coq checker
+translations: template-coq
 	$(MAKE) -C translations
 
 cleanplugins:
 	$(MAKE) -C template-coq cleanplugin
-	$(MAKE) -C pcuic cleanplugin
-	$(MAKE) -C checker cleanplugin
 	$(MAKE) -C safechecker cleanplugin
 	$(MAKE) -C erasure cleanplugin
 
 ci-local:
 	./configure.sh local
-	$(MAKE) all test-suite TIMED=pretty-timed
+	$(MAKE) all test-suite
 
 ci-opam:
 	# Use -v so that regular output is produced

README.md

@@ -68,20 +68,13 @@ In addition to this representation of terms, Template Coq includes:
   checker, and inserting them in the global environment, in
   the style of MTac.
 
+- A formalisation of the expected typing rules reflecting the ones of Coq
 
-### [Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.12/checker)
-
-A partial type-checker for the Calculus of Inductive Constructions,
-whose extraction to ML is runnable as a plugin (using command `MetaCoq
-Check foo`). This checker uses _fuel_, so it must be passed a number
-of maximal reduction steps to perform when calling conversion, and is
-NOT verified.
-
-### [PCUIC](https://github.com/MetaCoq/metacoq/tree/coq-8.12/pcuic)
+### [PCUIC](https://github.com/MetaCoq/metacoq/tree/coq-8.11/pcuic)
 
 PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is
 a cleaned up version of the term language of Coq and its associated
-type system, equivalent to the one of Coq. This version of the
+type system, shown equivalent to the one of Coq. This version of the
 calculus has proofs of standard metatheoretical results:
 
 - Weakening for global declarations, weakening and substitution for

TODO.md

@@ -29,11 +29,16 @@
 
 - Clean `Derive`s: always derive `Siganture`, `NoConf`, ... directly after the
   definition of the inductive. (To avoid doing it several times.)
+  (Mostly done)
+  
+- Finish the PCUICSigmaCalculus proofs.
 
-- Remove `Program` from everywhere.
-
-
+# Medium Projects
 
+- Change Template-PCUIC translations to translate casts to applications of 
+  identity functions (vm_cast, default_cast etc) to make the back and forth
+  the identity and derive weakening/substitution/etc.. from the PCUIC theorems.
+  Is that really better than identity functions?
 # Big projects
 
 - Refine the longest-simple-path algorithm on universes with the 
@@ -49,6 +54,9 @@
   be definable. Probably not very useful though because if the elimination is 
   restricted then it means some Type is in the constructor and won't be projectable.
 
+- Verify the substitution calculus of P.M Pédrot using skewed lists at
+  https://github.com/coq/coq/pull/13537 and try to use it to implement efficient explicit 
+  substitutions.
 
 ## Website