Joho bazel system tests

.bazelrc

@@ -2,3 +2,8 @@ common --enable_bzlmod
 
 build:lint --aspects=//tools/lint:linters.bzl%pylint,//tools/lint:linters.bzl%ty
 build:lint --output_groups=+rules_lint_human
+
+# --combined_report=lcov merges per-test .dat files into one LCOV report.
+# --instrumentation_filter restricts instrumentation to the trlc library only.
+coverage --combined_report=lcov
+coverage --instrumentation_filter="//trlc[/:]"

.gitignore

@@ -1,10 +1,13 @@
 # Project ignores
 docs
+htmlcov
 .coverage*
 *.lobster
 
 # Python ignores
 *.pyc
+__pycache__
+.ruff_cache
 *.egg-info
 .venv/
 venv/

BUILD

@@ -57,3 +57,9 @@ alias(
     name = "format.fix",
     actual = "//tools/format:format",
 )
+
+filegroup(
+    name = "coverage",
+    srcs = ["coverage.cfg"],
+    visibility = ["//visibility:public"],
+)

CHANGELOG.md

@@ -27,12 +27,25 @@ generated in the following situations:
 
 ### 2.0.4-dev
 
-* [BAZEL] Add Rules Lint for Formatting and Linting
+* [TRLC] Rework system tests as Bazel-native golden-file tests: each
+  test directory is now a single `py_test` with one method per output
+  mode (`output`, `output.brief`, `output.json`, `output.smtlib`),
+  selectable via `--test_filter`.
 
-* [BAZEL] Update Bazel to 8.5.1
+* [TRLC] Add `--log FILE PREFIX` to write all output to FILE
+  and strip PREFIX from file paths (used by Bazel system test actions).
+
+* [TRLC] `Message_Handler` now accepts `out_path` to open and manage
+  its own output file; use as a context manager to ensure it is closed.
+
+* [TRLC] Update Bazel CVC5 version to 1.3.2.
 
 * [BAZEL] Update Rules Python to 1.1.0
 
+* [BAZEL] Add Rules Lint for Formatting and Linting
+
+* [BAZEL] Update Bazel to 8.5.1
+
 ### 2.0.3
 
 * [API] Fix incorrect output of `Integer_Literal.dump()` method.

MODULE.bazel

@@ -29,6 +29,7 @@ python.toolchain(python_version = "3.11")
 python.toolchain(
     is_default = True,
     python_version = "3.12",
+    configure_coverage_tool = True,
 )
 
 use_repo(python, "python_versions")
@@ -68,26 +69,27 @@ use_repo(pip_dev, "trlc_dev_dependencies")
 
 http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
 
+
 http_archive(
     name = "cvc5_linux",
     build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "ab9344e2dddda794669c888a3afcd99f25f2627e1d426bd7d08ecb267361b331",
+    sha256 = "30abf22d8042f3c4d3eb1120c595abd461f92f276a6d1264895fb4403b5fb3fd",
     strip_prefix = "cvc5-Linux-x86_64-static-gpl",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static-gpl.zip",
+    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-Linux-x86_64-static-gpl.zip",
 )
 
 http_archive(
     name = "cvc5_mac",
     build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "2b983ca743ef1327b51408bf8ba6c08c97beaadde2c3968da701ca16bb1e3740",
+    sha256 = "9b00ae44d51903cd830e281c97066d7e4c0a57f1aa6c5b275435d3016427be64",
     strip_prefix = "cvc5-macOS-arm64-static-gpl",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-macOS-arm64-static-gpl.zip",
+    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-macOS-arm64-static-gpl.zip",
 )
 
 http_archive(
     name = "cvc5_windows",
     build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "256f4af3f4181e770801df436852cb3c76c86dbf9b69a47064d7f8d5bc0ee1d2",
+    sha256 = "206d55380f9a0ccf43541756b5ce2be487efcbbf322b93dc1de662856c70e5cc",
     strip_prefix = "cvc5-Win64-x86_64-static",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Win64-x86_64-static.zip",
+    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-Win64-x86_64-static.zip",
 )

Makefile

@@ -12,28 +12,34 @@ test: unit-tests system-tests
 	make coverage
 	util/check_local_modifications.sh
 
+# bazel equivalent: bazel test //tests-unit/... //tests-system:all_tests
 test-all: unit-tests system-tests-all
 	make coverage
 	util/check_local_modifications.sh
 
+# bazel equivalent: bazel coverage --combined_report=lcov //tests-system/... //api-examples/...
+#   genhtml "$(bazel info output_path)/_coverage/_coverage_report.dat" -o htmlcov
 coverage:
 	coverage combine -q
 	coverage html --rcfile=coverage.cfg
 	coverage report --rcfile=coverage.cfg --fail-under=94
 
+# bazel equivalent: bazel test //tests-unit/...
 unit-tests:
 	coverage run -p \
                 --branch --rcfile=coverage.cfg \
                 --data-file .coverage \
                 -m unittest discover -s tests-unit -v
 
+# bazel equivalent: bazel test //tests-system:fast
 system-tests:
 	mkdir -p docs
 	coverage run -p --rcfile=coverage.cfg --branch --data-file .coverage \
 		./trlc-lrm-generator.py
 	make -C tests-system -B -j8 fast
 	make -C tests-large-partial -B -j8 fast
 
+# bazel equivalent: bazel test //tests-system:all_tests
 system-tests-all:
 	mkdir -p docs
 	coverage run -p --rcfile=coverage.cfg --branch --data-file .coverage \

README.md

@@ -65,6 +65,6 @@ The Python implementation can be used for several purposes:
   (required when using the `--verify` option)
 
 Optional dependency (not installed automatically):
-* [Binary CVC5](https://github.com/cvc5/cvc5/releases/tag/cvc5-1.0.8)
+* [Binary CVC5](https://github.com/cvc5/cvc5/releases/tag/cvc5-1.3.2)
   (An alternative to PyPI CVC5, make sure to rename the binary to
   `cvc5` and put it on your PATH).

bazel/_private/BUILD.bazel

@@ -0,0 +1 @@
+exports_files(["mode_test.py"])