Integrate Rocq checker into CI

.github/workflows/ci.yml

@@ -16,10 +16,6 @@ concurrency:
 
 jobs:
   build:
-    strategy:
-      matrix:
-        version: [4.14.1]
-
 
     runs-on: ubuntu-22.04
 
@@ -49,4 +45,68 @@ jobs:
     - name: Run tests
       working-directory: rems-project/casemate
       run: |
-        make checks
+        make check-examples
+
+  build_rocq:
+    strategy:
+      matrix:
+        version: [4.14.1]
+
+    runs-on: ubuntu-22.04
+
+    steps:
+
+    - run: mkdir -p rems-project
+
+    - uses: actions/checkout@v3
+      with:
+        path: rems-project/casemate
+
+    - name: System dependencies (ubuntu)
+      run: |
+        sudo apt update
+        sudo apt install build-essential opam
+
+    - name: Restore OPAM cache
+      id: cache-opam-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: ~/.opam
+        key: ${{ matrix.version }}
+
+    - name: Setup OPAM
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      working-directory: rems-project/casemate/src/casemate-check-rocq
+      run: |
+        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam repo add --yes iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+        opam pin add --yes --no-action https://github.com/tchajed/coq-record-update.git
+        opam install --deps-only --yes .
+        opam install --yes .
+
+    - name: Save OPAM cache
+      uses: actions/cache/save@v4
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      with:
+        path: ~/.opam
+        key: ${{ matrix.version }}
+
+    - name: Install Casemate-rocq
+      working-directory: rems-project/casemate/src/casemate-check-rocq
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam install --yes .
+
+    - name: Configure
+      working-directory: rems-project/casemate
+      run: |
+        ./configure
+
+    - name: Run Rocq checks
+      working-directory: rems-project/casemate
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        make check-rocq

Makefile

@@ -1,5 +1,5 @@
 .PHONY: build clean
-.PHONY: checks example-traces
+.PHONY: checks example-traces check-examples check-rocq
 .PHONY: casemate casemate-check casemate-lib
 .PHONY: help
 
@@ -53,5 +53,10 @@ clean:
 example-traces:
 	$(call build_subdir,RUN,examples,logs)
 
-checks:
-	$(call build_subdir,RUN,examples,checks)
+check-rocq:
+	$(call build_subdir,RUN,examples,check-rocq)
+
+check-examples:
+	$(call build_subdir,RUN,examples,check-examples)
+
+checks: check-examples check-rocq

examples/Makefile

@@ -1,4 +1,4 @@
-.PHONY: build clean logs list-build-objs
+.PHONY: build clean logs checks list-build-objs
 
 build-objs += simple
 build-objs += good_write
@@ -40,22 +40,20 @@ test_logs = $(patsubst %,$(src)/tests/%.log,$(build-objs))
 
 common_obj = $(src)/common.o
 
-test_checks = $(patsubst %,check-%,$(build-objs))
-
-checks: $(test_checks)
 expected: $(test_expects)
-logs: $(test_logs)
 
 .PRECIOUS: $(common_obj) $(test_objs) $(test_logs)
 
 $(src)/%: $(src)/tests/%.o $(common_obj) $(casemate_o)
 	$(call run_cmd,LD,$@,$(CC) $^ -o $@)
 
-$(src)/tests/%.log: FORCE
-	$(call run_cmd,RUN,$(src)/$*,test -f $(src)/$* && ($(src)/$* -at 1> $@ 2>/dev/null || true))
+check-examples: FORCE
+	$(call run_cmd,CHECK,examples,$(src)/scripts/run_tests.py --examples)
+
+check-rocq: FORCE
+	$(call run_cmd,CHECK,examples,$(src)/scripts/run_tests.py --rocq)
 
-check-%: $(src)/tests/%.log FORCE
-	$(call run_cmd,CHECK,$(src)/$*,$(src)/scripts/check_simulation.py $< $(src)/$(EXPECTEDDIR)/$*.log)
+checks: check-examples check-rocq
 
 clean-%:
 	$(call run_clean,$(src)/$*,rm -f $(src)/$* $(src)/tests/$*.o $(src)/tests/$*.log)

examples/scripts/run_tests.py

