fix bootstrap

benchmarks/metacoq_erasure/certiCoqErase.ml

@@ -58,7 +58,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   let open List in
   let rec aux p = 
   match p with
-  | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ | Coq_tInt _ | Coq_tFloat _ -> p
+  | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ | Coq_tInt _ | Coq_tFloat _ | tString _ -> p
   | Coq_tEvar (k, l) -> Coq_tEvar (k, map aux l)
   | Coq_tSort u -> Coq_tSort (fix_universe u)
   | Coq_tCast (t, k, t') -> Coq_tCast (aux t, k, aux t')
@@ -136,4 +136,4 @@ let erase ~bypass env evm c =
   debug (fun () -> str"Quoting");
   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
+  time (str"Erasure") certicoq_erase prog

bootstrap/certicoqc/Makefile

@@ -56,7 +56,7 @@ COQLIB = $(shell coqc -where)
 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
+	-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  
 GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
 CFILES = certicoqc_wrapper.c $(GENCFILES)
 
@@ -86,7 +86,7 @@ test.vo: test.v
 	mkdir -p tests
 	ulimit -a
 	ulimit -H -a
-	ulimit -Ss 65500 && coqc $(TESTCOQOPTS) test.v
+	ulimit -Ss unlimited && ulimit -s unlimited && coqc $(TESTCOQOPTS) test.v
 
 clean: Makefile.certicoqc
 	make -f Makefile.certicoqc clean

bootstrap/certicoqc/certicoqc_plugin_wrapper.ml

@@ -79,6 +79,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
   | Coq_tInt i -> Coq_tInt i
   | Coq_tFloat f -> Coq_tFloat f
+  | Coq_tString f -> Coq_tString f
   | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty)
   and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
     { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }
@@ -171,4 +172,4 @@ let compile opts prog =
   let res = certicoq_pipeline opts prog in
   info "Certicoq pipeline ran";
   (* print_obj 10 (Obj.repr (fst res)); *)
-  res
+  res

bootstrap/certicoqc/test.v

@@ -47,4 +47,6 @@ CertiCoqC Eval demo2. *)
 
 (* Time CertiCoqC Compile -build_dir "tests" -time -O 1 demo1. *)
 
+Require Import Coq.Strings.PrimString.
+
 Time CertiCoqC Compile -build_dir "tests" -time -O 1 certicoqc.

runtime/prim_int63.c

@@ -7,7 +7,7 @@ typedef value primbool;
 typedef value primintcarry;
 typedef value primintpair;
 
-#define trace(...) // printf(__VA_ARGS__)
+#define trace(...) printf(__VA_ARGS__)
 
 #define maxuint63 0x7FFFFFFFFFFFFFFF
 

runtime/prim_string.c

@@ -5,41 +5,43 @@
 
 typedef value primstring;
 
+#define trace(...) printf(__VA_ARGS__)
+
 value prim_string_compare(primstring x, primstring y)
 {
   /* register signed long long xr = Unsigned_long_val(x); */
   /* register signed long long yr = Unsigned_long_val(y); */
   /* register signed long long result = xr - yr; */
-  /* trace("Calling prim_int63_compare\n"); */
-  /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
+  trace("Calling prim_string_compare\n");
+  /* trace("Calling prim_string_compare on %llu and %llu: %lli \n", x, y); */
   /* if (result == 0) return 1; */
   /* else if (result < 0) return 3; */
   /* else */
-    return 5;
+    return 1;
 }
 
 primint prim_string_get(primstring x, primint y)
 {
   /* register signed long long xr = Unsigned_long_val(x); */
   /* register signed long long yr = Unsigned_long_val(y); */
   /* register signed long long result = xr - yr; */
-  /* trace("Calling prim_int63_compare\n"); */
+  trace("Calling prim_string_get\n");
   /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
   /* if (result == 0) return 1; */
   /* else if (result < 0) return 3; */
   /* else */
-    return 5;
+    return 97;
 }
 
 primint prim_string_length(primstring x)
 {
   /* register signed long long xr = Unsigned_long_val(x); */
   /* register signed long long yr = Unsigned_long_val(y); */
   /* register signed long long result = xr - yr; */
-  /* trace("Calling prim_int63_compare\n"); */
+  trace("Calling prim_string_length\n");
   /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
   /* if (result == 0) return 1; */
   /* else if (result < 0) return 3; */
   /* else */
-  return 5;
+  return 0;
 }