Merge pull request #95 from CertiCoq/coq8.19

Coq 8.19 compatibility

Author: mattam82

.github/workflows/build.yml

@@ -19,7 +19,7 @@ jobs:
         opam_file:
           - 'coq-certicoq.opam'
         image:
-          - 'yforster/coq:8.17.0--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3--elpi.1.17.1-metacoq-v1.3-8.17'
+          - 'yforster/coq:8.19.1--clang-11--compcert-3.13.1--extlib-0.12.1--equations-1.3--metacoq-1.3.1'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v3
@@ -51,6 +51,6 @@ jobs:
               make -C ~/repo/benchmarks all
             endGroup
             startGroup "Test bootstrapped plugins"
-              cd repo && ./configure.sh global
+              cd ~/repo && ./configure.sh global
               make -C ~/repo/bootstrap test
             endGroup

.gitignore

@@ -137,3 +137,5 @@ bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
 bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.h
 bootstrap/certicoqc/tests/test.demo1.c
 bootstrap/certicoqc/tests/test.demo1.h
+plugin/.filestoinstall
+cplugin/.merlin

benchmarks/certicoq_eval.v

@@ -1,7 +1,7 @@
 From Equations Require Import Equations.
 From Coq Require Import Uint63 Wf_nat ZArith Lia Arith.
 From CertiCoq Require Import CertiCoq.
-
+CertiCoq -help.
 Set CertiCoq Build Directory "_build".
 
 (* This warns about uses of primitive operations, but we compile them fine *)
@@ -13,8 +13,8 @@ Program Definition long_vector n : Vector.t nat n :=
   Vector.of_list (List.repeat 1000 n).
   Next Obligation. now rewrite List.repeat_length. Qed.
 
-Definition silent_long_vector := 0.
- (* Vector.eqb _ Nat.eqb (long_vector 5000) (long_vector 5000). *)
+Definition silent_long_vector :=
+ Vector.eqb _ Nat.eqb (long_vector 5000) (long_vector 5000).
 
 (* Time Eval vm_compute in silent_long_vector. (* Blows up *) *)
 (* 1.23s *)
@@ -68,7 +68,7 @@ CertiCoq Eval -time sha_fast_noproofs.
 (* Executed in 0.037175 sec *)
 
 Time CertiCoq Eval sha_fast_noproofs.
-(* Finished transaction in 0.06 sec *)
+(* Finished transaction in 0.02 sec *)
 
 CertiCoq Eval -time sha_fast_noproofs.
 (* Executed in 0.045 sec *)
@@ -106,9 +106,9 @@ Definition vs_hard :=
 (* Blows up *) Time Eval vm_compute in vs_hard.
 *)
 
-(* CertiCoq Eval -time vs_hard. *)
+CertiCoq Eval -time vs_hard.
 (* Executed in 0.06s *)
-(* CertiCoq Eval -time vs_hard. *)
+CertiCoq Eval -time vs_hard.
 
 (* CertiCoq Eval -time vs_easy. *)
 (* Executed in 0.007s *)

benchmarks/lib/Binom.v

@@ -1,6 +1,4 @@
-Require Import Coq.Arith.Arith
-               Coq.Numbers.Natural.Peano.NPeano
-               List.
+Require Import Coq.Arith.Arith List.
 
 Import ListNotations.
 Import Nat. (* For 8.5.0 *)

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.17.0
+## GNUMakefile for Coq 8.19.1
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -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.17.0
+COQMAKEFILE_VERSION:=8.19.1
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -293,18 +293,26 @@ CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
 CAMLFLAGS+=$(OCAMLWARN)
 
 ifneq (,$(TIMING))
-TIMING_ARG=-time
-ifeq (after,$(TIMING))
-TIMING_EXT=after-timing
+  ifeq (after,$(TIMING))
+    TIMING_EXT=after-timing
+  else
+    ifeq (before,$(TIMING))
+      TIMING_EXT=before-timing
+    else
+      TIMING_EXT=timing
+    endif
+  endif
+  TIMING_ARG=-time-file $<.$(TIMING_EXT)
 else
