Joho adapt bazel python api

.github/workflows/ci.yml

@@ -62,7 +62,7 @@ jobs:
           echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH
       - name: Fetch CVC5
         run: |
-          util/fetch_cvc5.py 1.3.1 ${{ matrix.cvc5-plat }}
+          util/fetch_cvc5.py ${{ matrix.cvc5-plat }}
           echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
       - name: Executing unit tests
         run: |

.github/workflows/docs.yml

@@ -45,7 +45,7 @@ jobs:
           sudo apt-get install -y graphviz
       - name: Fetch CVC5
         run: |
-          util/fetch_cvc5.py 1.2.0 linux
+          util/fetch_cvc5.py linux
           echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
       - name: Test CVC5
         run: |

BUILD

@@ -38,7 +38,7 @@ alias(
 compile_pip_requirements(
     name = "requirements",
     src = "requirements.txt",
-    requirements_txt = "requirements.txt.bazel",
+    requirements_txt = "requirements_lock.txt",
 )
 
 # Run: bazel run //:requirements_dev.update

MODULE.bazel

@@ -40,7 +40,7 @@ pip = use_extension("@rules_python//python/extensions:pip.bzl", "pip")
     pip.parse(
         hub_name = "trlc_dependencies",
         python_version = python_version,
-        requirements_lock = "//:requirements.txt",
+        requirements_lock = "//:requirements_lock.txt",
     )
     for python_version in [
         "3.9",
@@ -70,6 +70,11 @@ use_repo(pip_dev, "trlc_dev_dependencies")
 http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
 
 
+# ---------------------------------------------------------------------------
+# CVC5 binary archives
+# Keep in synch with CVC5_DEFAULT_VERSION in util/fetch_cvc5.py
+# and requirements.txt / requirements_dev.txt
+# ---------------------------------------------------------------------------
 http_archive(
     name = "cvc5_linux",
     build_file = "@trlc//:cvc5.BUILD",

bazel/_private/mode_test.py

@@ -67,14 +67,12 @@ def _run_mode(mode):
 
     args = ["trlc"]
 
-    if mode in ("output", "output.smtlib"):
+    if mode == "output":
+        args += ["--verify"]
+    elif mode == "output.smtlib":
         # _CVC5_RLOC is a runfiles-relative path produced by
         # $(rlocationpath //:cvc5); resolve it via TEST_SRCDIR directly.
         cvc5 = os.path.join(os.environ["TEST_SRCDIR"], _CVC5_RLOC)
-        # TODO: The Makefile only passes --use-cvc5-binary for
-        #       output.smtlib, not for plain output.  Align once the
-        #       golden files have been regenerated without cvc5 for
-        #       the "output" mode.
         args += ["--verify", "--use-cvc5-binary", cvc5]
     elif mode == "output.brief":
         args += ["--no-lint", "--brief"]

bazel/_private/system_test.bzl

@@ -1,54 +1,20 @@
-"""File system test runner for the trlc repository.
+"""Golden-file system test runner for trlc.
 
-``trlc_system_test(test_dir)`` creates one ``native.py_test`` per test
-directory.  Inside ``mode_test.py`` each available output mode is run
-sequentially; failures are collected and reported at the end.
-
-Each mode invokes ``trlc --log`` (writes output to a file) and
-diffs the result against the committed golden file.
-
-Which modes are run is determined at runtime by ``mode_test.py`` by listing
-the ``output*`` golden files present in the test directory.  Extra trlc flags
-(e.g. ``--no-detailed-info``) are read from an optional ``options`` file
-inside the test directory.
+Runs trlc against each output* golden file in a test directory and diffs
+the results.  Extra flags may be provided via an optional ``options`` file.
 """
 
 def trlc_system_test(test_dir):
-    """Create a single golden-file py_test for a tests-system/ directory.
-
-    Args forwarded via Bazel ``args`` to ``mode_test.py``:
-
-    .. code-block:: text
-
-        argv[1]  root_dir   "tests-system"
-        argv[2]  test_dir   plain string, e.g. "checks-1"
-        argv[3]  cvc5_rloc  $(rlocationpath //:cvc5)
-
-    Available modes are discovered at runtime from the ``output*`` files
-    present in the test directory.  An optional ``options`` file in the
-    directory may contain extra trlc flags (one per line or whitespace-
-    separated), e.g. ``--no-detailed-info``.
-
-    Two Bazel targets are created (example for ``test_dir = "checks-1"``):
-
-    .. code-block:: text
-
-        //tests-system:checks-1_test  (py_test)
-        //tests-system:checks-1       (test_suite alias)
+    """Create a py_test and test_suite alias for a tests-system/ subdirectory.
 
     Args:
       test_dir: subdirectory name inside tests-system/.
     """
     srcs = native.glob([test_dir + "/**"])
 
-    # cvc5 is always needed: "output" mode (always present) requires it.
-    #
-    # NOTE: the py_test must NOT be named test_dir because Bazel would create
-    # a runfiles symlink  tests-system/<test_dir> -> bazel-out/…/<test_dir>
-    # that obscures the source-directory symlinks for the golden files inside
-    # it.  The "_test" suffix avoids that collision.  A test_suite under the
-    # plain test_dir name preserves the short  bazel test //tests-system:<dir>
-    # invocation.
+    # cvc5 binary is always included for tests with an output.smtlib golden file.
+    # The "_test" suffix avoids a runfiles symlink collision with the source dir;
+    # a test_suite alias under the plain name allows: bazel test //tests-system:<dir>
     test_target = test_dir + "_test"
 
     native.py_test(

requirements.txt

@@ -1,2 +1,2 @@
 pyvcg==1.0.9
-cvc5>=1.3.1
+cvc5>=1.3.2

requirements_dev.txt

@@ -1,6 +1,5 @@
-# Carryover from requirements.txt
 pyvcg==1.0.9
-cvc5>=1.3.1
+cvc5>=1.3.2
 
 # Development tools
 pycodestyle>=2.12

trlc.bzl

@@ -23,7 +23,7 @@ def trlc_specification_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc
     native.py_test(
         name = name,
         srcs = srcs,
-        args = ["--use-cvc5-binary $(location @trlc//:cvc5)", "--verify", "--skip-trlc-files"],
+        args = ["--verify", "--skip-trlc-files"],
         main = main,
         deps = ["@trlc//trlc:trlc"],
         data = ["@trlc//:cvc5"] + reqs,
@@ -68,7 +68,7 @@ def trlc_requirements_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc.
     native.py_test(
         name = name,
         srcs = srcs,
-        args = ["--use-cvc5-binary $(location @trlc//:cvc5)", "--verify"],
+        args = ["--verify"],
         main = main,
         deps = ["@trlc//trlc:trlc"],
         data = ["@trlc//:cvc5"] + reqs,

trlc/BUILD

@@ -17,5 +17,8 @@ py_library(
         "version.py",
     ],
     visibility = ["//visibility:public"],
-    deps = [requirement("pyvcg")],
+    deps = [
+        requirement("pyvcg"),
+        requirement("cvc5"),
+    ],
 )

util/fetch_cvc5.py

@@ -31,8 +31,17 @@
 CVC5_BINARY = "cvc5"
 CVC5_EXECUTABLE = True
 
+# -----------------------------------------------------------------------
+# Canonical CVC5 binary version used throughout this project.
+# Bump this together with:
+#   * The http_archive URLs/sha256 hashes in MODULE.bazel
+#   * The "cvc5>=" lower-bound in requirements.txt / requirements_dev.txt
+# -----------------------------------------------------------------------
+CVC5_DEFAULT_VERSION = "1.3.2"
+
 ap = argparse.ArgumentParser()
-ap.add_argument("version")
+ap.add_argument("--version", default=CVC5_DEFAULT_VERSION,
+                help="CVC5 release tag (default: %(default)s)")
 ap.add_argument("platform")
 
 options = ap.parse_args()