Merge remote-tracking branch 'origin/coq-8.17' into master-8.17

.github/workflows/build.yml

@@ -4,7 +4,7 @@ on:
   push:
     branches:
       - master
-      - coq-8.16
+      - coq-8.17
   pull_request:
     branches:
       - "**"
@@ -19,7 +19,7 @@ jobs:
         opam_file:
           - 'coq-certicoq.opam'
         image:
-          - 'yforster/coq:8.16.1--clang-11--compcert-3.11--extlib-0.11.8--equations-1.3--elpi.1.16'
+          - 'mattam82/coq:8.17--ocaml-4.13.1--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v2
@@ -36,6 +36,9 @@ jobs:
             startGroup "Copy repo (for later benchmarking)"
               cp -r `pwd` ~/repo
             endGroup
+            startGroup "opam pin"
+              opam pin -y submodules/metacoq
+            endGroup
           after_script: |
             startGroup "List installed packages"
               opam list

benchmarks/lib/Makefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.16.1
+## GNUMakefile for Coq 8.17.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -76,7 +76,7 @@ VERBOSE ?=
 TIMED?=
 TIMECMD?=
 # Use command time on linux, gtime on Mac OS
-TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMEFMT?="$(if $(findstring undefined, $(flavor 1)),$@,$(1)) (real: %e, user: %U, sys: %S, mem: %M ko)"
 ifneq (,$(TIMED))
 ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=command time -f $(TIMEFMT)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.16.1
+COQMAKEFILE_VERSION:=8.17.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -677,12 +677,14 @@ clean::
 	$(HIDE)rm -f $(CMOFILES)
 	$(HIDE)rm -f $(CMIFILES)
 	$(HIDE)rm -f $(CMAFILES)
-	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
+	$(HIDE)rm -f $(CMXFILES)
 	$(HIDE)rm -f $(CMXAFILES)
 	$(HIDE)rm -f $(CMXSFILES)
-	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
+	$(HIDE)rm -f $(OFILES)
 	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
 	$(HIDE)rm -f $(MLGFILES:.mlg=.ml)
+	$(HIDE)rm -f $(CMXFILES:.cmx=.cmt)
+	$(HIDE)rm -f $(MLIFILES:.mli=.cmti)
 	$(HIDE)rm -f $(ALLDFILES)
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
@@ -788,17 +790,43 @@ else
 TIMING_EXTRA =
 endif
 
+# can't make
+# https://www.gnu.org/software/make/manual/make.html#Static-Pattern
+# work with multiple target rules
+# so use eval in a loop instead
+# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets
+# if available (GNU Make >= 4.3)
+ifneq (,$(filter grouped-target,$(.FEATURES)))
+define globvorule=
+
+# take care to $$ variables using $< etc
+  $(1).vo $(1).glob &: $(1).v | $(VDFILE)
+	$(SHOW)COQC $(1).v
+	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v $$(TIMING_EXTRA)
+ifeq ($(COQDONATIVE), "yes")
+	$(SHOW)COQNATIVE $(1).vo
+	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
+endif
+
+endef
+else
+
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
 	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
-	$(HIDE)$(COQNATIVE) $(COQLIBS) $@
+	$(HIDE)$(call TIMER,[email protected]) $(COQNATIVE) $(COQLIBS) $@
 endif
 
-# FIXME ?merge with .vo / .vio ?
+# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets
 $(GLOBFILES): %.glob: %.v
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)'COQC $< (for .glob)'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+endif
+
+$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile))))
 
 $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -vio $<

benchmarks/lib/_CoqProject

@@ -1,4 +1,6 @@
 -R ./ CertiCoq.Benchmarks.lib
+-arg -w -arg -deprecated
+
 Binom.v
 Color.v
 vs.v

benchmarks/metacoq_erasure/Loader.v

@@ -1,2 +1,4 @@
 From MetaCoq Require Import ExtractableLoader.
+From CertiCoq Require Export CertiCoqVanilla. (* We reuse the ML certicoq plugin to parse options and print Clight code *)
+(* Using Export to get the primitives registrations the *)
 Declare ML Module "coq-certicoq-bootstrapped-erasure.plugin".

benchmarks/metacoq_erasure/Makefile

@@ -1,10 +1,10 @@
-PKGS = -package coq-metacoq-template-ocaml,coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac
+PKGS = -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-certicoqc
 LINKOPTS = -linkpkg -dontlink str,unix,dynlink,threads,zarith
