From c475e80a6ffda14abf7d89e75f1ec51469a8c509 Mon Sep 17 00:00:00 2001 From: Jochen Hoenle Date: Tue, 3 Mar 2026 09:10:29 +0100 Subject: [PATCH 1/2] [bazel] use python api - use python api of cvc5 instead of local binary - restructure requirements in bazel to match standard conventions --- BUILD | 2 +- MODULE.bazel | 7 ++- MODULE.bazel.lock | 20 ++++---- bazel/_private/mode_test.py | 8 ++-- bazel/_private/system_test.bzl | 48 +++---------------- requirements.txt | 2 +- requirements_dev.txt | 3 +- ...rements.txt.bazel => requirements_lock.txt | 0 trlc.bzl | 4 +- trlc/BUILD | 5 +- 10 files changed, 35 insertions(+), 64 deletions(-) rename requirements.txt.bazel => requirements_lock.txt (100%) diff --git a/BUILD b/BUILD index 19cf02e2..09ce5cea 100644 --- a/BUILD +++ b/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 diff --git a/MODULE.bazel b/MODULE.bazel index 7cc6d3d1..01a78ff2 100644 --- a/MODULE.bazel +++ b/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", diff --git a/MODULE.bazel.lock b/MODULE.bazel.lock index 2c918605..95075536 100644 --- a/MODULE.bazel.lock +++ b/MODULE.bazel.lock @@ -682,10 +682,10 @@ "@@rules_python+//python/extensions:pip.bzl%pip": { "general": { "bzlTransitiveDigest": "Z2EwAlnWwmyPNSF4pT+ZyT3/Csf4YVbyQPmxi3fBMEQ=", - "usagesDigest": "B9WByXMQOeCDEjtpOkG/1hz+Pl4i2Pyiw1BRraLz0zk=", + "usagesDigest": "prOPP6t8gegT4BTUuOXjkS7zR1SMdrRccGZu1Ky0V/M=", "recordedFileInputs": { - "@@//requirements.txt": "3fbbc32af771695c98b9f794b0513f0809c342b973aa0d4005727965af158b8f", "@@//requirements_dev_lock.txt": "02f3ced94521bd20df5fa3b866ca6f83f381538df4748c388ff38336a1d6901f", + "@@//requirements_lock.txt": "88f504bd5b34de27ea835a92f4892e49c92f78bf84276838b80bd0bacd0787e3", "@@protobuf+//python/requirements.txt": "983be60d3cec4b319dcab6d48aeb3f5b2f7c3350f26b3a9e97486c37967c73c5", "@@rules_fuzzing+//fuzzing/requirements.txt": "ab04664be026b632a0d2a2446c4f65982b7654f5b6851d2f9d399a19b7242a5b", "@@rules_python+//tools/publish/requirements_darwin.txt": "095d4a4f3d639dce831cd493367631cd51b53665292ab20194bac2c0c6458fa8", @@ -3192,7 +3192,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_10_host//:python", "repo": "trlc_dependencies_310", - "requirement": "cvc5>=1.3.1" + "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_dependencies_310_pyvcg": { @@ -3201,7 +3201,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_10_host//:python", "repo": "trlc_dependencies_310", - "requirement": "pyvcg==1.0.9" + "requirement": "pyvcg==1.0.9 --hash=sha256:4230ebfdc1796b86fc1511a860214e3ba355a85730d4c7647e3abd6fb89f43e6 --hash=sha256:4d33af5a05529b8ec62db2f133b64b781a3ddf3fcac07ac0f592ca416f8b0e2b" } }, "trlc_dependencies_311_cvc5": { @@ -3210,7 +3210,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_11_host//:python", "repo": "trlc_dependencies_311", - "requirement": "cvc5>=1.3.1" + "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_dependencies_311_pyvcg": { @@ -3219,7 +3219,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_11_host//:python", "repo": "trlc_dependencies_311", - "requirement": "pyvcg==1.0.9" + "requirement": "pyvcg==1.0.9 --hash=sha256:4230ebfdc1796b86fc1511a860214e3ba355a85730d4c7647e3abd6fb89f43e6 --hash=sha256:4d33af5a05529b8ec62db2f133b64b781a3ddf3fcac07ac0f592ca416f8b0e2b" } }, "trlc_dependencies_312_cvc5": { @@ -3228,7 +3228,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_12_host//:python", "repo": "trlc_dependencies_312", - "requirement": "cvc5>=1.3.1" + "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_dependencies_312_pyvcg": { @@ -3237,7 +3237,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_12_host//:python", "repo": "trlc_dependencies_312", - "requirement": "pyvcg==1.0.9" + "requirement": "pyvcg==1.0.9 --hash=sha256:4230ebfdc1796b86fc1511a860214e3ba355a85730d4c7647e3abd6fb89f43e6 --hash=sha256:4d33af5a05529b8ec62db2f133b64b781a3ddf3fcac07ac0f592ca416f8b0e2b" } }, "trlc_dependencies_39_cvc5": { @@ -3246,7 +3246,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_9_host//:python", "repo": "trlc_dependencies_39", - "requirement": "cvc5>=1.3.1" + "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_dependencies_39_pyvcg": { @@ -3255,7 +3255,7 @@ "dep_template": "@trlc_dependencies//{name}:{target}", "python_interpreter_target": "@@rules_python++python+python_3_9_host//:python", "repo": "trlc_dependencies_39", - "requirement": "pyvcg==1.0.9" + "requirement": "pyvcg==1.0.9 --hash=sha256:4230ebfdc1796b86fc1511a860214e3ba355a85730d4c7647e3abd6fb89f43e6 --hash=sha256:4d33af5a05529b8ec62db2f133b64b781a3ddf3fcac07ac0f592ca416f8b0e2b" } }, "trlc_dev_dependencies_312_alabaster": { diff --git a/bazel/_private/mode_test.py b/bazel/_private/mode_test.py index 4c219309..e71a079f 100644 --- a/bazel/_private/mode_test.py +++ b/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"] diff --git a/bazel/_private/system_test.bzl b/bazel/_private/system_test.bzl index c9dcb9c0..4fe90b36 100644 --- a/bazel/_private/system_test.bzl +++ b/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/ -> 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. + # 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: test_target = test_dir + "_test" native.py_test( diff --git a/requirements.txt b/requirements.txt index d3d533aa..6498905e 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,2 @@ pyvcg==1.0.9 -cvc5>=1.3.1 +cvc5>=1.3.2 diff --git a/requirements_dev.txt b/requirements_dev.txt index 98f83ae3..438be4a4 100644 --- a/requirements_dev.txt +++ b/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 diff --git a/requirements.txt.bazel b/requirements_lock.txt similarity index 100% rename from requirements.txt.bazel rename to requirements_lock.txt diff --git a/trlc.bzl b/trlc.bzl index 82ec68a2..18a5ab17 100644 --- a/trlc.bzl +++ b/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, diff --git a/trlc/BUILD b/trlc/BUILD index 72ff0240..f94a1362 100644 --- a/trlc/BUILD +++ b/trlc/BUILD @@ -17,5 +17,8 @@ py_library( "version.py", ], visibility = ["//visibility:public"], - deps = [requirement("pyvcg")], + deps = [ + requirement("pyvcg"), + requirement("cvc5"), + ], ) From 70f762b3f804eb6962414591bce8f09c96b26bb6 Mon Sep 17 00:00:00 2001 From: Jochen Hoenle Date: Tue, 3 Mar 2026 09:12:51 +0100 Subject: [PATCH 2/2] use same cvc5 version in all scattered tests --- .github/workflows/ci.yml | 2 +- .github/workflows/docs.yml | 2 +- util/fetch_cvc5.py | 11 ++++++++++- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 87be9542..e9846ed3 100644 --- a/.github/workflows/ci.yml +++ b/.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: | diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 5f975d0b..698e5a99 100644 --- a/.github/workflows/docs.yml +++ b/.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: | diff --git a/util/fetch_cvc5.py b/util/fetch_cvc5.py index 49e21b9b..f84e1648 100755 --- a/util/fetch_cvc5.py +++ b/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()