Merge pull request #93 from CertiCoq/metacoq-bump

Metacoq bump

.github/workflows/build.yml

@@ -9,7 +9,7 @@ on:
     branches:
       - "**"
   workflow_dispatch:
-    inputs:
+    inputs: {}
 
 jobs:
   build-matrix:
@@ -19,24 +19,23 @@ jobs:
         opam_file:
           - 'coq-certicoq.opam'
         image:
-          - 'mattam82/coq:8.17--ocaml-4.13.1--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3' # comment back in if MetaCoq commit changes
-          # - 'yforster/coq:8.17.0--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3--elpi.1.17.1-metacoq-8.17.dev.e0794e3'
+          - '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'
       fail-fast: false  # don't stop jobs if one fails
     steps:
-      - uses: actions/checkout@v2
-        with:
-          submodules: true
+      - uses: actions/checkout@v3
+        # with:
+        #   submodules: true
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}
           opam_file: ${{ matrix.opam_file }}
-          before_install: | # comment back in if MetaCoq commit changes
-            startGroup "fix permission issues"
-              sudo chown -R coq:coq .
-            endGroup
-            startGroup "opam pin"
-              opam pin -n -y submodules/metacoq
-            endGroup
+          # before_install: | # comment back in if MetaCoq commit changes
+          #   startGroup "fix permission issues"
+          #     sudo chown -R coq:coq .
+          #   endGroup
+          #   startGroup "opam pin"
+          #     opam pin -n -y submodules/metacoq
+          #   endGroup
           before_script: |
             startGroup "fix permission issues"
               sudo chown -R coq:coq .

.gitignore

@@ -131,4 +131,9 @@ bootstrap/certicoqchk/META
 bootstrap/certicoqc*/glue.c
 bootstrap/certicoqc*/glue.h
 plugin/.merlin
-_build
+_build
+.vscode/CertiCoq.code-workspace
+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

.vscode/launch.json

@@ -10,10 +10,7 @@
             "request": "launch",
             "name": "Debug",
             "program": "${workspaceFolder}/_opam/bin/coqc",