-OCAMLOPTS = -I ../../_opam/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8
+OCAMLOPTS = -open Metacoq_template_plugin -I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8
 GENCFILES = glue.CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.metacoq_erasure.c \
 		CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.metacoq_erasure.c
 CFILES = certicoq_erasure.c ${GENCFILES} gc_stack.c print.c
-COPTS = -I ../../_opam/lib/ocaml -I . -I ../../theories/Runtime
+COPTS = -g -I ../../_opam/lib/ocaml -I . -I ../../theories/Runtime
 # ffi.CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.QuoteFFI.c
 COQOPTS = -Q ../../theories/Codegen CertiCoq.Codegen -Q ../../libraries CertiCoq.Libraries \
 	-Q ../../theories/LambdaANF CertiCoq.LambdaANF -Q ../../theories/LambdaBoxLocal CertiCoq.LambdaBoxLocal \
@@ -27,7 +27,7 @@ clean:
 Loader.vo: Loader.v install
 	coqc -I . -Q . CertiCoq.Benchmarks.metacoq_erasure Loader.v
 
-metacoq_erasure.vo ${GENCFILES} &: metacoq_erasure.v
+metacoq_erasure.vo: metacoq_erasure.v
 	coqc ${COQOPTS} $<
 
 %.o: %.c
@@ -51,15 +51,11 @@ g_safe_erasure.ml: g_safe_erasure.mlg certiCoqErase.cmx
 %.cmi: %.mli
 	ocamlfind opt ${PKGS} ${OCAMLOPTS} -for-pack Certicoq_erasure_plugin $<
 
-%.cmx: %.ml
+%.cmx: %.ml %.cmi
 	ocamlfind opt -c ${PKGS} ${OCAMLOPTS} -for-pack Certicoq_erasure_plugin $<
 
 install: certicoq_erasure_plugin.cmxa certicoq_erasure_plugin.cmxs certicoq_erasure_plugin.cmx
 	ocamlfind remove coq-certicoq-bootstrapped-erasure
 	ocamlfind install coq-certicoq-bootstrapped-erasure META $+
 
-install: certicoq_erasure_plugin.cmxa certicoq_erasure_plugin.cmxs certicoq_erasure_plugin.cmx
-	ocamlfind remove coq-certicoq-bootstrapped-erasure
-	ocamlfind install coq-certicoq-bootstrapped-erasure META $+
-
-.PHONY: plugin test
+.PHONY: plugin test

benchmarks/metacoq_erasure/certiCoqErase.ml

@@ -134,6 +134,6 @@ let fix_quoted_program (p : Ast0.Env.program) =
 
 let erase ~bypass env evm c =
   debug (fun () -> str"Quoting");
-  let prog = time (str"Quoting") (quote_term_rec ~bypass ~with_universes:false env) (EConstr.to_constr evm c) in
+  let prog = time (str"Quoting") (quote_term_rec ~bypass ~with_universes:false env) evm (EConstr.to_constr evm c) in
   let prog = fix_quoted_program prog in
   time (str"Erasure") certicoq_erase prog

benchmarks/metacoq_erasure/metacoq_erasure.v

@@ -36,7 +36,7 @@ CertiCoq Compile -time -O 1 metacoq_erasure
 Extract Constants [
   (* coq_msg_debug => "print_msg_debug", *)
   coq_msg_info => "coq_msg_info",
-  PCUICWfEnvImpl.guard_impl => "metacoq_guard_impl" ] 
+  PCUICWfEnvImpl.guard_impl => "metacoq_guard_impl" ]
 Include [ "print.h" ].
 
 (*
@@ -51,4 +51,4 @@ Extract Constants [
   PCUICTyping.guard_checking => "print_msg_info",
   coq_msg_info => "print_msg_info"
    ] 
-Include [ "print.h" ].*)
+Include [ "print.h" ].*)

bootstrap/certicoqc/g_certicoqc.mli

@@ -1 +1 @@
-val __coq_plugin_name : string
+(* val __coq_plugin_name : string *)

bootstrap/certicoqc/test.v

@@ -1,6 +1,7 @@
 From MetaCoq.Template Require Import All.
 From MetaCoq.Utils Require Import bytestring.
 From MetaCoq.Common Require Import Primitive.