-ifeq (before,$(TIMING))
-TIMING_EXT=before-timing
-else
-TIMING_EXT=timing
-endif
+  TIMING_ARG=
 endif
+
+ifneq (,$(PROFILING))
+  PROFILE_ARG=-profile $<.prof.json
+  PROFILE_ZIP=gzip $<.prof.json
 else
-TIMING_ARG=
+  PROFILE_ARG=
+  PROFILE_ZIP=true
 endif
 
 # Files #######################################################################
@@ -592,13 +600,24 @@ beautify: $(BEAUTYFILES)
 # There rules can be extended in Makefile.local
 # Extensions can't assume when they run.
 
+# We use $(file) to avoid generating a very long command string to pass to the shell
+# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux)
+# However Apple ships old make which doesn't have $(file) so we need a fallback
+$(file >.hasfile,1)
+HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi)
+
+MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\
+  $(shell rm -f .filestoinstall) \
+  $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall)))
+
 # findlib needs the package to not be installed, so we remove it before
 # installing it (see the call to findlib_remove)
 install: META
-	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+	@$(MKFILESTOINSTALL)
+	$(HIDE)code=0; for f in $$(cat .filestoinstall); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
 	done; exit $$code
-	$(HIDE)for f in $(FILESTOINSTALL); do\
+	$(HIDE)for f in $$(cat .filestoinstall); do\
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
 	 if [ "$$?" != "0" -o -z "$$df" ]; then\
 	   echo SKIP "$$f" since it has no logical path;\
@@ -611,6 +630,7 @@ install: META
 	$(call findlib_remove)
 	$(call findlib_install, META $(FINDLIBFILESTOINSTALL))
 	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
+	@rm -f .filestoinstall
 install-extra::
 	@# Extension point
 .PHONY: install install-extra
@@ -642,18 +662,20 @@ install-doc:: html mlihtml
 
 uninstall::
 	@# Extension point
+	@$(MKFILESTOINSTALL)
 	$(call findlib_remove)
-	$(HIDE)for f in $(FILESTOINSTALL); do \
+	$(HIDE)for f in $$(cat .filestoinstall); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf" ;\
 	done
-	$(HIDE)for f in $(FILESTOINSTALL); do \
+	$(HIDE)for f in $$(cat .filestoinstall); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\
 	 (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
 	done
+	@rm -f .filestoinstall
 
 .PHONY: uninstall
 
@@ -784,12 +806,6 @@ $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix
 	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
 		-shared -o $@ $<
 
-ifneq (,$(TIMING))
-TIMING_EXTRA = > $<.$(TIMING_EXT)
-else
-TIMING_EXTRA =
-endif
-
 # can't make
 # https://www.gnu.org/software/make/manual/make.html#Static-Pattern
 # work with multiple target rules
@@ -800,20 +816,22 @@ 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)
+  $(1).vo $(1).glob &: $(1).v | $$(VDFILE)
+	$$(SHOW)COQC $(1).v
+	$$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
+	$$(HIDE)$$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
-	$(SHOW)COQNATIVE $(1).vo
-	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
+	$$(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)
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
 	$(HIDE)$(call TIMER,[email protected]) $(COQNATIVE) $(COQLIBS) $@

bootstrap/certicoqc/Makefile

@@ -2,7 +2,15 @@
 CCOMPILER := $(shell { command -v clang-11 || command -v clang || command -v gcc; } 2>/dev/null)
 # clang options
 CCOMPILEROPTS = -fPIC -fomit-frame-pointer -g -c -I . -I $(RUNTIME_DIR) -I ${OCAMLLIB} -w -Wno-everything -O2
+UNAME=$(shell uname -s)
+ifeq '$(UNAME)' 'Darwin'
+  SED= $(shell which gsed)
+  ifeq '$(SED)' ''
+   $(error "Must have gsed installed on MacOS, try e.g. brew install gsed")
+  endif
+else
 SED=`which gsed || which sed`
+endif
 
 # CompCert compiler
 CCOMPCOMPILER := $(CCOMPILER)
