|
| 1 | +# Using TRLC with Bazel |
| 2 | + |
| 3 | +TRLC ships Bazel macros in [`trlc.bzl`](@trlc//trlc.bzl) |
| 4 | + |
| 5 | +## Setup |
| 6 | + |
| 7 | +```python |
| 8 | +# MODULE.bazel |
| 9 | +bazel_dep(name = "trlc", version = "x.x.x") |
| 10 | +``` |
| 11 | + |
| 12 | +```python |
| 13 | +# BUILD |
| 14 | +load("@trlc//:trlc.bzl", |
| 15 | + "trlc_specification", |
| 16 | + "trlc_requirements", |
| 17 | + "trlc_requirements_test", |
| 18 | + "trlc_specification_test") |
| 19 | +``` |
| 20 | + |
| 21 | +It includes the pre-built CVC5 binary for Linux, macOS, and Windows. |
| 22 | + |
| 23 | +--- |
| 24 | + |
| 25 | +## Public API |
| 26 | + |
| 27 | +### `trlc_specification(name, srcs)` |
| 28 | + |
| 29 | +Collects `.rsl` schema files into a bazel target. |
| 30 | + |
| 31 | +| Attribute | Description | |
| 32 | +|-----------|-------------| |
| 33 | +| `name` | Target name. | |
| 34 | +| `srcs` | `*.rsl` files. | |
| 35 | + |
| 36 | +--- |
| 37 | + |
| 38 | +### `trlc_requirements(name, srcs, spec=[], deps=[])` |
| 39 | + |
| 40 | +Collects `.trlc` requirement files, wired to their schema and any |
| 41 | +imported packages. |
| 42 | + |
| 43 | +| Attribute | Description | |
| 44 | +|-----------|-------------| |
| 45 | +| `name` | Target name. | |
| 46 | +| `srcs` | `*.trlc` files. | |
| 47 | +| `spec` | Direct `trlc_specification` targets. | |
| 48 | +| `deps` | Other `trlc_requirements` targets whose packages are imported. | |
| 49 | + |
| 50 | +--- |
| 51 | + |
| 52 | +### `trlc_requirements_test(name, reqs, srcs=…, main=…)` |
| 53 | + |
| 54 | +Runs `trlc --verify`. The test passes when TRLC reports no errors. |
| 55 | +Pass a custom `srcs`/`main` to run your own Python script instead |
| 56 | +of the built-in CLI (see [TUTORIAL-API.md](TUTORIAL-API.md)). |
| 57 | + |
| 58 | +| Attribute | Description | |
| 59 | +|-----------|-------------| |
| 60 | +| `name` | Target name. | |
| 61 | +| `reqs` | `trlc_requirements` targets to validate. | |
| 62 | +| `srcs` | Override the entry-point script (optional). | |
| 63 | +| `main` | Filename of the entry point (required when `srcs` is set). | |
| 64 | + |
| 65 | +--- |
| 66 | + |
| 67 | +### `trlc_specification_test(name, reqs)` |
| 68 | + |
| 69 | +Like `trlc_requirements_test` but passes `--skip-trlc-files`. Use |
| 70 | +this to check the RSL schema is consistent before any `.trlc` data |
| 71 | +files exist. |
| 72 | + |
| 73 | +--- |
| 74 | + |
| 75 | +## Example — `api-examples/filename-check/` |
| 76 | + |
| 77 | +See the complete working example in |
| 78 | +[`api-examples/filename-check/`](../api-examples/filename-check/). |
| 79 | + |
| 80 | +--- |
| 81 | + |
| 82 | +## Multi-package layout |
| 83 | + |
| 84 | +Chain packages with `deps` when one `.trlc` file imports another: |
| 85 | + |
| 86 | +```python |
| 87 | +# base/BUILD |
| 88 | +trlc_specification(name = "spec", srcs = ["base.rsl"]) |
| 89 | +trlc_requirements(name = "reqs", srcs = ["base_reqs.trlc"], spec = [":spec"]) |
| 90 | + |
| 91 | +# feature/BUILD |
| 92 | +trlc_requirements( |
| 93 | + name = "reqs", |
| 94 | + srcs = ["feature_reqs.trlc"], |
| 95 | + spec = [":feature_spec"], |
| 96 | + deps = ["//base:reqs"], # pulls in base.rsl + base_reqs.trlc |
| 97 | +) |
| 98 | +``` |
0 commit comments