+
 From Coq Require Import PrimFloat PrimInt63.
 From CertiCoq.CertiCoqC Require Import CertiCoqC.
 
@@ -25,7 +26,9 @@ Definition string_of_bool b :=
 #[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int.
 #[export] Instance Z_show : Show BinNums.Z := string_of_Z.
 Require Import ZArith.
-
+
+From MetaCoq.ErasurePlugin Require Import Loader.
+Fail From CertiCoq.CertiCoqC Require Import compile.
 From CertiCoq.CertiCoqC Require Import compile.
 From CertiCoq.Common Require Import Pipeline_utils.
 

bootstrap/certicoqchk/certicoqchk.ml

@@ -23,7 +23,7 @@ let quote gr =
   let sigma, c = Evd.fresh_global env sigma gr in
   debug_msg debug "Quoting";
   let time = Unix.gettimeofday() in
-  let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass:true env (EConstr.to_constr sigma c) in
+  let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass:true env sigma (EConstr.to_constr sigma c) in
   let time = (Unix.gettimeofday() -. time) in
   debug_msg debug (Printf.sprintf "Finished quoting in %f s.. checking." time);
   term
@@ -34,4 +34,4 @@ let check gr =
   let b = Certicoqchk_plugin_wrapper.check (Obj.magic p) (* Go through a type equality *) in
   match b with
   | Datatypes.Coq_true -> () 
-  | Datatypes.Coq_false -> CErrors.user_err Pp.(str"The program does not typecheck")
+  | Datatypes.Coq_false -> CErrors.user_err Pp.(str"The program does not typecheck")

bootstrap/certicoqchk/compile.v

@@ -21,18 +21,17 @@ From MetaCoq.ErasurePlugin Require Import Erasure.
 
 #[local,program] Instance assume_normalization {nor} : @PCUICSN.Normalization config.default_checker_flags nor.
 Next Obligation. todo "we should write a Template Monad program to prove normalization for the particular program being inferred, rather than axiomatizing it". Qed.
-
 #[local] Existing Instance PCUICSN.normalization.
 
-Program Definition infer_and_pretty_print_template_program (cf := config.default_checker_flags)
-  {nor : PCUICSN.normalizing_flags} {guard : abstract_guard_impl}
+Program Definition infer_and_pretty_print_template_program (cf := config.default_checker_flags) {guard : abstract_guard_impl}
+  {nor : normalizing_flags}
   (p : Ast.Env.program) φ
   : string + string :=
-  match infer_template_program (normalization_in := _) (cf:=cf) p φ return string + string with
+  let e' := PCUICProgram.trans_env_env (TemplateToPCUIC.trans_global_env p.1) in
+  match infer_template_program (cf:=cf) p φ return string + string with
   | CorrectDecl t =>