-            "args": [ "-I", ".", "-Q", "../../theories/Codegen", "CertiCoq.Codegen", "-Q", "../../libraries", "CertiCoq.Libraries", "-Q", "../../theories/LambdaANF",
-             "CertiCoq.LambdaANF", "-Q", "../../theories/LambdaBoxLocal", "CertiCoq.LambdaBoxLocal", "-Q", "../../theories/Compiler", "CertiCoq.Compiler", "-Q", "../../theories/common", "CertiCoq.Common",
-              "-Q", "../../theories/Glue", "CertiCoq.Glue", "-Q", "../../theories/LambdaBoxMut", "CertiCoq.LambdaBoxMut", "-Q", "../../plugin", "CertiCoq.Plugin", "-I", "../../plugin", "-Q",
-               "../../cplugin", "CertiCoq.VanillaPlugin", "-I", "../../cplugin", "-Q", "theories", "CertiCoq.CertiCoqC", "test.v"],
+            "args": [ "test.v"],
             "cwd": "${workspaceFolder}/bootstrap/certicoqc"
         },
         {

Makefile

@@ -2,8 +2,8 @@
 
 
 all theories/Extraction/extraction.vo: theories/Makefile libraries/Makefile
-	$(MAKE) -C libraries -j`nproc`
-	$(MAKE) -C theories -j`nproc`
+	$(MAKE) -C libraries -j1
+	$(MAKE) -C theories -j1
 
 theories/Makefile: theories/_CoqProject
 	cd theories;coq_makefile -f _CoqProject -o Makefile

benchmarks/test_primitive.v

@@ -4,6 +4,8 @@ From CertiCoq.Plugin Require Import CertiCoq.
 From Coq Require Import Uint63 ZArith.
 Open Scope bs.
 
+Set CertiCoq Build Directory "_build".
+
 Definition cst := coq_msg_info (Primitive.string_of_prim_int ((1 << 63))%uint63).
 Set Warnings "-primitive-turned-into-axiom".
 CertiCoq Run cst.
@@ -16,9 +18,13 @@ From MetaCoq.ErasurePlugin Require Import Loader.
 
 (* From MetaCoq.Erasure Require Import Loader. *)
 
-(* Definition testd := diveucl_21 9305446873517 1793572051078448654 4930380657631323783. *)
-(* Definition testmul := head0 3221225472. *)
-(* Eval compute in testmul. *)
+Definition testd := diveucl_21 9305446873517 1793572051078448654 4930380657631323783. 
+Definition testmul := head0 3221225472.
+Eval compute in testmul.
+
+(* MetaCoq Erase -time -typed testmul. *)
+
+CertiCoq Eval -time -debug -typed-erasure testmul.
 (* 
 Result: 549755813886, 0
 Calling prim_int63_eqb on 0 and 0: 1, 1 
@@ -27,7 +33,33 @@ Calling prim_int63_addmuldiv
 Calling addmuldiv with 1, 0 and 0: 0 *)
 (* Definition testd := diveucl_21 4 0 4611686018427387904. *)
 (* Eval compute in testd. *)
-Definition cst_big : BigN.t * BigN.t := BigN.div_eucl (2 ^ 129 + (2 ^ 39 - 2)) 3.
+Definition cst_small : BigN.t * BigN.t := BigN.div_eucl (6) 3.
+Time Eval vm_compute in cst_small.
+Time Eval compute in cst_small.
+CertiCoq Eval -time -typed-erasure -unsafe-erasure cst_small. (* Execution: 0.001s *)
+CertiCoq Show IR -time -typed-erasure -unsafe-erasure cst_small. (* Execution: 0.001s *)
+
+From Coq Require Import StreamMemo.
+
+CertiCoq Show IR -time -typed-erasure -unsafe-erasure memo_make. (* Execution: 0.001s *)
+
+Definition cst_big : bool := 
+  let x := BigN.div_eucl (2 ^ 129 + (2 ^ 39 - 2)) 3 in 
+  BigN.eqb (fst x) (fst x).
+
+Time Eval vm_compute in cst_big. (* 0s *)
+
+(*CertiCoq Eval -time -typed-erasure -unsafe-erasure cst_big.*) (* Execution: 0.001s, slow compilation *)
+(* CertiCoq Eval -time -unsafe-erasure cst_big. *)
+
+Definition cst_big2 : bool := 
+  let x := BigN.div_eucl (2 ^ 64500000 + (2 ^ 39 - 2)) 3 in 
+  BigN.eqb (fst x) (fst x).
+
+(*Time Eval vm_compute in cst_big2. (* 14 s *) *)
+(* Time CertiCoq Eval -debug -time -typed-erasure -unsafe-erasure cst_big2. *)
+ (* 69s *)
+
 Require Import Cyclic63.
 Open Scope uint63_scope.
 Definition test := (addmuldiv 32 3 5629499534213120)%uint63.
@@ -55,6 +87,6 @@ Definition string_of_primpair (x : int * int) :=
 Definition result := coq_msg_info (Primitive.string_of_prim_int test).
 (* Definition result := ("(" ++ Primitive.string_of_prim_int (fst cst_big) ++ ", " ++ *)
     (* Primitive.string_of_prim_int (snd cst_big) ++ ")")%bs. *)
-Time Eval native_compute in result.
+Time Eval vm_compute in result.
 
 CertiCoq Run result.

bootstrap/certicoqc/Makefile

@@ -1,4 +1,15 @@
-CCOMPILER := $(shell { command -v clang-11 || command -v clang; } 2>/dev/null)
+# clang compiler 
+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
+SED=`which gsed || which sed`
+
+# CompCert compiler
+CCOMPCOMPILER := $(CCOMPILER)
+# $(shell { command -v ccomp; } 2>/dev/null)
+# ccomp options
+CCOMPCOMPILEROPTS = $(CCOMPILEROPTS)
+# -g -c -I . -I $(RUNTIME_DIR) -I ${OCAMLLIB} -w -flongdouble -O2
 
 -include ../../Makefile.conf
 
@@ -34,69 +45,86 @@ COQLIBINSTALL = $(COQLIB)/user-contrib/CertiCoq/CertiCoqC
 OCAMLLIB = $(shell ocamlc -where)
 OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_plugin -package coq-certicoq-vanilla.plugin -open Certicoq_vanilla_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.c CertiCoq.CertiCoqC.compile.certicoqc.c
-CFILES = certicoqc_wrapper.c ${GENCFILES}
+GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
+CFILES = certicoqc_wrapper.c $(GENCFILES)
 
 RUNTIME_DIR = ../../plugin/runtime
-RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_c_ffi.o
+RUNTIME_FILES = $(RUNTIME_DIR)/gc_stack.o $(RUNTIME_DIR)/prim_floats.o $(RUNTIME_DIR)/prim_int63.o $(RUNTIME_DIR)/coq_c_ffi.o
 
 VFILES = theories/Loader.v theories/PrimInt63.v theories/PrimFloats.v theories/CertiCoqC.v
 
-CCOMPILEROPTS = -fPIC -g -c -I . -I ${RUNTIME_DIR} -I ${OCAMLLIB} -w -Wno-everything -O2
-# ccomp CCOMPOPTS = -g -c -I . -I ${OCAMLLIB} -Wno-int-conversion -O2
+.PHONY: runtime certicoqc
 
-.PHONY: certicoqc
+all: plugin
 
 plugin: theories/compile.vo certicoqc
 
+runtime: $(RUNTIME_FILES:.o=.c)
+	cd $(RUNTIME_DIR) && $(MAKE)
+
 Makefile.certicoqc: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.certicoqc
 
-certicoqc: Makefile.certicoqc certicoqc_plugin.cmxs
+certicoqc: runtime Makefile.certicoqc certicoqc_plugin.cmxs
 	$(MAKE) -f Makefile.certicoqc
 
 test: test.vo
 
 test.vo: test.v
 	mkdir -p tests
-	ulimit -Ss 65500 && coqc ${TESTCOQOPTS} test.v
+	ulimit -a
+	ulimit -H -a
+	ulimit -Ss 65500 && coqc $(TESTCOQOPTS) test.v
 
 clean: Makefile.certicoqc
 	make -f Makefile.certicoqc clean
-	rm *.cm* *.o *.vo
+	rm -f *.cm* *.o *.vo theories/*.vo
 
-theories/compile.vo ${GENCFILES} &: theories/compile.v
-	coqc ${COQOPTS} $<
+theories/CertiCoqC.vo: theories/CertiCoqC.v
+	coqc $(COQOPTS) $<
 
-%.o: %.c
-	$(CCOMPILER) $(CCOMPILEROPTS) -o $@ $<
+theories/compile.v: theories/CertiCoqC.vo
 
-certicoqc_plugin.cmxs: certicoqc_plugin.cmxa ${CFILES:.c=.o} ${RUNTIME_FILES}
-	ocamlfind ocamlopt ${OCAMLOPTS} -shared -o $@ $+
-
-certicoqc_plugin.cmx: certicoqc_plugin_wrapper.cmx certicoqc.cmx g_certicoqc.cmx
-	ocamlfind opt ${OCAMLOPTS} -pack -o $@ $+
-
-certicoqc_plugin.cmxa: certicoqc_plugin.cmx
-	ocamlfind opt -linkall ${OCAMLOPTS} -a -o $@ $<
+theories/compile.vo CertiCoq.CertiCoqC.compile.certicoqc.c &: theories/compile.v
+	coqc $(COQOPTS) $<
 
 g_certicoqc.ml: g_certicoqc.mlg certicoqc.cmx certicoqc_plugin_wrapper.cmx
 	coqpp $<
 
-certicoqc_wrapper.c: theories/compile.vo
-
 certicoqc.cmx: certicoqc_plugin_wrapper.cmx
 
+.PRECIOUS: $(GENCFILES)
+
+$(GENCFILES:%.c=%.o): %.o: %.c
+	$(SED) -f unicode.sed -i $<
+	$(CCOMPCOMPILER) $(CCOMPCOMPILEROPTS) -o $@ $<
+
+certicoqc_wrapper.o: %.o: %.c
+	$(SED) -f unicode.sed -i $<
+	$(CCOMPILER) $(CCOMPILEROPTS) -o $@ $<
+
+certicoqc_plugin.cmx: certicoqc_plugin_wrapper.cmx certicoqc.cmx g_certicoqc.cmx
+	ocamlfind opt $(OCAMLOPTS) -pack -o $@ $+
+
+certicoqc_plugin.cmxa: certicoqc_plugin.cmx
+	ocamlfind opt -linkall $(OCAMLOPTS) -a -o $@ $<
+
+certicoqc_plugin.cmxs: certicoqc_plugin.cmxa $(CFILES:.c=.o) $(RUNTIME_FILES)
+	ocamlfind ocamlopt $(OCAMLOPTS) -shared -o $@ $+
+
+.PRECIOUS: %.cmi
 %.cmi: %.mli
-	ocamlfind opt ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin $<
+	ocamlfind opt $(PKGS) $(OCAMLOPTS) -for-pack Certicoqc_plugin $<
 
 %.cmx: %.ml	%.cmi
-	ocamlfind opt -c ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin -o $@ $<
+	ocamlfind opt -c $(PKGS) $(OCAMLOPTS) -for-pack Certicoqc_plugin -o $@ $<
 
 install: theories/compile.vo certicoqc_plugin.cmxs
 	install -d "$(COQLIBINSTALL)"
-	install -m 0644 theories/compile.v theories/compile.vo certicoqc_plugin.cmx* "$(COQLIBINSTALL)"
+	install -m 0644 theories/CertiCoqC.v theories/CertiCoqC.vo theories/compile.v theories/compile.vo certicoqc_plugin.cmx* "$(COQLIBINSTALL)"
 	make -f Makefile.certicoqc install
 	ocamlfind install -add coq-certicoqc certicoqc_plugin.cmx* certicoqc_plugin.cmi
 
 .PHONY: plugin test
+
+.NOTPARALLEL:

bootstrap/certicoqc/_CoqProject

@@ -6,4 +6,3 @@
 META.coq-certicoqc
 
 theories/Loader.v
-theories/CertiCoqC.v

bootstrap/certicoqc/certicoqc.ml

@@ -18,7 +18,7 @@ module MLCompiler : Certicoq.CompilerInterface with
   let printProg prog names (dest : string) (imports : import list) =
     let imports' = List.map (fun i -> match i with
       | FromRelativePath s -> "#include \"" ^ s ^ "\""
-      | FromLibrary s -> "#include <" ^ s ^ ">"
+      | FromLibrary (s, _) -> "#include <" ^ s ^ ">"
       | FromAbsolutePath s ->
           failwith "Import with absolute path should have been filled") imports in
     PrintClight.print_dest_names_imports prog (Cps.M.elements names) dest imports'

bootstrap/certicoqc/certicoqc_plugin_wrapper.ml

@@ -146,6 +146,21 @@ let fix_quoted_program (p : Ast0.Env.program) =
   let declarations = fix_declarations declarations in
   { Ast0.Env.universes = universes; declarations; retroknowledge = retro }, term
 
+let rec print_obj depth x = 
+  if depth <= 0 then Printf.printf "_"
+  else
+  let x = Obj.magic x in
+  if Obj.is_block x then let size = Obj.size x in
+                            if Obj.tag x = 247 then
+                              Printf.printf "POINTER%!"
+                            else
+                            (Printf.printf ("(block[%i] (tag %i) %!") (Obj.size x) (Obj.tag x) ;
+                            for i = 0 to size - 1 do
+                              print_obj (pred depth) (Obj.field x i)
+                            done;
+                            Printf.printf ")")
+  else Printf.printf ("%i %!") x
+
 let compile opts prog =
   info "Calling certicoq-compiled certicoq";
   (* let pretty= Pretty.print_program false (Obj.magic (Caml_nat.nat_of_caml_int 100)) (Obj.magic prog) in *)
@@ -155,4 +170,5 @@ let compile opts prog =
   (* time (str"Compilation with bootstrapped compiler") *)
   let res = certicoq_pipeline opts prog in
   info "Certicoq pipeline ran";
+  (* print_obj 10 (Obj.repr (fst res)); *)
   res