@@ -0,0 +1,86 @@
+#!/usr/bin/env python3
+import sys
+import pathlib
+import argparse
+import subprocess
+
+HERE = pathlib.Path(__file__).parent
+EXAMPLES_ROOT = HERE.parent
+CASEMATE_ROOT = EXAMPLES_ROOT.parent
+CASEMATE_CHECK_ROCQ_ROOT = CASEMATE_ROOT / "src" / "casemate-check-rocq"
+
+EXAMPLES = (
+    subprocess.run(
+        ["make", "list-build-objs"],
+        cwd=EXAMPLES_ROOT,
+        capture_output=True,
+        text=True,
+        check=True,
+    ).stdout.strip().split()
+)
+
+
+def runmsg(prefix, s):
+    print(f'  {prefix:<8}\t\t\t{s}', file=sys.stderr)
+
+def check_expected(test_name):
+    example_exe = EXAMPLES_ROOT / test_name
+    out_path = (EXAMPLES_ROOT / "tests" / test_name).with_suffix(".log")
+
+    runmsg("RUN", test_name)
+    with open(out_path, "wb") as logf:
+        subprocess.run(
+            [str(example_exe)],
+            cwd=EXAMPLES_ROOT,
+            stdout=logf,
+            check=False,
+        )
+
+    expected = (EXAMPLES_ROOT / "expected" / test_name).with_suffix(".log")
+    runmsg("CHECK", test_name)
+    subprocess.run(
+        ["python3", "./scripts/check_simulation.py", str(out_path), str(expected)],
+        cwd=EXAMPLES_ROOT,
+        check=True,
+    )
+
+def check_rocq_trace(test_name):
+    expected_log = (EXAMPLES_ROOT / "expected" / test_name).with_suffix(".log")
+
+    runmsg("CHECK", test_name)
+
+    expected_status = expected_log.read_text().strip().splitlines()[-1]
+    expected_status = 121 if expected_status.startswith("!") else 0
+
+    cp = (
+        subprocess.run(
+            ["dune", "exec", "casemate", "--", str(expected_log)],
+            cwd=CASEMATE_CHECK_ROCQ_ROOT,
+            check=False,
+        )
+    )
+
+    if cp.returncode != expected_status:
+        raise ValueError(f"Fail check on {test_name}")
+
+
+def main(argv):
+    args = parser.parse_args(argv)
+
+    for example in EXAMPLES:
+        expected_log = (EXAMPLES_ROOT / "expected" / example).with_suffix(".log")
+
+        if expected_log.exists():
+            if args.rocq:
+                check_rocq_trace(example)
+            else:
+                check_expected(example)
+
+
+parser = argparse.ArgumentParser()
+grp = parser.add_mutually_exclusive_group(required=True)
+grp.add_argument("--rocq", action="store_true", default=False)
+grp.add_argument("--examples", action="store_true", default=False)
+
+if __name__ == "__main__":
+    sys.exit(main(sys.argv[1:]))

src/casemate-check-rocq/src/casemate.ml

@@ -56,16 +56,29 @@ let run_model ?(dump_state = false) ?(dump_roots = false) ?(dump_trans = false)
     if Result.is_error res.cmr_data then Fmt.pr "@[%a@]@." pp_tr trans;
     res.cmr_data
   in
-  Iters.fold_result step_ cms_init xs |> Fmt.pr "@[%a@]@." pp_step_result
+  let res = Iters.fold_result step_ cms_init xs in
+  Fmt.pr "@[%a@]@." pp_step_result res;
+  res
 
 (** Cmdline args **)
 
 open Cmdliner
 
 let ( $$ ) f a = Term.(const f $ a)
-let info = Cmd.info "parser" ~doc:"Describe me"
 
-let term =
+let step_error : Cmd.Exit.code = 121
+
+let exits =
+  Cmd.Exit.defaults @ [ Cmd.Exit.info step_error ~doc:"on bad model step." ]
+
+let exit_of_step r =
+  match r with
+  | Ok _ -> Ok Cmd.Exit.ok
+  | Error _ -> Ok step_error
+
+let info = Cmd.info "parser" ~doc:"Describe me" ~exits:exits
+
+let term : Cmd.Exit.code Term.t =
   let open Arg in
   let trace =
     value
@@ -92,15 +105,17 @@ let term =
     (fun read write limit dump_state dump_roots dump_trans trace ->
       match (read, write, trace) with
       | None, None, Some f ->
-          Ok (run_model ~dump_state ~dump_roots ~dump_trans ?limit (`Text f))
+          run_model ~dump_state ~dump_roots ~dump_trans ?limit (`Text f) |> exit_of_step
       | Some f, None, None ->
-          Ok (run_model ~dump_state ~dump_roots ~dump_trans ?limit (`Bin f))
-      | None, Some e, Some f -> Ok (pre_parse e f)
+          run_model ~dump_state ~dump_roots ~dump_trans ?limit (`Bin f) |> exit_of_step
+      | None, Some e, Some f ->
+        let () = pre_parse e f in
+        Ok Cmd.Exit.ok
       | None, None, None -> Error "No input."
       | _ -> Error "Invalid arguments.")
     $$ read $ write $ limit $ dump_s $ dump_r $ dump_t $ trace)
   |> Term.term_result' ~usage:true
 
 let _ =
   Fmt_tty.setup_std_outputs ();
-  Cmd.v info term |> Cmd.eval
+  Cmd.v info term |> Cmd.eval' |> exit