-    let e' := PCUICProgram.trans_env_env (TemplateToPCUIC.trans_global_env p.1) in
-    inl ("Environment is well-formed and " ^ Pretty.print_term (empty_ext p.1) [] true p.2 ^
-         " has type: " ^ print_term (PCUICAst.PCUICEnvironment.empty_ext e') []  t.π1)
+    inl ("Environment is well-formed and " ^ Pretty.print_term (empty_ext p.1) [] false p.2 ^
+         " has type: " ^ print_term (PCUICAst.PCUICEnvironment.empty_ext e') [] t.π1)
   | EnvError Σ (AlreadyDeclared id) =>
     inr ("Already declared: " ^ id)
   | EnvError Σ (IllFormedDecl id e) =>

bootstrap/certicoqchk/g_certicoqchk.mli

@@ -1 +1 @@
-val __coq_plugin_name : string
+(* val __coq_plugin_name : string *)

coq-certicoq.opam

@@ -31,11 +31,12 @@ install: [
 depends: [
   "ocaml"
   "stdlib-shims"
-  "coq" {>= "8.16" & < "8.17~"}
-  "coq-compcert" {= "3.11"}
-  "coq-equations" {= "1.3+8.16"}
-  # "coq-metacoq-erasure-plugin" {>= "1.2+8.17"} Temporarily disable as we rely on the submodule
-  "coq-ext-lib" {>= "0.11.5"}
+  "coq" {>= "8.17" & < "8.18~"}
+  "coq-compcert" {= "3.12"}
+  "coq-equations" {= "1.3+8.17"}
+  # "coq-metacoq-erasure-plugin" {>= "1.2+8.17"} Temporarily removed as we rely on the submodule
+  # "coq-metacoq-safechecker-plugin" {>= "1.2+8.17"}
+  "coq-ext-lib" {>= "0.11.8"}
 ]
 
 synopsis: "A Verified Compiler for Gallina, Written in Gallina "

cplugin/_CoqProject

@@ -59,8 +59,6 @@ extraction/envMap.mli
 extraction/envMap.ml
 extraction/pCUICWfEnv.mli
 extraction/pCUICWfEnv.ml
-# extraction/pCUICWfUniverses.mli
-# extraction/pCUICWfUniverses.ml
 extraction/pCUICWfEnvImpl.mli
 extraction/pCUICWfEnvImpl.ml
 extraction/typing0.mli
@@ -357,8 +355,6 @@ extraction/pCUICErrors.ml
 extraction/pCUICErrors.mli
 extraction/pCUICExpandLets.ml
 extraction/pCUICExpandLets.mli
-# extraction/pCUICEquality.mli
-# extraction/pCUICEquality.ml
 extraction/pCUICEqualityDec.mli
 extraction/pCUICEqualityDec.ml
 extraction/pCUICNormal.ml
@@ -450,8 +446,8 @@ extraction/uncurry_proto.ml
 extraction/uncurry_proto.mli
 extraction/universes0.ml
 extraction/universes0.mli
-extraction/values.ml
-extraction/values.mli
+extraction/values0.ml
+extraction/values0.mli
 extraction/wGraph.ml
 extraction/wGraph.mli
 extraction/zArith_dec.ml
@@ -462,3 +458,5 @@ extraction/zbool.ml
 extraction/zbool.mli
 extraction/zpower.ml
 extraction/zpower.mli
+extraction/optionMonad.mli
+extraction/optionMonad.ml

cplugin/certicoq.ml

@@ -297,7 +297,7 @@ let quote opts gr =
   let sigma, c = Evd.fresh_global env sigma gr in
   debug_msg debug "Quoting";
   let time = Unix.gettimeofday() in
-  let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass:false env (EConstr.to_constr sigma c) in
+  let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass:false env sigma (EConstr.to_constr sigma c) in
   let time = (Unix.gettimeofday() -. time) in
   debug_msg debug (Printf.sprintf "Finished quoting in %f s.." time);
   Obj.magic term
@@ -499,6 +499,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
     let term = quote opts gr in
     let debug = opts.debug in
     let options = make_pipeline_options opts in
+    let term = FixRepr.fix_quoted_program term in
     let p = Pipeline.show_IR options (Obj.magic term) in
     match p with
     | (CompM.Ret prg, dbg) ->
@@ -532,7 +533,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
         (Printer.pr_global gr ++ str " is not an inductive type") in
     debug_msg debug "Quoting";
     let time = Unix.gettimeofday() in
-    let term = quote_term_rec ~bypass:true env (EConstr.to_constr sigma c) in
+    let term = quote_term_rec ~bypass:true env sigma (EConstr.to_constr sigma c) in
     let time = (Unix.gettimeofday() -. time) in
     debug_msg debug (Printf.sprintf "Finished quoting in %f s.." time);
     (term, name)
@@ -570,4 +571,4 @@ module CompileFunctor (CI : CompilerInterface) = struct
 end
 
 module MLCompile = CompileFunctor (MLCompiler)
-include MLCompile
+include MLCompile

cplugin/certicoq_vanilla_plugin.mlpack

@@ -230,7 +230,7 @@ Zbits
 Integers
 Floats
 AST
-Values
+Values0
 LambdaBoxMut_to_LambdaBoxMut_eta
 LambdaBoxMut_to_LambdaBoxLocal
 Camlcoq

cplugin/static/printCsyntax.ml

@@ -18,7 +18,7 @@
 
 open Format
 open Camlcoq
-open Values
+open Values0
 open AST
 open! Ctypes
 open Cop
@@ -183,7 +183,7 @@ let rec precedence = function
 (* Expressions *)
 
 let print_pointer_hook
-   : (formatter -> Values.block * Integers.Int.int -> unit) ref
+   : (formatter -> Values0.block * Integers.Int.int -> unit) ref
    = ref (fun p (b, ofs) -> ())
 
 let is_nan (f : float) = f <> f