Rocq is Rocq

etc/ci_coverage_tests.sh

@@ -27,7 +27,7 @@ elif [ "$1" = "other" ]; then
     test/oneoff/run_tests.py || returncode=1
     test/float/run_tests.py || returncode=1
 elif [ "$1" = "rocq" ]; then
-    test/coq/run_tests.py || returncode=1
+    test/rocq/run_tests.py || returncode=1
     test/c/run_tests.py --targets coq || returncode=1
 fi
 

src/sail_coq_backend/sail_plugin_coq.ml

@@ -57,70 +57,76 @@ let opt_coq_isla : string option ref = ref None
 let opt_coq_lib_style : Pretty_print_coq.library_style option ref = ref None
 let opt_separate_interface_file = ref false
 
-let coq_options =
+let make_options prefix hide =
   [
-    ( Flag.create ~prefix:["coq"] ~arg:"directory" "output_dir",
+    ( Flag.create ~prefix ~hide ~arg:"directory" "output_dir",
       Arg.String (fun dir -> opt_coq_output_dir := Some dir),
-      "set a custom directory to output generated Coq"
+      "set a custom directory to output generated Rocq"
     );
-    ( Flag.create ~prefix:["coq"] ~arg:"filename" "lib",
+    ( Flag.create ~prefix ~hide ~arg:"filename" "lib",
       Arg.String (fun l -> opt_libs_coq := l :: !opt_libs_coq),
-      "provide additional library to open in Coq output"
+      "provide additional library to open in Rocq output"
     );
-    ( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules",
+    ( Flag.create ~prefix ~hide ~arg:"filename" "alt_modules",
       Arg.String (fun l -> opt_alt_modules_coq := l :: !opt_alt_modules_coq),
-      "provide alternative modules to open in Coq output"
+      "provide alternative modules to open in Rocq output"
     );
-    ( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules2",
+    ( Flag.create ~prefix ~hide ~arg:"filename" "alt_modules2",
       Arg.String (fun l -> opt_alt_modules2_coq := l :: !opt_alt_modules2_coq),
-      "provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default \
+      "provide additional alternative modules to open only in main (non-_types) Rocq output, and suppress default \
        definitions of MR and M monads"
     );
-    ( Flag.create ~prefix:["coq"] ~arg:"typename" "extern_type",
+    ( Flag.create ~prefix ~hide ~arg:"typename" "extern_type",
       Arg.String Pretty_print_coq.(fun ty -> opt_extern_types := ty :: !opt_extern_types),
       "do not generate a definition for the type"
     );
-    ( Flag.create ~prefix:["coq"] "generate_extern_types",
+    ( Flag.create ~prefix ~hide "generate_extern_types",
       Arg.Set Pretty_print_coq.opt_generate_extern_types,
       "generate only extern types rather than suppressing them"
     );
-    ( Flag.create ~prefix:["coq"] ~arg:"filename" "isla",
+    ( Flag.create ~prefix ~hide ~arg:"filename" "isla",
       Arg.String (fun fname -> opt_coq_isla := Some fname),
-      "generate Coq code for decoding Isla trace values"
+      "generate Rocq code for decoding Isla trace values"
     );
-    ( Flag.create ~prefix:["coq"] "record_update",
+    ( Flag.create ~prefix ~hide "record_update",
       Arg.Set Pretty_print_coq.opt_coq_record_update,
       "use coq-record-update package's syntax for record updates"
     );
-    ( Flag.create ~prefix:["coq"] "lib_style",
+    ( Flag.create ~prefix ~hide "lib_style",
       Arg.Symbol
         ( ["bbv"; "stdpp"],
           fun s -> opt_coq_lib_style := match s with "bbv" -> Some BBV | "stdpp" -> Some Stdpp | _ -> assert false
         ),
-      "select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv otherwise)"
+      "select which style of Rocq library to use (default: stdpp when the concurrency interfaces is used, bbv \
+       otherwise)"
     );
-    ( Flag.create ~prefix:["coq"] ~debug:true "undef_axioms",
+    ( Flag.create ~prefix ~hide "undef_axioms",
       Arg.Set Pretty_print_coq.opt_undef_axioms,
       "generate axioms for functions that are declared but not defined"
     );
-    ( Flag.create ~prefix:["coq"] "minimal_eq_dec",
+    (* Old debug form of option *)
+    (Flag.create ~prefix ~hide:true ~debug:true "undef_axioms", Arg.Set Pretty_print_coq.opt_undef_axioms, "");
+    ( Flag.create ~prefix ~hide "minimal_eq_dec",
       Arg.Clear Pretty_print_coq.opt_coq_all_eq_dec,
       " generate decidable equality instances only when necessary"
     );
-    ( Flag.create ~prefix:["coq"] ~debug:true "warn_nonex",
+    ( Flag.create ~prefix ~hide ~debug:true "warn_nonex",
       Arg.Set Rewrites.opt_coq_warn_nonexhaustive,
-      "generate warnings for non-exhaustive pattern matches in the Coq backend"
+      "generate warnings for non-exhaustive pattern matches in the Rocq backend"
     );
-    ( Flag.create ~prefix:["coq"] ~arg:"function" ~debug:true "debug_on",
+    ( Flag.create ~prefix ~hide ~arg:"function" ~debug:true "debug_on",
       Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f :: !Pretty_print_coq.opt_debug_on),
-      "produce debug messages for Coq output on given function"
+      "produce debug messages for Rocq output on given function"
     );
-    ( Flag.create ~prefix:["coq"] "separate_interface_file",
+    ( Flag.create ~prefix ~hide "separate_interface_file",
       Arg.Set opt_separate_interface_file,
       "create separate file for concurrency interface definitions"
     );
   ]
 
+let rocq_options = make_options ["rocq"] false
+let coq_options = make_options ["coq"] true |> List.map (fun (fl, arg, _desc) -> (fl, arg, ""))
+
 let coq_rewrites =
   let open Rewrites in
   [
@@ -251,7 +257,7 @@ let output libs files =
 
 let ignore_grouped_regstate () =
   if !State.opt_type_grouped_regstate then begin
-    Reporting.simple_warn "-grouped-regstate option not supported in the Coq back-end, ignoring";
+    Reporting.simple_warn "-grouped-regstate option not supported in the Rocq back-end, ignoring";
     State.opt_type_grouped_regstate := false
   end
 
@@ -260,5 +266,11 @@ let coq_target out_file { ctx; ast; effect_info; env; _ } =
   output !opt_libs_coq [(out_file, ctx, effect_info, env, ast)]
 
 let _ =
-  Target.register ~name:"coq" ~options:coq_options ~pre_parse_hook:ignore_grouped_regstate ~rewrites:coq_rewrites
-    ~asserts_termination:true coq_target
+  ignore
+    (Target.register ~name:"rocq" ~options:rocq_options ~pre_parse_hook:ignore_grouped_regstate ~rewrites:coq_rewrites
+       ~asserts_termination:true coq_target
+    );
+  ignore
+    (Target.register ~name:"coq" ~options:coq_options ~pre_parse_hook:ignore_grouped_regstate ~rewrites:coq_rewrites
+       ~asserts_termination:true coq_target
+    )

test/c/mk_coq_main.sh → test/c/mk_rocq_main.sh

@@ -1,12 +1,12 @@
 #!/bin/bash
 
-OUT="_coqbuild_$1/main.v"
+OUT="_rocqbuild_$1/main.v"
 
-if grep -q 'ConcurrencyInterface' "_coqbuild_$1/$1.v"; then
-  if grep -q 'ConcurrencyInterfaceV2' "_coqbuild_$1/$1.v"; then
+if grep -q 'ConcurrencyInterface' "_rocqbuild_$1/$1.v"; then
+  if grep -q 'ConcurrencyInterfaceV2' "_rocqbuild_$1/$1.v"; then
     V2=true
   fi
-  if grep -q 'sail_model_init.*: unit :=' "_coqbuild_$1/$1.v"; then
+  if grep -q 'sail_model_init.*: unit :=' "_rocqbuild_$1/$1.v"; then
     RUN="main tt"
   else
     RUN="Defs.bind0 (sail_model_init tt) (main tt)"
@@ -160,7 +160,7 @@ else
 
   Goal True.
 EOF
-  if grep -q "Definition main '(tt : unit) : unit :=" "_coqbuild_$1/$1.v"; then
+  if grep -q "Definition main '(tt : unit) : unit :=" "_rocqbuild_$1/$1.v"; then
     cat <<EOF >> "$OUT"
   let result := eval vm_compute in (main tt) in
   match result with
@@ -171,12 +171,12 @@ EOF
   Qed.
 EOF
   else
-    if grep -q 'initial_regstate' "_coqbuild_$1/$1.v"; then
+    if grep -q 'initial_regstate' "_rocqbuild_$1/$1.v"; then
       REGSTATE="initial_regstate"
     else
       REGSTATE='init_regstate'
     fi
-    if grep -q 'sail_model_init.*: unit :=' "_coqbuild_$1/$1.v"; then
+    if grep -q 'sail_model_init.*: unit :=' "_rocqbuild_$1/$1.v"; then
       RUN="main tt"
     else
       RUN="Prompt_monad.bind0 (sail_model_init tt) (main tt)"

test/c/run_tests.py

@@ -158,7 +158,7 @@ def test_lem(name):
         results.collect(tests)
     return results.finish()
 
-def test_coq(name):
+def test_rocq(name):
     banner('Testing {}'.format(name))
     results = Results(name)
     results.expect_failure("inc_tests.sail", "missing built-in functions for increasing vectors in Coq library")
@@ -186,24 +186,24 @@ def test_coq(name):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 # Generate Coq from Sail
-                step('\'{}\' -coq -coq-record-update -D PRINT_EFFECTS -splice coq-print.splice -undefined_gen -o {} {}'.format(sail, basename, filename))
+                step('\'{}\' --rocq --rocq-record-update -D PRINT_EFFECTS --splice rocq-print.splice --undefined-gen -o {} {}'.format(sail, basename, filename))
 
-                step('mkdir -p _coqbuild_{}'.format(basename))
-                step('mv {}.v _coqbuild_{}'.format(basename, basename))
-                step('mv {}_types.v _coqbuild_{}'.format(basename, basename))
-                step('./mk_coq_main.sh {} {}'.format(basename, basename.capitalize()))
-                os.chdir('_coqbuild_{}'.format(basename))
+                step('mkdir -p _rocqbuild_{}'.format(basename))
+                step('mv {}.v _rocqbuild_{}'.format(basename, basename))
+                step('mv {}_types.v _rocqbuild_{}'.format(basename, basename))
+                step('./mk_rocq_main.sh {} {}'.format(basename, basename.capitalize()))
+                os.chdir('_rocqbuild_{}'.format(basename))
 
                 step('coqc {}_types.v'.format(basename))
                 step('coqc {}.v'.format(basename))
                 step('coqtop -require-import {}_types -require-import {} -l main.v -batch | tee /dev/stderr | grep -q OK'.format(basename,basename), expected_status = 1 if basename.startswith('fail') else 0)
-                filter_command = '''ocaml ../coq_output_filter.ml < '''
+                filter_command = '''ocaml ../rocq_output_filter.ml < '''
                 step('''{} output.out | diff - ../{}.expect'''.format(filter_command, basename, basename))
                 if os.path.exists('../{}.err_expect'.format(basename)):
                     step('''{} error.out | diff - ../{}.err_expect'''.format(filter_command, basename, basename))
 
                 os.chdir('..')
-                step('rm -r _coqbuild_{}'.format(basename))
+                step('rm -r _rocqbuild_{}'.format(basename))
                 print('{} {}{}{}'.format(filename, color.PASS, 'ok', color.END))
                 sys.exit()
         results.collect(tests)
@@ -241,8 +241,8 @@ def test_coq(name):
 if 'lem' in targets:
     xml += test_lem('lem')
 
-if 'coq' in targets:
-    xml += test_coq('coq')
+if 'rocq' in targets or 'coq' in targets:
+    xml += test_rocq('rocq')
 
 xml += '</testsuites>\n'
 

test/lean/run_tests.py

@@ -99,7 +99,7 @@ def test_lean(subdir: str, skip_list = None, runnable: bool = False):
                 # TODO: should probably be dependent on whether print should be pure or effectful.
                 extra_flags = [
                     '--splice',
-                    'coq-print.splice',
+                    'rocq-print.splice',
                     '--strict-bitvector',
                 ] if runnable else [ ]
                 if not runnable:

test/coq/run_tests.py → test/rocq/run_tests.py

@@ -23,7 +23,7 @@
 }
 
 def test(name, dir, lib):
-    banner('Testing Coq backend on {} with {}'.format(name, lib))
+    banner('Testing Rocq backend on {} with {}'.format(name, lib))
     results = Results('{} on {}'.format(name, lib))
     results.expect_failure('exist1.sail', 'Needs an existential witness')
     results.expect_failure('while_MM.sail', 'Non-terminating loops - I\'ve written terminating versions of these')
@@ -60,7 +60,7 @@ def test(name, dir, lib):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('mkdir -p _build_{}'.format(basename))
-                step('\'{}\' --coq --coq-lib-style {} --dcoq-undef-axioms --strict-bitvector --coq-output-dir _build_{} -o out {}/{}'.format(sail, lib, basename, dir, filename))
+                step('\'{}\' --rocq --rocq-lib-style {} --rocq-undef-axioms --strict-bitvector --rocq-output-dir _build_{} -o out {}/{}'.format(sail, lib, basename, dir, filename))
                 os.chdir('_build_{}'.format(basename))
                 step('coqc out_types.v', name=basename)
                 step('coqc out.v', name=basename)