@@ -35,8 +43,12 @@ ifeq '$(CERTICOQ_CONFIG)' 'local'
 
   TESTCOQOPTS = $(COQOPTS)
 else
+ ifeq '$(CERTICOQ_CONFIG)' 'global'
   COQOPTS = -I . -Q theories CertiCoq.CertiCoqC
   TESTCOQOPTS = 
+ else
+  $(error "Must first set CERTICOQ_CONFIG by running ./configure.sh")
+ endif
 endif
 
 PKGS = -package 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
@@ -127,4 +139,4 @@ install: theories/compile.vo certicoqc_plugin.cmxs
 
 .PHONY: plugin test
 
-.NOTPARALLEL:
+.NOTPARALLEL:

coq-certicoq.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev+8.17"
+version: "dev+8.19"
 maintainer: "The CertiCoq Team"
 homepage: "https://certicoq.org/"
 dev-repo: "git+https://github.com/CertiCoq/certicoq"
@@ -33,12 +33,12 @@ depends: [
   "ocaml"
   "conf-clang"
   "stdlib-shims"
-  "coq" {>= "8.17" & < "8.18~"}
-  "coq-compcert" {= "3.12"}
-  "coq-equations" {= "1.3+8.17"}
-  "coq-metacoq-erasure-plugin" {= "8.17.dev"}
-  "coq-metacoq-safechecker-plugin" {= "8.17.dev"}
-  "coq-ext-lib" {>= "0.11.8"}
+  "coq" {>= "8.19" & < "8.20~"}
+  "coq-compcert" {= "3.13.1"}
+  "coq-equations" {= "1.3+8.19"}
+  "coq-metacoq-erasure-plugin" {= "1.3.1+8.19"}
+  "coq-metacoq-safechecker-plugin" {= "1.3.1+8.19"}
+  "coq-ext-lib" {>= "0.12"}
 ]
 
 synopsis: "A Verified Compiler for Gallina, Written in Gallina "

cplugin/CoqMsgFFI.v

@@ -11,4 +11,4 @@ CertiCoq Register [
   coq_msg_notice => "coq_msg_notice",
   coq_msg_debug => "coq_msg_debug",
   coq_user_error => "coq_user_error" ]
-Include [ "coq_c_ffi.h" "coq_ffi.h" as library ].
+Include [ Library "coq_c_ffi.h" "coq_ffi.h" ].

cplugin/Makefile.local

@@ -7,12 +7,13 @@ CAMLFLAGS+=-w -32 # Unused values
 CAMLFLAGS+=-w -39 # Unused rec flagss
 CAMLFLAGS+=-w -20 # Unused arguments
 CAMLFLAGS+=-w -60 # Unused functor arguments
-CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims
+CAMLPKGS += -package coq-metacoq-template-ocaml.plugin,stdlib-shims
 
 CC=$(shell which gcc || which clang-11)
 
 merlin-hook::
-		$(HIDE)echo 'FLG $(OPENS)' >> .merlin
+		$(HIDE)echo 'PKG coq-metacoq-template-ocaml.plugin' >> .merlin
+		$(HIDE)echo 'PKG stdlib-shims' >> .merlin
 
 get_ordinal.o: get_ordinal.c
 	$(CC) -c -o $@ -I runtime $<

cplugin/PrimFloats.v

@@ -20,4 +20,4 @@ CertiCoq Register [
   Coq.Floats.PrimFloat.of_uint63 => "prim_float_of_uint63" with tinfo,
   Coq.Floats.PrimFloat.next_up => "prim_float_next_up" with tinfo,
   Coq.Floats.PrimFloat.next_down => "prim_float_next_down" with tinfo ]
-Include [ "prim_floats.h" as library ].
+Include [ Library "prim_floats.h" ].

cplugin/PrimInt63.v

@@ -27,4 +27,4 @@ CertiCoq Register [
   Coq.Numbers.Cyclic.Int63.PrimInt63.lor => "prim_int63_lor", 
   Coq.Numbers.Cyclic.Int63.PrimInt63.lxor => "prim_int63_lxor"
 ]
-Include [ "prim_int63.h" as library ].
+Include [ Library "prim_int63.h" ].