From eb38a6fb3daa9d162e7827050a7f665a4ec956ea Mon Sep 17 00:00:00 2001 From: Jochen Hoenle Date: Wed, 25 Feb 2026 16:23:37 +0100 Subject: [PATCH 1/2] [TRLC] include argument to output to logfile instead of stdout --- trlc/errors.py | 57 ++++++++++++++++++++++++++++++++++++++++++-------- trlc/trlc.py | 32 +++++++++++++++++++++------- 2 files changed, 72 insertions(+), 17 deletions(-) diff --git a/trlc/errors.py b/trlc/errors.py index 86878c9e..229f1cc4 100644 --- a/trlc/errors.py +++ b/trlc/errors.py @@ -149,6 +149,12 @@ class Message_Handler: :attribute brief: When true displays as much context as possible :type: Boolean + :attribute out: Output stream (stdout if None) + :type: file or None + + :attribute strip_prefix: Prefix stripped from file paths in messages + :type: str or None + :attribute warnings: Number of system or user warnings raised :type: int @@ -158,9 +164,16 @@ class Message_Handler: :attribute supressed: Number of messages supressed by policy :type: int + Can be used as a context manager (``with Message_Handler(...) as + mh:``), which will automatically close any file opened via + ``out_path``. + """ - def __init__(self, brief=False, detailed_info=True): + def __init__(self, brief=False, detailed_info=True, + out=None, strip_prefix=None, out_path=None): assert isinstance(brief, bool) + assert isinstance(strip_prefix, str) or strip_prefix is None + assert isinstance(out_path, str) or out_path is None self.brief = brief self.show_details = detailed_info self.warnings = 0 @@ -168,6 +181,27 @@ def __init__(self, brief=False, detailed_info=True): self.suppressed = 0 self.sm = None self.suppress_kind = set() + self.strip_prefix = strip_prefix + if out_path is not None: + self._owned_file = open(out_path, "w", encoding="UTF-8") # pylint: disable=consider-using-with + self.out = self._owned_file + else: + self._owned_file = None + self.out = out + + def close(self): + if self._owned_file is not None: + self._owned_file.close() + self._owned_file = None + + def __enter__(self): + return self + + def __exit__(self, *_): + self.close() + + def __del__(self): + self.close() def suppress(self, kind): assert isinstance(kind, Kind) @@ -178,8 +212,7 @@ def cross_file_reference(self, location): if self.sm is None: return location.to_string(include_column=False) - else: - return self.sm.cross_file_reference(location) + return self.sm.cross_file_reference(location) def emit(self, location, @@ -195,15 +228,21 @@ def emit(self, assert isinstance(extrainfo, str) or extrainfo is None assert isinstance(category, str) or category is None + def _loc_str(include_column=True): + loc = location.to_string(include_column) + if self.strip_prefix and loc.startswith(self.strip_prefix): + loc = loc[len(self.strip_prefix):] + return loc + if self.brief: context = None - msg = "%s: trlc %s: %s" % (location.to_string(), + msg = "%s: trlc %s: %s" % (_loc_str(), str(kind), message) else: context = location.context_lines() - msg = "%s: %s: %s" % (location.to_string(len(context) == 0), + msg = "%s: %s: %s" % (_loc_str(len(context) == 0), str(kind), message) @@ -216,10 +255,10 @@ def emit(self, else: if context: assert len(context) == 2 - print(context[0].replace("\t", " ")) - print(context[1].replace("\t", " "), msg) + print(context[0].replace("\t", " "), file=self.out) + print(context[1].replace("\t", " "), msg, file=self.out) else: - print(msg) + print(msg, file=self.out) if not self.brief \ and self.show_details \ @@ -230,7 +269,7 @@ def emit(self, indent = 0 for line in extrainfo.splitlines(): print("%s| %s" % (" " * indent, - line.rstrip())) + line.rstrip()), file=self.out) if fatal: raise TRLC_Error(location, kind, message) diff --git a/trlc/trlc.py b/trlc/trlc.py index 85fc269d..2dd0ea13 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -636,6 +636,14 @@ def trlc(): action="store_true", help=("If there are no errors, produce a summary" " naming every file processed.")) + og_output.add_argument("--log", + nargs = 2, + metavar = ("FILE", "PREFIX"), + default = None, + help = ("Write all output to FILE, strip PREFIX" + " from file paths in messages." + " Intended for use as a Bazel build" + " action.")) og_output.add_argument("--error-on-warnings", action="store_true", help=("If there are warnings, return status code" @@ -688,7 +696,10 @@ def trlc(): except subprocess.CalledProcessError: ap.error("cannot run %s" % options.use_cvc5_binary) - mh = Message_Handler(options.brief, not options.no_detailed_info) + mh = Message_Handler(options.brief, + not options.no_detailed_info, + out_path = options.log[0] if options.log else None, + strip_prefix = options.log[1] if options.log else None) if options.no_user_warnings: # pragma: no cover mh.suppress(Kind.USER_WARNING) @@ -731,6 +742,7 @@ def trlc(): ok &= sm.register_directory(".") if not ok: + mh.close() return 1 if sm.process() is None: @@ -747,7 +759,7 @@ def trlc(): if isinstance(tmp[obj.name][key], Fraction): tmp[obj.name][key] = float(tmp[obj.name][key]) - print(json.dumps(tmp, indent=2, sort_keys=True)) + print(json.dumps(tmp, indent=2, sort_keys=True), file=mh.out) total_models = len(sm.rsl_files) parsed_models = len([item @@ -791,7 +803,7 @@ def count(parsed, total, what): if mh.suppressed: # pragma: no cover summary += " with %u supressed messages" % mh.suppressed - print(summary) + print(summary, file=mh.out) if options.show_file_list and ok: # pragma: no cover def get_status(parser): @@ -807,21 +819,25 @@ def get_status(parser): print("> %s Model %s (Package %s)" % (get_status(parser), filename, - parser.cu.package.name)) + parser.cu.package.name), file=mh.out) if not options.skip_trlc_files: for filename in sorted(sm.trlc_files): parser = sm.trlc_files[filename] print("> %s Requirements %s (Package %s)" % (get_status(parser), filename, - parser.cu.package.name)) + parser.cu.package.name), file=mh.out) if ok: if options.error_on_warnings and mh.warnings \ or mh.errors: # pragma: no cover - return 1 - return 0 - return 1 + rv = 1 + else: + rv = 0 + else: + rv = 1 + mh.close() + return rv def main(): From 935d8203bc920ca0ee8a9bfc5ab9a77837512c5c Mon Sep 17 00:00:00 2001 From: Jochen Hoenle Date: Wed, 25 Feb 2026 16:24:32 +0100 Subject: [PATCH 2/2] [bazel] system tests: - setup wrapper for system tests - integrate unit tests in bazel - adapt documentation --- .bazelrc | 5 + .gitignore | 3 + BUILD | 6 + CHANGELOG.md | 17 ++- MODULE.bazel | 14 ++- MODULE.bazel.lock | 37 +----- Makefile | 6 + README.md | 2 +- bazel/_private/BUILD.bazel | 1 + bazel/_private/mode_test.py | 119 ++++++++++++++++++ bazel/_private/partial_test.bzl | 53 ++++++++ bazel/_private/system_test.bzl | 70 +++++++++++ documentation/dev_setup.md | 64 +++++++++- lobster-trlc-system-test.py | 6 +- requirements.txt.bazel | 97 ++++++++------ tests-large-partial/BUILD | 20 +++ tests-large-partial/Makefile | 7 +- tests-large-partial/partial-1.scenario | 1 - tests-large-partial/partial-1/options | 1 + .../{partial-1.output => partial-1/output} | 0 tests-large-partial/partial-2.scenario | 1 - tests-large-partial/partial-2/options | 1 + .../{partial-2.output => partial-2/output} | 0 tests-system/BUILD | 49 ++++++++ tests-system/bzl-api-deps/BUILD | 29 +++++ tests-system/bzl-api-deps/base_items.trlc | 11 ++ tests-system/bzl-api-deps/base_schema.rsl | 6 + tests-system/bzl-api-deps/ext_items.trlc | 13 ++ tests-system/bzl-api-deps/ext_schema.rsl | 6 + tests-system/bzl-api-deps/output | 1 + tests-system/bzl-api-deps/output.brief | 1 + tests-system/bzl-api-deps/output.json | 19 +++ tests-system/bzl-api-deps/output.smtlib | 1 + tests-system/bzl-api-simple/BUILD | 17 +++ tests-system/bzl-api-simple/output | 1 + tests-system/bzl-api-simple/output.brief | 1 + tests-system/bzl-api-simple/output.json | 13 ++ tests-system/bzl-api-simple/output.smtlib | 1 + tests-system/bzl-api-simple/reqs.trlc | 13 ++ tests-system/bzl-api-simple/schema.rsl | 12 ++ tests-system/bzl-api-spec-check/BUILD | 17 +++ tests-system/bzl-api-spec-check/output | 1 + tests-system/bzl-api-spec-check/output.brief | 1 + tests-system/bzl-api-spec-check/output.json | 8 ++ tests-system/bzl-api-spec-check/output.smtlib | 1 + .../bzl-api-spec-check/placeholder.trlc | 7 ++ tests-system/bzl-api-spec-check/types.rsl | 7 ++ tests-unit/BUILD.bazel | 28 +++++ trlc.bzl | 2 + trlc/errors.py | 5 +- trlc/trlc.py | 19 +-- 51 files changed, 724 insertions(+), 97 deletions(-) create mode 100644 bazel/_private/BUILD.bazel create mode 100644 bazel/_private/mode_test.py create mode 100644 bazel/_private/partial_test.bzl create mode 100644 bazel/_private/system_test.bzl create mode 100644 tests-large-partial/BUILD delete mode 100644 tests-large-partial/partial-1.scenario create mode 100644 tests-large-partial/partial-1/options rename tests-large-partial/{partial-1.output => partial-1/output} (100%) delete mode 100644 tests-large-partial/partial-2.scenario create mode 100644 tests-large-partial/partial-2/options rename tests-large-partial/{partial-2.output => partial-2/output} (100%) create mode 100644 tests-system/BUILD create mode 100644 tests-system/bzl-api-deps/BUILD create mode 100644 tests-system/bzl-api-deps/base_items.trlc create mode 100644 tests-system/bzl-api-deps/base_schema.rsl create mode 100644 tests-system/bzl-api-deps/ext_items.trlc create mode 100644 tests-system/bzl-api-deps/ext_schema.rsl create mode 100644 tests-system/bzl-api-deps/output create mode 100644 tests-system/bzl-api-deps/output.brief create mode 100644 tests-system/bzl-api-deps/output.json create mode 100644 tests-system/bzl-api-deps/output.smtlib create mode 100644 tests-system/bzl-api-simple/BUILD create mode 100644 tests-system/bzl-api-simple/output create mode 100644 tests-system/bzl-api-simple/output.brief create mode 100644 tests-system/bzl-api-simple/output.json create mode 100644 tests-system/bzl-api-simple/output.smtlib create mode 100644 tests-system/bzl-api-simple/reqs.trlc create mode 100644 tests-system/bzl-api-simple/schema.rsl create mode 100644 tests-system/bzl-api-spec-check/BUILD create mode 100644 tests-system/bzl-api-spec-check/output create mode 100644 tests-system/bzl-api-spec-check/output.brief create mode 100644 tests-system/bzl-api-spec-check/output.json create mode 100644 tests-system/bzl-api-spec-check/output.smtlib create mode 100644 tests-system/bzl-api-spec-check/placeholder.trlc create mode 100644 tests-system/bzl-api-spec-check/types.rsl create mode 100644 tests-unit/BUILD.bazel diff --git a/.bazelrc b/.bazelrc index 1b899988..ccb3993f 100644 --- a/.bazelrc +++ b/.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[/:]" diff --git a/.gitignore b/.gitignore index c067b8d3..f75186ec 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,13 @@ # Project ignores docs +htmlcov .coverage* *.lobster # Python ignores *.pyc +__pycache__ +.ruff_cache *.egg-info .venv/ venv/ diff --git a/BUILD b/BUILD index 75d74775..19cf02e2 100644 --- a/BUILD +++ b/BUILD @@ -57,3 +57,9 @@ alias( name = "format.fix", actual = "//tools/format:format", ) + +filegroup( + name = "coverage", + srcs = ["coverage.cfg"], + visibility = ["//visibility:public"], +) diff --git a/CHANGELOG.md b/CHANGELOG.md index 27b34be4..db8a98f1 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/MODULE.bazel b/MODULE.bazel index 7c16eaf6..7cc6d3d1 100644 --- a/MODULE.bazel +++ b/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", ) diff --git a/MODULE.bazel.lock b/MODULE.bazel.lock index 1fd082b0..2c918605 100644 --- a/MODULE.bazel.lock +++ b/MODULE.bazel.lock @@ -685,7 +685,7 @@ "usagesDigest": "B9WByXMQOeCDEjtpOkG/1hz+Pl4i2Pyiw1BRraLz0zk=", "recordedFileInputs": { "@@//requirements.txt": "3fbbc32af771695c98b9f794b0513f0809c342b973aa0d4005727965af158b8f", - "@@//requirements_dev_lock.txt": "4859f25307badbe8aaad7b49426c9336cfb60a09a326027e16f780d1573279f3", + "@@//requirements_dev_lock.txt": "02f3ced94521bd20df5fa3b866ca6f83f381538df4748c388ff38336a1d6901f", "@@protobuf+//python/requirements.txt": "983be60d3cec4b319dcab6d48aeb3f5b2f7c3350f26b3a9e97486c37967c73c5", "@@rules_fuzzing+//fuzzing/requirements.txt": "ab04664be026b632a0d2a2446c4f65982b7654f5b6851d2f9d399a19b7242a5b", "@@rules_python+//tools/publish/requirements_darwin.txt": "095d4a4f3d639dce831cd493367631cd51b53665292ab20194bac2c0c6458fa8", @@ -3330,15 +3330,6 @@ "requirement": "cvc5==1.3.2 --hash=sha256:04174c5cd3c858c972792debc96436632635db2f8c4098806cc7aa51a8de2920 --hash=sha256:13759b6b50d46aa79e3a75e8979b8f36d5eb3fbce9430c5de5ee014ab202344a --hash=sha256:1b1cee4e49db78d8053a509109cede9e768fb3353c3662f72cd28b3a2fb73762 --hash=sha256:1d8bd54142131346a127ec9eebda155c961c05489909d6f16a5c29f1b38d6030 --hash=sha256:2109a1577b9f62f79dd72f8d8eb06db9e51eb2a6b9e84abf79865e1694dd1a59 --hash=sha256:25bcf19294cb166fc4a4f4b5c77379707706f9fc215ecf581328050ada4865fc --hash=sha256:298ac4ab00d54aadde83cfd21fe886177446523bc0d4ace4bb3eb9b300f8611d --hash=sha256:29d4c28e3399244b8df7c9e5154f3f8c47fcf9720dbd2dd38b2c59abc8b40e51 --hash=sha256:2ab5ce33c38229c7c02d7190f9da4d99bf016a5d066be6d5b71d99747c334bd4 --hash=sha256:30565c03228b4eed78d21fbc86130f0b9c7b4454eec4364b0bc62f1a01f2266b --hash=sha256:31782354a51464d98bc8f64fdb2db148365e584954eee2f9e7b3eaedc5722f81 --hash=sha256:31ca0e5ba1592c85459f40e8559bc07dea1fcf7d59074a2abd07e3f2abf0ddf5 --hash=sha256:31d6f9265232fdf4d413d25a446210f14d6d08fc697f4ce5c6f2e878331cceb7 --hash=sha256:3b63586503d90628fda73f6f8f3ddabd73bebb7fb93bc369beecd4c389d999dc --hash=sha256:3baef0cef04cd4c956e91aab2c6937b0930f7c4d98454b11dc8a33f13a25e7b3 --hash=sha256:3e2a1ba179ac76d3ce3b973cf99d4a1368cf5b69ce8952163d668a08e6d76b1c --hash=sha256:40938b5a7551ec0850d3945ed54a3249cb9d00fba7a4eec360e81e2a1f5cc1e5 --hash=sha256:420e3b389d12df6650ff8781d297762edbaad35eb1946e72fdf2b713a0088ad0 --hash=sha256:43301779da3d09d5159f0950cc99e93a814dc366a5b0af913a3d4c1ffb2f54a8 --hash=sha256:4544943cbf58d7130773f2026399c27eb9410d6a739b77ce730339f82c82243e --hash=sha256:49602b38f3c9789d8052c2ff598f43f661efa226fc4487cfdb03cc05f20b95d2 --hash=sha256:4a50718aac4030e3be48744f2419a5609c17553495822c841164fa10811fd426 --hash=sha256:4c16e8238152e34a12c742a6c97909dab551f5ff775d1b6b872f2993d0192760 --hash=sha256:59fdb1c2cc84d2875de228873b38b3a8a6af13ee8e6d87a963045c1f4ca8df00 --hash=sha256:5f22deab1feb6b5c594cdff174781a8ce44a9b9061b386918eb426203cd0133c --hash=sha256:62144306406721ef1b0d1d060ecb1b31624e98d1eeb2ed886b2f1673d04d6fc4 --hash=sha256:64e9160cd89cb415bade28ec35e8521b187f698ca332c4276bf1cfdddfdc6660 --hash=sha256:7390831bd32067c263fd78485cf1413cf5ccd635df3cfc391138368c90b78356 --hash=sha256:794aca0e5b57b0bdf707ca2c6f46072e7d90cf04470685a07eeafd395bd8acb8 --hash=sha256:7af4c8cc835ed32aa6190585b888a7e49a90e491152b3229c2ba3ad1306eb7c7 --hash=sha256:7b0b2eff94641f413bbeb172b54cfd0ac2a26c2c6bb79d41d18df1bc4a8ecb0c --hash=sha256:7bbe7f1a6949aed2eb059794697d9a25afc13efbeb1a729d5c327971a45a05b9 --hash=sha256:7e2a39dc267caacfa0f1fb23844c6cc58ddeeef9b1417d7e5e3ca1f51ac68e5f --hash=sha256:878d73ccd8b7dcd17a5f5e9750bc45f4b7da5ed07dd36a77cb8369d089883540 --hash=sha256:912e4de05eda1fa86f707eda932f1bd9e8d8a6316a28458fd57334d2f8f104f9 --hash=sha256:92dc62facddffd7c08be9048f42cbc0283544918a8db770cadab04041c176b11 --hash=sha256:9534ffd384356db74b83818f41ab9da58f8c7dc7551ae81a11ad624a7f519844 --hash=sha256:9b962b21635f83b46bd9a82d4f33f5e7d960b40b8b2eabad43f82172bcaaa659 --hash=sha256:aa2ea64dd6bee47c3a3a0606de014f7f60acabb0eb5282404aa12e990910b656 --hash=sha256:b1946ebe0f5990431d4d0569839813d0165b5299c95f486e5064b0c4454f4977 --hash=sha256:c77cadfde393d7949bda2a48f3d4c2a6f572cb0bc2147159212c29913c5a8c56 --hash=sha256:c7ac86cc4e68b732a4f9f80cdcacc085c3e11bb2aeef7c3138f2eb1fbef83a09 --hash=sha256:c8d897f85d3b9014df8d5320925b2c3b19bfd11d49667660e385ae673656de8a --hash=sha256:ce5efe02238e63df935a3fc737c4f059797acfd9282b74c37d8fd01473691ebf --hash=sha256:d10a263214327f086bbb3825029135f6224c4b0498997a4817a4f7af29de2a9b --hash=sha256:d208c9eda9f0279cc31e36f5af2b7c057749b267f1766bd4a1f1c4aefe646218 --hash=sha256:d94b9f2a3c51720e60798ca0995debac8aa967d374a29d0a25e346d05429a409 --hash=sha256:d9c3e89bf650ffa2c9ab6bb63a7229d7bce8d7ba880655a73878d8a9fb3716d5 --hash=sha256:dbaa132c67daa6513aa94ab96406db258dcc41bc3fd5ce68019beebdc9fb280b --hash=sha256:f1f0209a641723c33c94c4998cd56fc085a0ae136932680cd8e1995e94430d48 --hash=sha256:f1ffd51587c2de76242e1857bc27dc482da8801391cd968f00d106de60473297 --hash=sha256:f2671232073e45c84c1f0c807b9c398b1e321b695d031a4a61f2c4ae4664c797 --hash=sha256:f37f25713d0dff3653d7e04668d1733d003855a735fc63d3666dcd2fbde0dca5 --hash=sha256:f7f410e513b4ca7c8e36cf8b3293de09841ec32825c4c073c9a802023a528108 --hash=sha256:f850dbcaffab3f3b3265ed17425db5f5dc841f9a8f5c5fa74bff02cebc198ed6 --hash=sha256:fb4146591032ff9e542f126ed51def92bc88aa1315ce400b16c0d56e773d5a7a --hash=sha256:ff41096837dbd0b09e9565bb5bf273a444bb0dff9331a1e90cb6c8876500928e" } }, - "trlc_dev_dependencies_312_dill": { - "repoRuleId": "@@rules_python+//python/private/pypi:whl_library.bzl%whl_library", - "attributes": { - "dep_template": "@trlc_dev_dependencies//{name}:{target}", - "python_interpreter_target": "@@rules_python++python+python_3_12_host//:python", - "repo": "trlc_dev_dependencies_312", - "requirement": "dill==0.4.1 --hash=sha256:1e1ce33e978ae97fcfcff5638477032b801c46c7c65cf717f95fbc2248f79a9d --hash=sha256:423092df4182177d4d8ba8290c8a5b640c66ab35ec7da59ccfa00f6fa3eea5fa" - } - }, "trlc_dev_dependencies_312_docutils": { "repoRuleId": "@@rules_python+//python/private/pypi:whl_library.bzl%whl_library", "attributes": { @@ -3411,15 +3402,6 @@ "requirement": "packaging==26.0 --hash=sha256:00243ae351a257117b6a241061796684b084ed1c516a08c48a3f7e147a9d80b4 --hash=sha256:b36f1fef9334a5588b4166f8bcd26a14e521f2b55e6b9de3aaa80d3ff7a37529" } }, - "trlc_dev_dependencies_312_platformdirs": { - "repoRuleId": "@@rules_python+//python/private/pypi:whl_library.bzl%whl_library", - "attributes": { - "dep_template": "@trlc_dev_dependencies//{name}:{target}", - "python_interpreter_target": "@@rules_python++python+python_3_12_host//:python", - "repo": "trlc_dev_dependencies_312", - "requirement": "platformdirs==4.9.2 --hash=sha256:9170634f126f8efdae22fb58ae8a0eaa86f38365bc57897a6c4f781d1f5875bd --hash=sha256:9a33809944b9db043ad67ca0db94b14bf452cc6aeaac46a88ea55b26e2e9d291" - } - }, "trlc_dev_dependencies_312_pycodestyle": { "repoRuleId": "@@rules_python+//python/private/pypi:whl_library.bzl%whl_library", "attributes": { @@ -3444,7 +3426,7 @@ "dep_template": "@trlc_dev_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_12_host//:python", "repo": "trlc_dev_dependencies_312", - "requirement": "pylint==4.0.5 --hash=sha256:00f51c9b14a3b3ae08cff6b2cdd43f28165c78b165b628692e428fb1f8dc2cf2 --hash=sha256:8cd6a618df75deb013bd7eb98327a95f02a6fb839205a6bbf5456ef96afb317c" + "requirement": "pylint==2.3.0 --hash=sha256:2bf4bd58d6d5d87174fbc9d1d134a9aeee852d4dc29cbd422a7015772770bc63 --hash=sha256:ee80c7af4f127b2a480d83010c9f0e97beb8eaa652b78c2837d3ed30b12e1182" } }, "trlc_dev_dependencies_312_pyproject_hooks": { @@ -3555,15 +3537,6 @@ "requirement": "sphinxcontrib-serializinghtml==2.0.0 --hash=sha256:6e2cb0eef194e10c27ec0023bfeb25badbbb5868244cf5bc5bdc04e4464bf331 --hash=sha256:e9d912827f872c029017a53f0ef2180b327c3f7fd23c87229f7a8e8b70031d4d" } }, - "trlc_dev_dependencies_312_tomlkit": { - "repoRuleId": "@@rules_python+//python/private/pypi:whl_library.bzl%whl_library", - "attributes": { - "dep_template": "@trlc_dev_dependencies//{name}:{target}", - "python_interpreter_target": "@@rules_python++python+python_3_12_host//:python", - "repo": "trlc_dev_dependencies_312", - "requirement": "tomlkit==0.14.0 --hash=sha256:592064ed85b40fa213469f81ac584f67a4f2992509a7c3ea2d632208623a3680 --hash=sha256:cf00efca415dbd57575befb1f6634c4f42d2d87dbba376128adb42c121b87064" - } - }, "trlc_dev_dependencies_312_urllib3": { "repoRuleId": "@@rules_python+//python/private/pypi:whl_library.bzl%whl_library", "attributes": { @@ -3701,7 +3674,6 @@ "charset_normalizer": "{\"trlc_dev_dependencies_312_charset_normalizer\":[{\"version\":\"3.12\"}]}", "coverage": "{\"trlc_dev_dependencies_312_coverage\":[{\"version\":\"3.12\"}]}", "cvc5": "{\"trlc_dev_dependencies_312_cvc5\":[{\"version\":\"3.12\"}]}", - "dill": "{\"trlc_dev_dependencies_312_dill\":[{\"version\":\"3.12\"}]}", "docutils": "{\"trlc_dev_dependencies_312_docutils\":[{\"version\":\"3.12\"}]}", "idna": "{\"trlc_dev_dependencies_312_idna\":[{\"version\":\"3.12\"}]}", "imagesize": "{\"trlc_dev_dependencies_312_imagesize\":[{\"version\":\"3.12\"}]}", @@ -3710,7 +3682,6 @@ "markupsafe": "{\"trlc_dev_dependencies_312_markupsafe\":[{\"version\":\"3.12\"}]}", "mccabe": "{\"trlc_dev_dependencies_312_mccabe\":[{\"version\":\"3.12\"}]}", "packaging": "{\"trlc_dev_dependencies_312_packaging\":[{\"version\":\"3.12\"}]}", - "platformdirs": "{\"trlc_dev_dependencies_312_platformdirs\":[{\"version\":\"3.12\"}]}", "pycodestyle": "{\"trlc_dev_dependencies_312_pycodestyle\":[{\"version\":\"3.12\"}]}", "pygments": "{\"trlc_dev_dependencies_312_pygments\":[{\"version\":\"3.12\"}]}", "pylint": "{\"trlc_dev_dependencies_312_pylint\":[{\"version\":\"3.12\"}]}", @@ -3726,7 +3697,6 @@ "sphinxcontrib_jsmath": "{\"trlc_dev_dependencies_312_sphinxcontrib_jsmath\":[{\"version\":\"3.12\"}]}", "sphinxcontrib_qthelp": "{\"trlc_dev_dependencies_312_sphinxcontrib_qthelp\":[{\"version\":\"3.12\"}]}", "sphinxcontrib_serializinghtml": "{\"trlc_dev_dependencies_312_sphinxcontrib_serializinghtml\":[{\"version\":\"3.12\"}]}", - "tomlkit": "{\"trlc_dev_dependencies_312_tomlkit\":[{\"version\":\"3.12\"}]}", "urllib3": "{\"trlc_dev_dependencies_312_urllib3\":[{\"version\":\"3.12\"}]}" }, "packages": [ @@ -3738,7 +3708,6 @@ "charset_normalizer", "coverage", "cvc5", - "dill", "docutils", "idna", "imagesize", @@ -3747,7 +3716,6 @@ "markupsafe", "mccabe", "packaging", - "platformdirs", "pycodestyle", "pygments", "pylint", @@ -3763,7 +3731,6 @@ "sphinxcontrib_jsmath", "sphinxcontrib_qthelp", "sphinxcontrib_serializinghtml", - "tomlkit", "urllib3" ], "groups": {} diff --git a/Makefile b/Makefile index 1dd0752d..78f79416 100644 --- a/Makefile +++ b/Makefile @@ -12,21 +12,26 @@ 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 \ @@ -34,6 +39,7 @@ system-tests: 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 \ diff --git a/README.md b/README.md index 5db9232d..431c2d33 100644 --- a/README.md +++ b/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). diff --git a/bazel/_private/BUILD.bazel b/bazel/_private/BUILD.bazel new file mode 100644 index 00000000..04385fe7 --- /dev/null +++ b/bazel/_private/BUILD.bazel @@ -0,0 +1 @@ +exports_files(["mode_test.py"]) diff --git a/bazel/_private/mode_test.py b/bazel/_private/mode_test.py new file mode 100644 index 00000000..4c219309 --- /dev/null +++ b/bazel/_private/mode_test.py @@ -0,0 +1,119 @@ +"""System test runner – runs all modes for one test directory. + +Arguments are supplied by the ``trlc_system_test`` / ``trlc_partial_test`` +macro via Bazel ``args`` on the ``py_test`` target: + + sys.argv[1] root_dir -- workspace-relative path of the test root, + e.g. "tests-system" or "tests-large-partial" + sys.argv[2] test_dir -- subdirectory name within root_dir + sys.argv[3] cvc5_rloc -- runfiles-relative path of the cvc5 binary + +Available modes are discovered at runtime by listing the ``output*`` golden +files present in the test directory. An optional ``options`` file in the +directory may supply extra trlc flags (whitespace-separated), e.g. +``--no-detailed-info`` or source paths for partial-loading tests. + +Path resolution uses only standard Bazel test environment variables +(https://bazel.build/reference/test-encyclopedia): + + TEST_SRCDIR -- absolute path to the base of the runfiles tree (required) + TEST_WORKSPACE -- local repository workspace name (optional) + TEST_TMPDIR -- private writable directory for test output (required) +""" + +import difflib +import os +import sys + +_ROOT_DIR = sys.argv[1] +_TEST_DIR = sys.argv[2] +_CVC5_RLOC = sys.argv[3] + + +def _srcdir(*parts): + """Resolve a path inside the runfiles tree via TEST_SRCDIR.""" + workspace = os.environ.get("TEST_WORKSPACE", "_main") + return os.path.join(os.environ["TEST_SRCDIR"], workspace, *parts) + + +def _get_modes(): + """Return the list of modes to run, derived from golden files present.""" + test_src = _srcdir(_ROOT_DIR, _TEST_DIR) + return sorted(f for f in os.listdir(test_src) if f.startswith("output")) + + +def _get_extra_args(): + """Return extra trlc flags from the optional ``options`` file, or ``[]``.""" + options_path = _srcdir(_ROOT_DIR, _TEST_DIR, "options") + if os.path.isfile(options_path): + with open(options_path, encoding="UTF-8") as fh: + return fh.read().split() + return [] + + +def _run_mode(mode): + """Run trlc for *mode* and return a diff string, or None on success.""" + # Import inside the function so that coverage instruments trlc. + from trlc.trlc import trlc # noqa: PLC0415 + + root = _srcdir(_ROOT_DIR) + sources = _srcdir(_ROOT_DIR, _TEST_DIR) + os.sep + golden_path = _srcdir(_ROOT_DIR, _TEST_DIR, mode) + actual_path = os.path.join(os.environ["TEST_TMPDIR"], "actual_" + mode) + + # chdir to root so that relative paths in options files (e.g. + # "large/pkg.trlc" in tests-large-partial) resolve correctly. + os.chdir(root) + + args = ["trlc"] + + if mode in ("output", "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"] + elif mode == "output.json": + args += ["--no-lint", "--debug-api-dump"] + + args.extend(_get_extra_args()) + args.append(sources) + + # Add logging configuration last so --log only consumes FILE and optional PREFIX. + args.extend(["--log", actual_path, root + os.sep]) + + sys.argv = args + trlc() + + with open(actual_path, encoding="UTF-8") as fh: + actual = fh.read() + with open(golden_path, encoding="UTF-8") as fh: + golden = fh.read() + + if actual == golden: + return None + return "".join( + difflib.unified_diff( + golden.splitlines(keepends=True), + actual.splitlines(keepends=True), + fromfile="golden (%s/%s)" % (_TEST_DIR, mode), + tofile="actual", + ) + ) + + +failed = [] +for _mode in _get_modes(): + diff = _run_mode(_mode) + if diff is not None: + print(diff, file=sys.stderr) + failed.append(_mode) + +if failed: + print("FAILED modes: %s" % ", ".join(failed), file=sys.stderr) + sys.exit(1) diff --git a/bazel/_private/partial_test.bzl b/bazel/_private/partial_test.bzl new file mode 100644 index 00000000..775b9a99 --- /dev/null +++ b/bazel/_private/partial_test.bzl @@ -0,0 +1,53 @@ +"""Bazel macro for tests-large-partial/ golden-file tests. + +``trlc_partial_test(test_name)`` creates one ``native.py_test`` that reuses +the shared ``mode_test.py`` runner from ``//bazel/_private``. + +The test subdirectory must contain: + +* ``output`` -- golden output (only this one mode is checked) +* ``options`` -- extra trlc flags, e.g. ``--show-file-list -I large large/pkg.trlc`` + (paths are relative to ``tests-large-partial/``) + +Args forwarded via Bazel ``args`` to ``mode_test.py``: + +.. code-block:: text + + argv[1] root_dir "tests-large-partial" + argv[2] test_dir plain string, e.g. "partial-1" + argv[3] cvc5_rloc $(rlocationpath //:cvc5) +""" + +def trlc_partial_test(test_name): + """Create a golden-file py_test for a tests-large-partial/ subdirectory. + + Args: + test_name: subdirectory name, e.g. ``"partial-1"``. + """ + srcs = native.glob([test_name + "/**"]) + + # NOTE: the py_test must NOT be named test_name because Bazel would create + # a runfiles symlink tests-large-partial/ -> bazel-out/…/ + # that obscures the source-directory symlinks for the golden files inside + # it. The "_test" suffix avoids that collision. A test_suite under the + # plain name preserves the short invocation style. + test_target = test_name + "_test" + + native.py_test( + name = test_target, + srcs = ["//bazel/_private:mode_test.py"], + main = "mode_test.py", + args = [ + "tests-large-partial", + test_name, + "$(rlocationpath //:cvc5)", + ], + deps = ["//trlc:trlc"], + data = list(srcs) + native.glob(["large/**"]) + ["//:cvc5", "//:coverage"], + size = "large", + ) + + native.test_suite( + name = test_name, + tests = [":" + test_target], + ) diff --git a/bazel/_private/system_test.bzl b/bazel/_private/system_test.bzl new file mode 100644 index 00000000..c9dcb9c0 --- /dev/null +++ b/bazel/_private/system_test.bzl @@ -0,0 +1,70 @@ +"""File system test runner for the trlc repository. + +``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. +""" + +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) + + 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/ -> bazel-out/…/ + # 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: + # invocation. + test_target = test_dir + "_test" + + native.py_test( + name = test_target, + srcs = ["//bazel/_private:mode_test.py"], + main = "mode_test.py", + args = [ + "tests-system", + test_dir, + "$(rlocationpath //:cvc5)", + ], + deps = ["//trlc:trlc"], + data = list(srcs) + ["//:cvc5", "//:coverage"], + ) + + native.test_suite( + name = test_dir, + tests = [":" + test_target], + ) diff --git a/documentation/dev_setup.md b/documentation/dev_setup.md index 3b2cf673..a7f9e632 100644 --- a/documentation/dev_setup.md +++ b/documentation/dev_setup.md @@ -14,7 +14,7 @@ the latest GNU make version. * You also need an executable `cvc5` binary on your PATH. Download the appropriate version from - https://github.com/cvc5/cvc5/releases/tag/cvc5-1.0.8 and rename + https://github.com/cvc5/cvc5/releases/tag/cvc5-1.3.2 and rename it. You can also build CVC5 from source if there is no pre-built release available for your platform. @@ -107,3 +107,65 @@ bazel run //:format.fix # Run all linters (pylint + ty) over every Python target bazel build --config=lint //... ``` + +## Running system tests via Bazel + +The system tests in `tests-system/` can be run as Bazel test +actions. Test directories are discovered **automatically** via +`native.glob` — no manual list to maintain. + +```bash +# Run all system tests (excludes "bulk") +bazel test //tests-system:fast + +# Run all system tests including bulk +bazel test //tests-system:all_tests + +# Run a single test directory +bazel test //tests-system:checks-1 + +``` + +### Adding a new system test + +1. Create the directory `tests-system//` with the usual TRLC + source files and golden files (`output`, `output.brief`, + `output.json`; optionally `output.smtlib`). +2. If the test requires `--no-detailed-info` (or any other trlc flag), + add an `options` file containing those flags (whitespace-separated). + The test runner reads this file automatically — no BUILD change is + needed. +3. Bazel picks up the new directory on the next build. No changes to + `tests-system/BUILD` are required. + +### Running the large partial-loading tests via Bazel + +The tests in `tests-large-partial/` exercise partial-loading of large +TRLC files: + +```bash +# Run all partial tests +bazel test //tests-large-partial:partial_tests + +# Run a single partial test +bazel test //tests-large-partial:partial-1 +``` + +New partial tests are picked up automatically — just add a +`.scenario` / `.output` pair in `tests-large-partial/`. + +## Coverage via Bazel + +The system tests run trlc in-process as `py_test` targets, so Bazel can +instrument the trlc library code with `coverage.py` automatically. + +```bash +# Collect coverage across all system tests and api-examples +bazel coverage //tests-system/... + +# Render as HTML (requires lcov / genhtml) +genhtml "$(bazel info output_path)/_coverage/_coverage_report.dat" -o htmlcov +``` + +The `coverage` namespace in `.bazelrc` sets `--combined_report=lcov` and +`--instrumentation_filter=//trlc[/:]` so only the trlc library is measured. diff --git a/lobster-trlc-system-test.py b/lobster-trlc-system-test.py index 878c2685..9f4b4f1a 100755 --- a/lobster-trlc-system-test.py +++ b/lobster-trlc-system-test.py @@ -23,9 +23,9 @@ import os import sys -from lobster.common.items import Tracing_Tag, Activity -from lobster.common.location import File_Reference -from lobster.common.io import lobster_write +from lobster.common.items import Tracing_Tag, Activity # pylint: disable=import-error +from lobster.common.location import File_Reference # pylint: disable=import-error +from lobster.common.io import lobster_write # pylint: disable=import-error from trlc.trlc import Source_Manager from trlc.errors import Message_Handler diff --git a/requirements.txt.bazel b/requirements.txt.bazel index 635b9838..3c62573e 100644 --- a/requirements.txt.bazel +++ b/requirements.txt.bazel @@ -1,42 +1,69 @@ # -# This file is autogenerated by pip-compile with Python 3.11 +# This file is autogenerated by pip-compile with Python 3.12 # by the following command: # # bazel run //:requirements.update # -cvc5==1.1.2 ; sys_platform == "linux" or sys_platform == "darwin" \ - --hash=sha256:06417fcb14968378013b522c67a7e3b88e032d9689e160fa28b3a9aa5af820f5 \ - --hash=sha256:13430b08dd96b06818a1696e824ba045077265e1b34378bf86c6ced83ab3a302 \ - --hash=sha256:15160cbb21d2df205ba688aba6eff5af1434ce8297c82924b619879f07354784 \ - --hash=sha256:26b26ff66a85a45c0fd03c19778ceb3c3b17837fcf222dbf78bd819e87b33078 \ - --hash=sha256:3c3f428c0ff8379db0f3e15bd74318a9b1984fbc626dc800856983cae1d5b345 \ - --hash=sha256:40eda8d888b6dbced3e73fe2a38cd930a4b48f67880169544969072d4196d7b5 \ - --hash=sha256:4eb3fb7d829ad6a4d70e837e82647ba978cb343555a459b866a2647ff42ae8e4 \ - --hash=sha256:4fa4075ddb8e5a6c6b1d1e50267689cccfe527e8707261b2a82a748b4425c7f6 \ - --hash=sha256:53c77150cfd521f8836a70446a75c5a9398bd2d49b0f5e60f259e348cfba99b2 \ - --hash=sha256:6ee4e08df71f38999acddf9fa449464791fc41c9d6f273300d4d5d232bcf494d \ - --hash=sha256:6fe8c6b657e919e395b82e00ab0cd3f1c2159bec9794ae44e30293c13cbefa20 \ - --hash=sha256:77e4a4b6cb609ffb4b037d7f1830f1c6638a18af8df0478cee10894235556d49 \ - --hash=sha256:7faacb9020487ce725e84a9f96e4e8d0a6ab0ca21cf2bff56f5a6642493a1058 \ - --hash=sha256:81a56af2689e89ffd883271ee2ace88c1b60dfe979f9502e2429a3f9a00b9c26 \ - --hash=sha256:8abfa8f34b3cd8905f5f2cddf7383bed0695f24e70c0131e899ab8634ffcd1a6 \ - --hash=sha256:94bdfb9b0b81fa3c6b5c6ee86b03a8755c0088d7ca01a815b3aa2633bad837f3 \ - --hash=sha256:97313d85ae96a541f120e7cc40ac908084998d460a4a7eac89d84b808985faee \ - --hash=sha256:bb46c61deebc73aa181b7cb7081c31d02d1628b242ddb8eb09b137d3aa438c79 \ - --hash=sha256:c1e2f3cf0ec6097da97c29e4cef2a0fbd912ea5e3031a98ef89c017f3f7a59b6 \ - --hash=sha256:cfb76c3a2737cccfda494f442b8686d026f76b5b13c4689f191d9db89efa8aef \ - --hash=sha256:d2bf0aa6c7eb4b240301f1d22315fdf2ec792e17a010c92717c0626189c44878 \ - --hash=sha256:d4694bd0700e2a85743fb64d8b041cd490840e77295e3c907a06e3d73cd6d3c5 \ - --hash=sha256:d9cffdfcc40d6c8cb8a36b75e8fe20e35fda46053ff99135fbffc6f086f97fcf \ - --hash=sha256:dc9ff5725237c1b8699636a13e533a2c4988cf32c18c7d3a89af54571ddfb315 \ - --hash=sha256:e2eb8a93902e361796c085337480b249338971a3f1df5655142289ace8a6263c \ - --hash=sha256:e3a4ae547a593469edd6f9cdfa17e8dac2e12e5a27376f919c4f2d62bf3ecbcd \ - --hash=sha256:e7801cebba7021e5716ccf373a96266470e0c5cdc4ee94e477083df106b3798c \ - --hash=sha256:e9612d5b21036e8d09b0db6f4206920364686501a9bfc157a1ed712477ec032d \ - --hash=sha256:f7527ba92b7804c06b7a8c9450cc814977fe47d8b81ee3c11ba49b1730ec847a \ - --hash=sha256:fb7e3e82157894f1d03109795350fed7195fe078177d09e1e232701834bf0878 +cvc5==1.3.2 \ + --hash=sha256:04174c5cd3c858c972792debc96436632635db2f8c4098806cc7aa51a8de2920 \ + --hash=sha256:13759b6b50d46aa79e3a75e8979b8f36d5eb3fbce9430c5de5ee014ab202344a \ + --hash=sha256:1b1cee4e49db78d8053a509109cede9e768fb3353c3662f72cd28b3a2fb73762 \ + --hash=sha256:1d8bd54142131346a127ec9eebda155c961c05489909d6f16a5c29f1b38d6030 \ + --hash=sha256:2109a1577b9f62f79dd72f8d8eb06db9e51eb2a6b9e84abf79865e1694dd1a59 \ + --hash=sha256:25bcf19294cb166fc4a4f4b5c77379707706f9fc215ecf581328050ada4865fc \ + --hash=sha256:298ac4ab00d54aadde83cfd21fe886177446523bc0d4ace4bb3eb9b300f8611d \ + --hash=sha256:29d4c28e3399244b8df7c9e5154f3f8c47fcf9720dbd2dd38b2c59abc8b40e51 \ + --hash=sha256:2ab5ce33c38229c7c02d7190f9da4d99bf016a5d066be6d5b71d99747c334bd4 \ + --hash=sha256:30565c03228b4eed78d21fbc86130f0b9c7b4454eec4364b0bc62f1a01f2266b \ + --hash=sha256:31782354a51464d98bc8f64fdb2db148365e584954eee2f9e7b3eaedc5722f81 \ + --hash=sha256:31ca0e5ba1592c85459f40e8559bc07dea1fcf7d59074a2abd07e3f2abf0ddf5 \ + --hash=sha256:31d6f9265232fdf4d413d25a446210f14d6d08fc697f4ce5c6f2e878331cceb7 \ + --hash=sha256:3b63586503d90628fda73f6f8f3ddabd73bebb7fb93bc369beecd4c389d999dc \ + --hash=sha256:3baef0cef04cd4c956e91aab2c6937b0930f7c4d98454b11dc8a33f13a25e7b3 \ + --hash=sha256:3e2a1ba179ac76d3ce3b973cf99d4a1368cf5b69ce8952163d668a08e6d76b1c \ + --hash=sha256:40938b5a7551ec0850d3945ed54a3249cb9d00fba7a4eec360e81e2a1f5cc1e5 \ + --hash=sha256:420e3b389d12df6650ff8781d297762edbaad35eb1946e72fdf2b713a0088ad0 \ + --hash=sha256:43301779da3d09d5159f0950cc99e93a814dc366a5b0af913a3d4c1ffb2f54a8 \ + --hash=sha256:4544943cbf58d7130773f2026399c27eb9410d6a739b77ce730339f82c82243e \ + --hash=sha256:49602b38f3c9789d8052c2ff598f43f661efa226fc4487cfdb03cc05f20b95d2 \ + --hash=sha256:4a50718aac4030e3be48744f2419a5609c17553495822c841164fa10811fd426 \ + --hash=sha256:4c16e8238152e34a12c742a6c97909dab551f5ff775d1b6b872f2993d0192760 \ + --hash=sha256:59fdb1c2cc84d2875de228873b38b3a8a6af13ee8e6d87a963045c1f4ca8df00 \ + --hash=sha256:5f22deab1feb6b5c594cdff174781a8ce44a9b9061b386918eb426203cd0133c \ + --hash=sha256:62144306406721ef1b0d1d060ecb1b31624e98d1eeb2ed886b2f1673d04d6fc4 \ + --hash=sha256:64e9160cd89cb415bade28ec35e8521b187f698ca332c4276bf1cfdddfdc6660 \ + --hash=sha256:7390831bd32067c263fd78485cf1413cf5ccd635df3cfc391138368c90b78356 \ + --hash=sha256:794aca0e5b57b0bdf707ca2c6f46072e7d90cf04470685a07eeafd395bd8acb8 \ + --hash=sha256:7af4c8cc835ed32aa6190585b888a7e49a90e491152b3229c2ba3ad1306eb7c7 \ + --hash=sha256:7b0b2eff94641f413bbeb172b54cfd0ac2a26c2c6bb79d41d18df1bc4a8ecb0c \ + --hash=sha256:7bbe7f1a6949aed2eb059794697d9a25afc13efbeb1a729d5c327971a45a05b9 \ + --hash=sha256:7e2a39dc267caacfa0f1fb23844c6cc58ddeeef9b1417d7e5e3ca1f51ac68e5f \ + --hash=sha256:878d73ccd8b7dcd17a5f5e9750bc45f4b7da5ed07dd36a77cb8369d089883540 \ + --hash=sha256:912e4de05eda1fa86f707eda932f1bd9e8d8a6316a28458fd57334d2f8f104f9 \ + --hash=sha256:92dc62facddffd7c08be9048f42cbc0283544918a8db770cadab04041c176b11 \ + --hash=sha256:9534ffd384356db74b83818f41ab9da58f8c7dc7551ae81a11ad624a7f519844 \ + --hash=sha256:9b962b21635f83b46bd9a82d4f33f5e7d960b40b8b2eabad43f82172bcaaa659 \ + --hash=sha256:aa2ea64dd6bee47c3a3a0606de014f7f60acabb0eb5282404aa12e990910b656 \ + --hash=sha256:b1946ebe0f5990431d4d0569839813d0165b5299c95f486e5064b0c4454f4977 \ + --hash=sha256:c77cadfde393d7949bda2a48f3d4c2a6f572cb0bc2147159212c29913c5a8c56 \ + --hash=sha256:c7ac86cc4e68b732a4f9f80cdcacc085c3e11bb2aeef7c3138f2eb1fbef83a09 \ + --hash=sha256:c8d897f85d3b9014df8d5320925b2c3b19bfd11d49667660e385ae673656de8a \ + --hash=sha256:ce5efe02238e63df935a3fc737c4f059797acfd9282b74c37d8fd01473691ebf \ + --hash=sha256:d10a263214327f086bbb3825029135f6224c4b0498997a4817a4f7af29de2a9b \ + --hash=sha256:d208c9eda9f0279cc31e36f5af2b7c057749b267f1766bd4a1f1c4aefe646218 \ + --hash=sha256:d94b9f2a3c51720e60798ca0995debac8aa967d374a29d0a25e346d05429a409 \ + --hash=sha256:d9c3e89bf650ffa2c9ab6bb63a7229d7bce8d7ba880655a73878d8a9fb3716d5 \ + --hash=sha256:dbaa132c67daa6513aa94ab96406db258dcc41bc3fd5ce68019beebdc9fb280b \ + --hash=sha256:f1f0209a641723c33c94c4998cd56fc085a0ae136932680cd8e1995e94430d48 \ + --hash=sha256:f1ffd51587c2de76242e1857bc27dc482da8801391cd968f00d106de60473297 \ + --hash=sha256:f2671232073e45c84c1f0c807b9c398b1e321b695d031a4a61f2c4ae4664c797 \ + --hash=sha256:f37f25713d0dff3653d7e04668d1733d003855a735fc63d3666dcd2fbde0dca5 \ + --hash=sha256:f7f410e513b4ca7c8e36cf8b3293de09841ec32825c4c073c9a802023a528108 \ + --hash=sha256:f850dbcaffab3f3b3265ed17425db5f5dc841f9a8f5c5fa74bff02cebc198ed6 \ + --hash=sha256:fb4146591032ff9e542f126ed51def92bc88aa1315ce400b16c0d56e773d5a7a \ + --hash=sha256:ff41096837dbd0b09e9565bb5bf273a444bb0dff9331a1e90cb6c8876500928e # via -r requirements.txt -pyvcg==1.0.6 \ - --hash=sha256:cf0ddec9a80f5880836bfe93214641e83fedf279311ad6182bb85b726d896e47 \ - --hash=sha256:eaa7c054c3fae21706855aa314761f139080661c63fa9712c48340c563513199 +pyvcg==1.0.9 \ + --hash=sha256:4230ebfdc1796b86fc1511a860214e3ba355a85730d4c7647e3abd6fb89f43e6 \ + --hash=sha256:4d33af5a05529b8ec62db2f133b64b781a3ddf3fcac07ac0f592ca416f8b0e2b # via -r requirements.txt diff --git a/tests-large-partial/BUILD b/tests-large-partial/BUILD new file mode 100644 index 00000000..108701b6 --- /dev/null +++ b/tests-large-partial/BUILD @@ -0,0 +1,20 @@ +load("@rules_python//python:defs.bzl", "py_binary") +load("//bazel/_private:partial_test.bzl", "trlc_partial_test") + +# --------------------------------------------------------------------------- +# Large partial-loading tests +# --------------------------------------------------------------------------- +# Tests are discovered dynamically: any subdirectory containing an ``output`` +# golden file is a test. The ``large/`` corpus directory has no ``output`` +# file and is therefore not picked up. +_TESTS = [ + f.split("/")[0] + for f in glob(["*/output"]) +] + +[trlc_partial_test(test_name = t) for t in _TESTS] + +test_suite( + name = "partial_tests", + tests = [":" + t for t in _TESTS], +) diff --git a/tests-large-partial/Makefile b/tests-large-partial/Makefile index 48719642..835cba2e 100644 --- a/tests-large-partial/Makefile +++ b/tests-large-partial/Makefile @@ -1,12 +1,13 @@ -TARGETS=$(addsuffix .output, $(basename $(wildcard *.scenario))) +TESTS=$(wildcard */options) +TARGETS=$(patsubst %/options,%/output,$(TESTS)) all: $(TARGETS) fast: $(TARGETS) -%.output: %.scenario +%/output: %/options -@coverage run -p --rcfile=../coverage.cfg --branch \ --data-file ../.coverage \ - ../trlc.py --verify $(file < $<) \ + ../trlc.py $(file < $<) \ > $@ 2>&1 rebuild-canned-tests: diff --git a/tests-large-partial/partial-1.scenario b/tests-large-partial/partial-1.scenario deleted file mode 100644 index 681269d6..00000000 --- a/tests-large-partial/partial-1.scenario +++ /dev/null @@ -1 +0,0 @@ ---show-file-list -I large large/package_1_1.trlc diff --git a/tests-large-partial/partial-1/options b/tests-large-partial/partial-1/options new file mode 100644 index 00000000..5dba94ef --- /dev/null +++ b/tests-large-partial/partial-1/options @@ -0,0 +1 @@ +--verify --show-file-list -I large large/package_1_1.trlc diff --git a/tests-large-partial/partial-1.output b/tests-large-partial/partial-1/output similarity index 100% rename from tests-large-partial/partial-1.output rename to tests-large-partial/partial-1/output diff --git a/tests-large-partial/partial-2.scenario b/tests-large-partial/partial-2.scenario deleted file mode 100644 index 4f55f825..00000000 --- a/tests-large-partial/partial-2.scenario +++ /dev/null @@ -1 +0,0 @@ ---show-file-list -I large large/package_3_1.trlc diff --git a/tests-large-partial/partial-2/options b/tests-large-partial/partial-2/options new file mode 100644 index 00000000..617af562 --- /dev/null +++ b/tests-large-partial/partial-2/options @@ -0,0 +1 @@ +--verify --show-file-list -I large large/package_3_1.trlc diff --git a/tests-large-partial/partial-2.output b/tests-large-partial/partial-2/output similarity index 100% rename from tests-large-partial/partial-2.output rename to tests-large-partial/partial-2/output diff --git a/tests-system/BUILD b/tests-system/BUILD new file mode 100644 index 00000000..132ca63d --- /dev/null +++ b/tests-system/BUILD @@ -0,0 +1,49 @@ +load("//bazel/_private:system_test.bzl", "trlc_system_test") + +# --------------------------------------------------------------------------- +# System integration tests +# --------------------------------------------------------------------------- +# Test directories are discovered dynamically via glob. Any subdirectory +# that contains an ``output`` golden file is treated as a test. Sub-packages +# (the bzl-api-* directories) have their own BUILD files and are excluded. +_SUBPACKAGES = [ + "bzl-api-deps", + "bzl-api-simple", + "bzl-api-spec-check", +] + +_ALL_TESTS = [ + f.split("/")[0] + for f in glob(["*/output"]) + if f.split("/")[0] not in _SUBPACKAGES +] + +[trlc_system_test(test_dir = d) for d in _ALL_TESTS] + +# "slow" tests are excluded from the :fast suite but included in :all_tests. +# Currently only "bulk" qualifies; add further names here if needed. +_SLOW_TESTS = ["bulk"] + +test_suite( + name = "fast", + tests = [":" + d for d in _ALL_TESTS if d not in _SLOW_TESTS], +) + +test_suite( + name = "all_tests", + tests = [":" + d for d in _ALL_TESTS], +) + +# --------------------------------------------------------------------------- +# Bazel API (trlc.bzl) integration tests +# Rules live in their own sub-packages; this suite aggregates them. +# --------------------------------------------------------------------------- + +test_suite( + name = "bzl_api", + tests = [ + "//tests-system/bzl-api-simple:bzl-api-simple-test", + "//tests-system/bzl-api-deps:bzl-api-deps-test", + "//tests-system/bzl-api-spec-check:bzl-api-spec-check-test", + ], +) diff --git a/tests-system/bzl-api-deps/BUILD b/tests-system/bzl-api-deps/BUILD new file mode 100644 index 00000000..eb365538 --- /dev/null +++ b/tests-system/bzl-api-deps/BUILD @@ -0,0 +1,29 @@ +load("//:trlc.bzl", "trlc_requirements", "trlc_requirements_test", "trlc_specification") + +trlc_specification( + name = "base_spec", + srcs = ["base_schema.rsl"], +) + +trlc_requirements( + name = "base_reqs", + srcs = ["base_items.trlc"], + spec = [":base_spec"], +) + +trlc_specification( + name = "ext_spec", + srcs = ["ext_schema.rsl"], +) + +trlc_requirements( + name = "ext_reqs", + srcs = ["ext_items.trlc"], + spec = [":ext_spec"], + deps = [":base_reqs"], +) + +trlc_requirements_test( + name = "bzl-api-deps-test", + reqs = [":ext_reqs"], +) diff --git a/tests-system/bzl-api-deps/base_items.trlc b/tests-system/bzl-api-deps/base_items.trlc new file mode 100644 index 00000000..26bf1de9 --- /dev/null +++ b/tests-system/bzl-api-deps/base_items.trlc @@ -0,0 +1,11 @@ +package DepsBase + +Component Engine { + name = "Engine" + description = "Main propulsion unit" +} + +Component Wheel { + name = "Wheel" + description = "Wheel assembly" +} diff --git a/tests-system/bzl-api-deps/base_schema.rsl b/tests-system/bzl-api-deps/base_schema.rsl new file mode 100644 index 00000000..8b50e3eb --- /dev/null +++ b/tests-system/bzl-api-deps/base_schema.rsl @@ -0,0 +1,6 @@ +package DepsBase + +type Component { + name String + description String +} diff --git a/tests-system/bzl-api-deps/ext_items.trlc b/tests-system/bzl-api-deps/ext_items.trlc new file mode 100644 index 00000000..a6df98fe --- /dev/null +++ b/tests-system/bzl-api-deps/ext_items.trlc @@ -0,0 +1,13 @@ +package DepsExt + +import DepsBase + +DepsBase.Component Gearbox { + name = "Gearbox" + description = "Transmission unit" +} + +System Powertrain { + name = "Powertrain" + priority = 1 +} diff --git a/tests-system/bzl-api-deps/ext_schema.rsl b/tests-system/bzl-api-deps/ext_schema.rsl new file mode 100644 index 00000000..7bb10a39 --- /dev/null +++ b/tests-system/bzl-api-deps/ext_schema.rsl @@ -0,0 +1,6 @@ +package DepsExt + +type System { + name String + priority Integer +} diff --git a/tests-system/bzl-api-deps/output b/tests-system/bzl-api-deps/output new file mode 100644 index 00000000..c2c83c81 --- /dev/null +++ b/tests-system/bzl-api-deps/output @@ -0,0 +1 @@ +Processed 2 models and 2 requirement files and found no issues diff --git a/tests-system/bzl-api-deps/output.brief b/tests-system/bzl-api-deps/output.brief new file mode 100644 index 00000000..c2c83c81 --- /dev/null +++ b/tests-system/bzl-api-deps/output.brief @@ -0,0 +1 @@ +Processed 2 models and 2 requirement files and found no issues diff --git a/tests-system/bzl-api-deps/output.json b/tests-system/bzl-api-deps/output.json new file mode 100644 index 00000000..9bab89ea --- /dev/null +++ b/tests-system/bzl-api-deps/output.json @@ -0,0 +1,19 @@ +{ + "Engine": { + "description": "Main propulsion unit", + "name": "Engine" + }, + "Gearbox": { + "description": "Transmission unit", + "name": "Gearbox" + }, + "Powertrain": { + "name": "Powertrain", + "priority": 1 + }, + "Wheel": { + "description": "Wheel assembly", + "name": "Wheel" + } +} +Processed 2 models and 2 requirement files and found no issues diff --git a/tests-system/bzl-api-deps/output.smtlib b/tests-system/bzl-api-deps/output.smtlib new file mode 100644 index 00000000..c2c83c81 --- /dev/null +++ b/tests-system/bzl-api-deps/output.smtlib @@ -0,0 +1 @@ +Processed 2 models and 2 requirement files and found no issues diff --git a/tests-system/bzl-api-simple/BUILD b/tests-system/bzl-api-simple/BUILD new file mode 100644 index 00000000..759d2ea1 --- /dev/null +++ b/tests-system/bzl-api-simple/BUILD @@ -0,0 +1,17 @@ +load("//:trlc.bzl", "trlc_requirements", "trlc_requirements_test", "trlc_specification") + +trlc_specification( + name = "spec", + srcs = ["schema.rsl"], +) + +trlc_requirements( + name = "reqs", + srcs = ["reqs.trlc"], + spec = [":spec"], +) + +trlc_requirements_test( + name = "bzl-api-simple-test", + reqs = [":reqs"], +) diff --git a/tests-system/bzl-api-simple/output b/tests-system/bzl-api-simple/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/bzl-api-simple/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-simple/output.brief b/tests-system/bzl-api-simple/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/bzl-api-simple/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-simple/output.json b/tests-system/bzl-api-simple/output.json new file mode 100644 index 00000000..28f8db97 --- /dev/null +++ b/tests-system/bzl-api-simple/output.json @@ -0,0 +1,13 @@ +{ + "REQ_001": { + "description": "The system shall process inputs correctly", + "id": "REQ_001", + "priority": 1 + }, + "REQ_002": { + "description": "The system shall produce correct outputs", + "id": "REQ_002", + "priority": 2 + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-simple/output.smtlib b/tests-system/bzl-api-simple/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/bzl-api-simple/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-simple/reqs.trlc b/tests-system/bzl-api-simple/reqs.trlc new file mode 100644 index 00000000..5c2af392 --- /dev/null +++ b/tests-system/bzl-api-simple/reqs.trlc @@ -0,0 +1,13 @@ +package Simple + +Requirement REQ_001 { + id = "REQ_001" + description = "The system shall process inputs correctly" + priority = 1 +} + +Requirement REQ_002 { + id = "REQ_002" + description = "The system shall produce correct outputs" + priority = 2 +} diff --git a/tests-system/bzl-api-simple/schema.rsl b/tests-system/bzl-api-simple/schema.rsl new file mode 100644 index 00000000..c9f0f827 --- /dev/null +++ b/tests-system/bzl-api-simple/schema.rsl @@ -0,0 +1,12 @@ +package Simple + +type Requirement { + id String + description String + priority Integer +} + +checks Requirement { + len(description) > 0, "description must not be empty" + priority > 0, "priority must be positive" +} diff --git a/tests-system/bzl-api-spec-check/BUILD b/tests-system/bzl-api-spec-check/BUILD new file mode 100644 index 00000000..b2c50cef --- /dev/null +++ b/tests-system/bzl-api-spec-check/BUILD @@ -0,0 +1,17 @@ +load("//:trlc.bzl", "trlc_requirements", "trlc_specification", "trlc_specification_test") + +trlc_specification( + name = "spec", + srcs = ["types.rsl"], +) + +trlc_requirements( + name = "reqs", + srcs = ["placeholder.trlc"], + spec = [":spec"], +) + +trlc_specification_test( + name = "bzl-api-spec-check-test", + reqs = [":reqs"], +) diff --git a/tests-system/bzl-api-spec-check/output b/tests-system/bzl-api-spec-check/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/bzl-api-spec-check/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-spec-check/output.brief b/tests-system/bzl-api-spec-check/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/bzl-api-spec-check/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-spec-check/output.json b/tests-system/bzl-api-spec-check/output.json new file mode 100644 index 00000000..0b6784ac --- /dev/null +++ b/tests-system/bzl-api-spec-check/output.json @@ -0,0 +1,8 @@ +{ + "SPEC_001": { + "description": "Placeholder requirement for spec-check test", + "id": "SPEC_001", + "severity": 3 + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-spec-check/output.smtlib b/tests-system/bzl-api-spec-check/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/bzl-api-spec-check/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/bzl-api-spec-check/placeholder.trlc b/tests-system/bzl-api-spec-check/placeholder.trlc new file mode 100644 index 00000000..e6f783bf --- /dev/null +++ b/tests-system/bzl-api-spec-check/placeholder.trlc @@ -0,0 +1,7 @@ +package SpecCheck + +Requirement SPEC_001 { + id = "SPEC_001" + description = "Placeholder requirement for spec-check test" + severity = 3 +} diff --git a/tests-system/bzl-api-spec-check/types.rsl b/tests-system/bzl-api-spec-check/types.rsl new file mode 100644 index 00000000..17b5f684 --- /dev/null +++ b/tests-system/bzl-api-spec-check/types.rsl @@ -0,0 +1,7 @@ +package SpecCheck + +type Requirement { + id String + description String + severity Integer +} diff --git a/tests-unit/BUILD.bazel b/tests-unit/BUILD.bazel new file mode 100644 index 00000000..c3f6ab45 --- /dev/null +++ b/tests-unit/BUILD.bazel @@ -0,0 +1,28 @@ +load("@rules_python//python:defs.bzl", "py_test") + +py_test( + name = "test_ast_bysection", + srcs = ["test_ast_bysection.py"], + deps = ["//trlc:trlc"], +) + +py_test( + name = "test_lexer", + srcs = ["test_lexer.py"], + deps = ["//trlc:trlc"], +) + +py_test( + name = "test_lexer_base", + srcs = ["test_lexer_base.py"], + deps = ["//trlc:trlc"], +) + +test_suite( + name = "unit_tests", + tests = [ + ":test_ast_bysection", + ":test_lexer", + ":test_lexer_base", + ], +) diff --git a/trlc.bzl b/trlc.bzl index aba71f86..82ec68a2 100644 --- a/trlc.bzl +++ b/trlc.bzl @@ -27,6 +27,7 @@ def trlc_specification_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc main = main, deps = ["@trlc//trlc:trlc"], data = ["@trlc//:cvc5"] + reqs, + **kwargs ) def _trlc_requirement_impl(ctx): @@ -71,4 +72,5 @@ def trlc_requirements_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc. main = main, deps = ["@trlc//trlc:trlc"], data = ["@trlc//:cvc5"] + reqs, + **kwargs ) diff --git a/trlc/errors.py b/trlc/errors.py index 229f1cc4..73cf3600 100644 --- a/trlc/errors.py +++ b/trlc/errors.py @@ -183,11 +183,12 @@ def __init__(self, brief=False, detailed_info=True, self.suppress_kind = set() self.strip_prefix = strip_prefix if out_path is not None: - self._owned_file = open(out_path, "w", encoding="UTF-8") # pylint: disable=consider-using-with + self._owned_file = open( # pylint: disable=consider-using-with + out_path, "w", encoding="UTF-8") self.out = self._owned_file else: self._owned_file = None - self.out = out + self.out = out if out is not None else sys.stdout def close(self): if self._owned_file is not None: diff --git a/trlc/trlc.py b/trlc/trlc.py index 2dd0ea13..6f33f642 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -637,13 +637,13 @@ def trlc(): help=("If there are no errors, produce a summary" " naming every file processed.")) og_output.add_argument("--log", - nargs = 2, + nargs = '+', metavar = ("FILE", "PREFIX"), default = None, - help = ("Write all output to FILE, strip PREFIX" - " from file paths in messages." - " Intended for use as a Bazel build" - " action.")) + help = ("Write all output to FILE, optionally" + " strip PREFIX from file paths in" + " messages. Intended for use as a" + " Bazel build action.")) og_output.add_argument("--error-on-warnings", action="store_true", help=("If there are warnings, return status code" @@ -670,6 +670,12 @@ def trlc(): metavar="DIR|FILE") options = ap.parse_args() + if options.log: + if len(options.log) > 2: + ap.error("--log accepts at most 2 values: FILE and optionally PREFIX") + if len(options.log) == 1: + options.log.append(None) + if options.version: # pragma: no cover print(TRLC_VERSION) sys.exit(0) @@ -829,8 +835,7 @@ def get_status(parser): parser.cu.package.name), file=mh.out) if ok: - if options.error_on_warnings and mh.warnings \ - or mh.errors: # pragma: no cover + if (options.error_on_warnings and mh.warnings) or mh.errors: # pragma: no cover rv = 1 else: rv = 0