add support for rocq 9.0

.github/workflows/docker-action.yml

@@ -14,7 +14,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20'
+          - 'rocq/rocq-prover:9.0'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4

.gitignore

@@ -20,3 +20,4 @@ ocamlgraph-1.7
 .merlin
 make_merlin.sh
 ott.install
+regression/regression

coq-ott.opam

@@ -18,7 +18,7 @@ this library.
 build: [make "-j%{jobs}%" "-C" "coq"]
 install: [make "-C" "coq" "install"]
 depends: [
-  "coq" {>= "8.14"}
+  ("coq" {>= "8.14" & < "9.0"}) | ("rocq-prover" {>= "9.0"} & "coq" {>= "9.0"})
 ]
 tags: [
   "category:Computer Science/Semantics and Compilation/Semantics"

regression/Makefile

@@ -36,11 +36,11 @@
 all: regression
 
 regression: regression.ml
-	ocamlc unix.cma str.cma -o regression -dtypes regression.ml
+	ocamlc -I +unix -I +str unix.cma str.cma -o regression -dtypes regression.ml
 
 regression_p: regression_p_client.ml regression_p_master.ml
-	ocamlc unix.cma str.cma -o regression_p_client regression_p_client.ml
-	ocamlc unix.cma str.cma -o regression_p_master regression_p_master.ml
+	ocamlc -I +unix -I +str unix.cma str.cma -o regression_p_client regression_p_client.ml
+	ocamlc -I +unix -I +str unix.cma str.cma -o regression_p_master regression_p_master.ml
 
 regression_para: regression_para.ml
 	ocamlp3lopt -par unix.cmxa str.cmxa -o regression_para regression_para.ml
@@ -77,7 +77,7 @@ clean-regr:
 
 # Jenkins
 
-# regression-jenkins: 
+# regression-jenkins:
 # 	ocamlc unix.cma str.cma -o regression-jenkins -dtypes regression-jenkins.ml
 
 run-jenkins: regression

regression/baseline-2025-03.txt

@@ -0,0 +1,103 @@
+ Coq CoqNL Isa  HOL OCaml LaTeX
+ -    -    -    + +  -    + + ../tests/leroy-jfp96.ott
+ -    -    -    -    -    + + ../tests/test-j.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-lj-list_ambiguity.ott
+ + +  + +  -    -    -    + - ../tests/test-mjp-trans.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-mjp.ott
+ + +  + +  + +  + +  + +  + + ../tests/test-pottier1.ott
+ + +  + +  + +  + +  + -  + + ../tests/test1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test10.ott
+ + +  + +  + +  + +  -    + + ../tests/test10_homs.ott
+ + +  + +  + +  -    -    + + ../tests/test10_isasyn.ott
+ + +  + +  + +  + +  -    + + ../tests/test10st.ott
+ + -  + -  + -  -    -    + + ../tests/test10st_fe.ott
+ + +  + +  + +  + +  -    + + ../tests/test10st_first_half.ott
+ + +  + +  + +  + +  + +  + + ../tests/test11.ott
+ + +  + +  + +  + +  + +  + + ../tests/test12.ott
+ + +  + +  + +  + +  + +  + + ../tests/test13.ott
+ + -  + -  + -  + -  + +  + + ../tests/test13b.ott
+ + +  + +  + +  + +  + +  + + ../tests/test14.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.2.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.3.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4b.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4c.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4d.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.5.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.6.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.7.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.2.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.3.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.4.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.5.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.6.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.1.ott
+ + +  + +  + -  + +  -    + + ../tests/test17.10.ott
+ + -  + -  + -  + +  -    + + ../tests/test17.11.ott
+ + +  + +  + -  + +  -    + + ../tests/test17.12.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.13.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.14.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.2.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.3.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.4.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.5.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.6.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.7.ott
+ + +  + +  + -  + +  + +  + + ../tests/test17.8.ott
+ + +  + +  + -  + +  + +  + + ../tests/test17.9.ott
+ + +  + +  + +  + +  + +  + + ../tests/test18.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test18.1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test18.2.ott
+ + -  + -  + -  + +  -    + + ../tests/test19.0.ott
+ + +  + +  + +  + -  + +  + + ../tests/test2.ott
+ -    -    -    -    -    + + ../tests/test3.ott
+ + +  + +  + +  + -  + -  + + ../tests/test4.ott
+ -    -    -    -    -    + + ../tests/test5.ott
+ -    -    -    -    -    + + ../tests/test6-tex.ott
+ -    -    -    -    -    + + ../tests/test6.ott
+ + -  + -  + +  + +  + +  + + ../tests/test8.ott
+ -    -    -    -    -    + + ../tests/test8p.ott
+ -    -    -    -    -    + + ../tests/test_jan_2006-09-08.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + +  + +  + -  + +  + + ../tests/test_lists_freevars_1.ott
+ + +  + +  + +  + +  -    + + sys-bool
+ + +  + +  + +  + +  -    + + sys-arith
+ + +  + +  + +  + +  -    + + sys-untyped
+ + +  + +  + -  + -  -    + + sys-puresimple
+ + +  + +  + +  + +  -    + + sys-tybool
+ + +  + +  + -  + +  -    + - sys-sortoffullsimple
+ + -  + -  + -  + -  -    + + sys-tuple
+ + +  + +  + +  + +  -    + + sys-puresub
+ + +  + +  + -  + +  -    + - sys-roughlyfullsimple
+ + -  + -  + -  + +  -    + + sys-purercdsub
+ -    -    -    -    -    -   ../tests/test_bind_aux_empty_1.ott
+ -    -    -    -    -    -   ../tests/test_bind_dots_1.ott
+ + +  + +  + -  + -  + -  + + ../tests/test_bind_isa_1.ott
+ + +  + +  + +  + -  + +  + + ../tests/test_coq_equality_x_1.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_defn_repeated_nonterminal_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_embed_top_1.ott
+ + -  + -  + -  + -  + +  + + ../tests/test_empty_defn.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_lists_coq_bind_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_lists_coq_defn_subrule_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_lists_coq_defn_subrule_2.ott
+ + +  + +  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_3.ott
+ + +  + +  + -  + -  + -  + + ../tests/test_lists_coq_defn_subrule_4.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_lists_coq_defn_tuple_1.ott
+ + +  + +  + -  + +  + +  + + ../tests/test_lists_coq_defn_tuple_2.ott
+ + +  + +  + -  + -  -    + - ../tests/test_lists_coq_list_functions_1.ott
+ + +  + +  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_2.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_lists_defn_list_form_1.ott
+ + -  + -  + -  + +  -    + + ../tests/test_lists_coq_list_functions_3.ott
+ + -  + -  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_4.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_subrules_1.ott
+ -    -    -    -    -    -   ../tests/test_lists_terminal_1.ott
+ + +  + +  + -  + +  -    + + ../tests/test_embed_location_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_embed_top_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_merge_embed_location_1-1.ott
+ + +  + +  + -  + +  -    + + ../tests/test_merge_embed_location_1-2.ott

regression/baseline-jenkins.txt

@@ -0,0 +1,102 @@
+ Coq CoqNL Isa  HOL OCaml LaTeX
+ -    -    -    + -  -    + + ../tests/leroy-jfp96.ott
+ -    -    -    -    -    + + ../tests/test-j.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-lj-list_ambiguity.ott
+ + +  + -  -    -    -    + - ../tests/test-mjp-trans.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-mjp.ott
+ + +  + -  + -  + +  + +  + + ../tests/test-pottier1.ott
+ + +  + -  + -  + +  + -  + + ../tests/test1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test10.ott
+ + +  + -  + -  + +  -    + + ../tests/test10_homs.ott
+ + +  + -  + -  -    -    + + ../tests/test10_isasyn.ott
+ + +  + -  + -  + +  -    + + ../tests/test10st.ott
+ + -  + -  + -  -    -    + + ../tests/test10st_fe.ott
+ + +  + -  + -  + +  -    + + ../tests/test10st_first_half.ott
+ + +  + -  + -  + +  + +  + + ../tests/test11.ott
+ + +  + -  + -  + +  + +  + + ../tests/test12.ott
+ + +  + -  + -  + +  + +  + + ../tests/test13.ott
+ + -  + -  + -  + -  + +  + + ../tests/test13b.ott
+ + +  + -  + -  + +  + +  + + ../tests/test14.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.3.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4b.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4c.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4d.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.5.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.6.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.7.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.3.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.4.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.5.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.6.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.1.ott
+ + +  + -  + -  + +  -    + + ../tests/test17.10.ott
+ + +  + -  + -  + +  -    + + ../tests/test17.11.ott
+ + +  + -  + -  + +  -    + + ../tests/test17.12.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.13.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.14.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.3.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.4.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.5.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.6.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.7.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.8.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.9.ott
+ + +  + -  + -  + +  + +  + + ../tests/test18.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test18.1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test18.2.ott
+ + +  + -  + -  + +  -    + + ../tests/test19.0.ott
+ + +  + -  + -  + -  + +  + + ../tests/test2.ott
+ -    -    -    -    -    + + ../tests/test3.ott
+ + +  + -  + -  + -  + -  + + ../tests/test4.ott
+ -    -    -    -    -    + + ../tests/test5.ott
+ -    -    -    -    -    + + ../tests/test6-tex.ott
+ -    -    -    -    -    + + ../tests/test6.ott
+ + -  + -  + -  + +  + +  + + ../tests/test8.ott
+ -    -    -    -    -    + + ../tests/test8p.ott
+ -    -    -    -    -    + + ../tests/test_jan_2006-09-08.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_freevars_1.ott
+ + -  + -  + -  + +  -    + + sys-bool
+ + -  + -  + -  + +  -    + + sys-arith
+ + -  + -  + -  + +  -    + + sys-untyped
+ + -  + -  + -  + -  -    + + sys-puresimple
+ + -  + -  + -  + +  -    + + sys-tybool
+ + -  + -  + -  + +  -    + - sys-sortoffullsimple
+ + -  + -  + -  + -  -    + + sys-tuple
+ + -  + -  + -  + +  -    + + sys-puresub
+ + -  + -  + -  + +  -    + - sys-roughlyfullsimple
+ + -  + -  + -  + +  -    + + sys-purercdsub
+ -    -    -    -    -    -   ../tests/test_bind_aux_empty_1.ott
+ -    -    -    -    -    -   ../tests/test_bind_dots_1.ott
+ + +  + -  + -  + -  + -  + + ../tests/test_bind_isa_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_coq_equality_x_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_defn_repeated_nonterminal_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_embed_top_1.ott
+ + -  + -  + -  + -  + +  + + ../tests/test_empty_defn.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_coq_bind_1.ott
+ + -  + -  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_3.ott
+ + -  + -  + -  + -  + +  + + ../tests/test_lists_coq_defn_tuple_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_coq_defn_tuple_2.ott
+ + -  + -  + -  + -  -    + - ../tests/test_lists_coq_list_functions_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_2.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_defn_list_form_1.ott
+ + -  + -  + -  + +  -    + + ../tests/test_lists_coq_list_functions_3.ott
+ + -  + -  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_4.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_subrules_1.ott
+ -    -    -    -    -    -   ../tests/test_lists_terminal_1.ott
+ + +  + -  + -  + +  -    + + ../tests/test_embed_location_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_embed_top_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_merge_embed_location_1-1.ott
+ + +  + -  + -  + +  -    + + ../tests/test_merge_embed_location_1-2.ott

regression/regression.ml

@@ -92,7 +92,7 @@ let latex_regressions = ref 0
 (* let twelf_progressions = ref 0 *)
 (* let twelf_regressions = ref 0 *)
 let summary = ref []
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 let config_state = ref []
 
 let _ =
@@ -354,7 +354,7 @@ let run_test i n (tn,tl) =
     if (command cmd) = 0
     then begin
       pp_success tgt name;
-      let cmd = "coqc -init-file _ott_coqrc.v "^name^".v > " ^ name ^ ".coq.out" (* was "/dev/null"*)  in
+      let cmd = "coqc -Q ../coq Ott "^name^".v > " ^ name ^ ".coq.out" (* was "/dev/null"*)  in
       let tgt = "Coq" in
       pp_tgt i_of_n tgt cmd;
       if (command cmd) = 0 then begin
@@ -382,7 +382,7 @@ let run_test i n (tn,tl) =
     if (command cmd) = 0
     then begin
       pp_success tgt name;
-      let cmd = "coqc -init-file _ott_coqrc.v "^name^".v" in
+      let cmd = "coqc -Q ../coq Ott "^name^".v" in
       let tgt = "Coq" in
       pp_tgt i_of_n tgt cmd;
       if (command cmd) = 0 then begin
@@ -575,7 +575,7 @@ let report tp a b =
     progressions := !progressions + 1;
     ott_progressions := !ott_progressions + 1
   end else 
-    if not a.ott && b.ott 
+    if not a.ott && b.ott && not (a.tp = Skipped || b.tp = Skipped)
     then begin
       regressions := !regressions + 1;
       ott_regressions := !ott_regressions + 1
@@ -839,4 +839,6 @@ let _ =
     end;
     output_string fd "</testsuite>\n";
     close_out fd
-  end
+  end;
+
+  if !regressions != 0 then exit 1

regression/regression.otl

@@ -86,6 +86,7 @@ sys-purercdsub : ../examples/tapl/common.ott ../examples/tapl/common_typing.ott
 ../tests/test_lists_coq_defn_subrule_1.ott
 ../tests/test_lists_coq_defn_subrule_2.ott
 ../tests/test_lists_coq_defn_subrule_3.ott
+../tests/test_lists_coq_defn_subrule_4.ott
 ../tests/test_lists_coq_defn_tuple_1.ott
 ../tests/test_lists_coq_defn_tuple_2.ott
 ../tests/test_lists_coq_list_functions_1.ott

regression/regression_p_client.ml

@@ -71,7 +71,7 @@ let latex_regressions = ref 0
 let twelf_progressions = ref 0
 let twelf_regressions = ref 0
 let summary = ref []
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 
 (* let _ = *)
 (*   putenv "CVSROOT" ":pserver:zappa@localhost:/usr/groups/netsem/dynsem/cvs"; *)

regression/regression_p_master.ml

@@ -67,7 +67,7 @@ let latex_progressions = ref 0
 let latex_regressions = ref 0
 let twelf_progressions = ref 0
 let twelf_regressions = ref 0
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 
 (* let _ = *)
 (*   if !night then begin *)

regression/regression_para.ml

@@ -83,7 +83,7 @@ let latex_regressions = ref 0
 let twelf_progressions = ref 0
 let twelf_regressions = ref 0
 let summary = ref []
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 let config_state = ref []
 
 let _ =