rules_ci

bazel_dep(name = "rules_ci", version = "0.3.0")

# MODULE.bazel
bazel_dep(name = "rules_ci", version = "0.0.1")

# BUILD.bazel — generate + drift-gate this repo's .gitlab-ci.yml, README badges, and hooks
load("@rules_ci//project:defs.bzl", "fastverk_project")

fastverk_project(name = "project", repo = "your/repo", badges = True, hooks = True)

bazel test //:project.ci_gates       # every drift/validation gate (CI + the pre-commit hook)
bazel run  //:project.hooks_install  # install the pre-commit hook (core.hooksPath)

load("@rules_ci//project:defs.bzl", "fastverk_project")

fastverk_project(name, repo, ci_include, ci_variables, ci_stages, ci_jobs, ci_extra, ci,
                 ci_jobs_native, features, products, expected_products, gate_tests, hooks, hooks_dir,
                 badges, host, badge_branch, write_to, validate, visibility)

bazel run  //:<name>.ci.update           # (re)generate the pipeline into the tree
bazel test //:<name>.ci.update_test      # CI-drift gate (CI + the pre-commit hook)
bazel build //:<name>.ci_validate        # schema gate

bazel test //:<name>.ci                  # the test gate (a test_suite)
# <name>.ci.pipeline.json                # publish jobs, read by the build-runner

bazel build //:<name>.products           # the discovered-products JSON manifest
bazel test  //:<name>.products_drift_test # declared-vs-discovered drift gate

bazel test //:<name>.ci_gates            # every drift/validation gate (CI + the hook)
bazel run  //:<name>.hooks_install       # install the pre-commit hook (core.hooksPath)

load("@rules_ci//release:defs.bzl", "products_drift_test")

products_drift_test(name, deps, expected)

load("@rules_ci//release:defs.bzl", "release_manifest")

release_manifest(name, deps)

load("@rules_ci//release:defs.bzl", "ReleaseArtifactInfo")

ReleaseArtifactInfo(kind, name, label, version_source, surface)

load("@rules_ci//release:defs.bzl", "ReleaseArtifactsInfo")

ReleaseArtifactsInfo(products)

load("@rules_ci//release:defs.bzl", "release_artifacts")

release_artifacts()

load("@rules_ci//hooks:defs.bzl", "git_hooks")

git_hooks(name, gates, hooks_dir)

Real usage, taken from the module’s examples/.

examples/native_project/BUILD.bazel

load("@rules_ci//ci:defs.bzl", "ci_job", "ci_publish")
load("@rules_ci//project:defs.bzl", "fastverk_project")
load("@rules_shell//shell:sh_test.bzl", "sh_test")

# A repo whose CI is Bazel targets, not a generated pipeline file.
#
# This is the shape readiness criterion C2 (`ci-as-rules`) asks for: no
# `.gitlab-ci.yml`, no `.github/workflows`, `MODULE.bazel` present. Before the
# `ci` backend existed, fastverk_project could not produce it — the macro always
# emitted the very file C2 forbids, so the criterion was unsatisfiable for every
# repo that used it.
#
#   bazel test  //examples/native_project:project.ci        # the test gate
#   bazel test  //examples/native_project:project.ci_gates  # the same, via the suite
#
# And, load-bearing: NO .gitlab-ci.yml is written anywhere by this target.
package(default_visibility = ["//visibility:public"])

fastverk_project(
    name = "project",
    ci = "native",
    ci_jobs_native = [
        ci_job(
            name = "unit",
            script = ["echo ok"],
            stage = "test",
        ),
        ci_publish(
            name = "pub",
            artifact = ":unit.sh",
            destination = "s3://example/native/",
            kind = "static_cdn",
        ),
    ],
    repo = "example/native",
)

# A repo that ships nothing and is built entirely off the BuildRun rail: no CI
# wiring at all. `project_none.ci_gates` must still ANALYZE — it was the dangling
# `.ci.update_test` reference in the gates list that made this shape impossible.
fastverk_project(
    name = "project_none",
    ci = "none",
    repo = "example/none",
)

# Turn the load-bearing claim above ("NO .gitlab-ci.yml is written") into a gate.
# A comment cannot fail CI, and this one guards readiness criterion C2 — see
# no_pipeline_file_test.sh for why absence needs a query to assert it.
genquery(
    name = "backend.targets",
    expression = "deps(//examples/native_project:project.ci_gates) + deps(//examples/native_project:project_none.ci_gates)",
    scope = [
        ":project.ci_gates",
        ":project_none.ci_gates",
    ],
)

sh_test(
    name = "no_pipeline_file_test",
    srcs = ["no_pipeline_file_test.sh"],
    data = [":backend.targets"],
    env = {"TARGETS": "$(rootpath :backend.targets)"},
)

examples/pipeline/BUILD.bazel

load("@rules_ci//ci:defs.bzl", "ci_job", "ci_pipeline", "ci_publish")
load("@rules_shell//shell:sh_test.bzl", "sh_test")

# Smoke test of the //ci re-export: express a pipeline through @rules_ci//ci and confirm the
# runtime (from rules_ci_ir) resolves through rules_ci.
#   bazel test  //examples/pipeline:demo
#   bazel build //examples/pipeline:demo.manifest
package(default_visibility = ["//visibility:public"])

# A test carrying its OWN tags — the shape that exposed the vacuous-suite bug.
# Every real test has tags (`savvi_ts_package` stamps `unit`, sizes imply others),
# and none of them carry `ci-job` / `ci-stage=…`, so a tagged job suite filtered
# them all out. Kept deliberately tagged: an untagged test would not reproduce it.
sh_test(
    name = "tagged_unit_test",
    srcs = ["tagged_unit_test.sh"],
    tags = ["unit"],
)

ci_pipeline(
    name = "demo",
    jobs = [
        ci_job(
            name = "unit",
            script = ["echo ok"],
            stage = "test",
        ),
        # `test =` (aliasing an existing test) rather than `script =`. Until this
        # example existed, every example used `script =`, so the alias path — the
        # one every migrating repo actually uses — was never exercised.
        ci_job(
            name = "aliased",
            stage = "test",
            test = ":tagged_unit_test",
        ),
        ci_publish(
            name = "pub",
            artifact = ":unit.sh",
            destination = "s3://example/demo/",
            kind = "static_cdn",
        ),
        # `npm` kind: `artifact` is an `npm pack`-layout tarball and `destination`
        # is the registry URL. Not a real tarball here — this only pins that the
        # kind resolves and lands in `demo.pipeline.json`; the runner's own
        # dry-run keeps `bazel run` harmless without credentials.
        ci_publish(
            name = "pub_npm",
            artifact = ":unit.sh",
            destination = "https://registry.example.com/api/v4/projects/1/packages/npm/",
            kind = "npm",
        ),
    ],
)

# The vacuity gate is now GENERATED by ci_job — `//examples/pipeline:aliased.not_vacuous_test`
# — so the hand-written genquery + sh_test that used to live here is gone. This
# package still exercises the shape that broke: `ci_job(test = ...)` over a test
# carrying its own unrelated tags.

from docs/DESIGN.md

rules_ci — design

A neutral intermediate representation (IR) for CI pipeline configuration, with proved-correct translations between

• GitLab CI YAML (.gitlab-ci.yml)
• GitHub Actions YAML (.github/workflows/*.yml)
• Bazel rule invocations (sh_test / genrule / py_test / custom)

The repo is in scaffold state — pinned schemas, Rust workspace skeleton, Bazel rule stubs, and this design doc are live; the Lean 4 IR + correctness theorems are placeholders pinned by the roadmap below.

Why an IR at all

Direct translations between three pairs of CI/build systems would require six translators (and grows quadratically as more targets are added). With a single IR in the middle, we instead need:

• N parsers (one per source format)
• N emitters (one per target format)
• Theorems about parser/emitter pairs, not about every direction.

A neutral IR also forces a sharp question: what is a CI pipeline, structurally? The translation work depends entirely on that abstraction holding up across three very different surface representations.

What “provably correct” means here

Three increasingly ambitious levels of correctness:

Level	Claim	Status
A. Structural	Parser is total over valid-schema inputs. Round-trip identity holds modulo normalization: parse · emit · parse ≡ parse. DAG invariants preserved: no cycles in needs / dependencies, every artifact consumer has a producer, every job’s stage exists in the stages list.	Targeted for v0.1.
B. Bisimulation under abstract semantics	Define an opaque execution model: a job consumes inputs, runs an unspecified action, produces outputs. Prove gitlab.exec ≃ ir.exec ≃ github.exec under that model. Captures scheduling, dependency ordering, artifact flow — but not what script: [pytest] actually executes.	v0.3+ goal.
C. Runtime equivalence	Model bash, the runner environment, container state, network. “Translated YAML exits with the same code as the original.”	Explicit non-goal. A research project, not a release.

The repo commits to level A as a hard guarantee, layers level B as work progresses, and treats level C as out of scope.

Lean-as-verifier, not Lean-as-runtime

Two natural ways to integrate Lean 4:

1. Runtime: compile the Lean translator binary, run it inside Bazel actions at build time. Pro: the proofs cover the actual running code. Con: Lean → C compile is slow, deployment story is heavy, and rewriting parsers in Lean is high-friction.

2. Verifier: Rust is the language of the actual translator; Lean formalizes the IR + the spec of each parser / emitter; a reference implementation in Lean is extracted (or hand-mirrored) and proven correct; property-based tests fuzz-generate schema-valid inputs and check that the Rust translator matches the Lean spec on every input. This is the Verus / Creusot model.

We pick verifier. The Rust translator is the production artifact. Lean provides:

• The IR’s algebraic types (canonical reference).
• Theorems on parser totality, round-trip identity, and invariant preservation.
• Reference implementations for each parser/emitter that the Rust code is fuzz-tested against.

The Lean code lives under ir/; the Rust workspace lives under translator/. The two are kept in sync by convention + a TODO-tracked roadmap of “Lean theorem proved → matching Rust property test landed.”

The IR

The IR is a single algebraic type, designed to be the least-upper-bound of what GitLab CI and GitHub Actions express. Sketch (Lean syntax, illustrative):

structure Job where
  name      : String
  stage     : String                  -- "build", "test", ...
  needs     : List String             -- predecessor job names
  rules     : List Rule               -- when this job is selected
  env       : Map String String       -- key=value
  image     : Option String           -- container reference
  script    : List String             -- shell lines, opaque
  artifacts : List ArtifactSpec
  cache     : List CachePath
  outputs   : Map String String       -- exported step outputs
  publish   : Option Publish          -- ship the build to a hosting surface
  deriving Repr, BEq

inductive Publish where               -- structured publish targets
  | pages (path : String)             -- publish `path` as the repo's Pages site
  deriving Repr, BEq

structure Pipeline where
  stages    : List String             -- ordered phase names
  variables : Map String String
  defaults  : Job                     -- inherited shape
  triggers  : List Trigger            -- which events run the pipeline
  jobs      : List Job
  includes  : List Include            -- cross-pipeline composition
  deriving Repr

The IR is not the union of every GitLab and GitHub feature — it’s the intersection of what can be translated faithfully. Source features that fall outside (e.g. GitLab’s nested extends, GitHub’s reusable workflows with secrets-inheritance) are either:

• Lowered to the IR at parse time when an equivalence exists (e.g. extends resolved before IR emission).
• Emitted as a translation diagnostic (unsupported feature X at path Y) when not.

Diagnostics are first-class outputs; a translation that emits diagnostics is still a translation, but downstream consumers (the Bazel rule, the registry) can treat them as warnings or hard errors.

Pages — the first publish node

publish is where the IR earns its keep most visibly: “publish this directory as the repo’s static site” is one intent the two backends realize with almost nothing in common. A job carrying publish := some (.pages "public") lowers as:

gitlab-emit — GitLab Pages is a magic job named pages whose public/ artifact is served (the publish dir is public/, or set via pages.publish: on 17.x+):

pages:
  stage: pages
  script:
    - <job.script>            # build the site into public/
  artifacts:
    paths: [public]
  rules:
    - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH

github-emit — GitHub Pages is a workflow that uploads the directory as a Pages artifact and deploys it, with the right permissions and environment:

jobs:
  pages:
    runs-on: ubuntu-latest
    permissions: { pages: write, id-token: write }
    environment: github-pages
    steps:
      - run: <job.script>                       # build the site
      - uses: actions/upload-pages-artifact@v3
        with: { path: public }
      - uses: actions/deploy-pages@v4

The shared core — job.script builds the site, then a directory is published — is exactly one Publish.Pages path. Everything else (the magic job name + public/ artifact vs. the upload/deploy actions + permissions + environment) is emitter-private. rules_gitlab’s gitlab_pages_job macro is the hand-written precursor of the gitlab-emit rendering; promoting it here means a repo authors the publish once, in the neutral IR, and gets both backends.

Structural invariant (level A): at most one job may carry a Publish.Pages, and gitlab-emit names that job pages.

Schemas + pinning

We pin the canonical upstream schemas (sha256), refreshed via a documented workflow:

• GitLab CI: gitlab.com/gitlab-org/gitlab-foss/.../editor/schema/ci.json (already in use by rules_gitlab).
• GitHub Actions: json.schemastore.org/github-workflow.json (mirror of SchemaStore’s curated version).

Bazel has no JSON Schema — but each spec-derived rule (in the style of rules_cloudformation) exposes a typed attr set that projects as a JSON Schema. The Bazel-emit side translates IR jobs into rule invocations against a fixed runtime: a small ci_job(name, script, deps, ...) Bazel rule built into this module (see Bazel emit).

Translator surface

Implemented in translator/ as a Cargo workspace with these crates:

Crate	What	Status
ci-ir	Pure-Rust IR types + invariants + property test helpers.	scaffold
gitlab-parse	.gitlab-ci.yml → IR. ruamel-yaml-equivalent + custom-tag absorber.	scaffold
github-parse	.github/workflows/*.yml → IR.	roadmap
gitlab-emit	IR → .gitlab-ci.yml.	roadmap
github-emit	IR → GitHub Actions workflow.	roadmap
bazel-emit	IR → Bazel rule invocations. Uses starlark crate’s AST to emit .bzl.	roadmap
aggregator	N members → fleet IR + Markdown similarity report. Subsumes the savvi-side Python aggregator.	scaffold (smoke)
ci-translate-cli	ci-translate --from gitlab --to github < input.yml > out.yml.	roadmap

Bazel rule surface

User-facing Bazel rules in rules/defs.bzl:

Rule	Status	What
ci_yaml_translate(name, src, from, to)	stub	Translate a single CI YAML file. from/to ∈ {gitlab, github, bazel}.
ci_yaml_aggregate(name, members)	stub	Fleet-wide aggregation + Markdown report (Rust reimplementation of the savvi ci_analysis rule).
ci_yaml_diff(name, a, b)	roadmap	Structural diff of two CI YAMLs at the IR level — catches reordering-only changes vs. real diffs.

These are stubs that exec the relevant Rust binary from @rules_ci_crates. Once the crates are populated, the stubs become real.

Bazel-emit

bazel-emit is the trickiest part. The IR’s notion of a “job” is a black-box shell script with explicit deps + artifacts; Bazel’s hermeticity requires either:

1. Wrap the script as sh_test: sh_test(name = "<job>", srcs = ["<job>.sh"], deps = [...]) where the deps are the predecessor jobs’ outputs. Lossy in the other direction (Bazel deps are at content-level granularity, but a CI needs: is at job-completion-level granularity — close enough for the structural translation).
2. Generate scaffold + leave the heavy lifting to humans: emit the dependency wiring and let the user fill in real Bazel rule types. Less invasive; more useful as a migration tool.

We start with (1) — explicit sh_test + genrule emission. The output is a single <name>.bzl file consumed by a downstream load(...) in a hand-written BUILD.bazel. The Rust starlark crate (https://github.com/facebookexperimental/starlark-rust) provides AST + pretty-printing so the emitted file is canonical (stable across rebuilds, easy to diff).

Concrete shape:

## Emitted: //path:bazel_pipeline.bzl
load(
    "@rules_ci//rules/runtime:defs.bzl",
    "ci_job",
)

def my_pipeline():
    ci_job(
        name = "build",
        stage = "build",
        script = ["uv sync", "uv build"],
        image = "registry/savvi-ops:ci-py3.13",
    )
    ci_job(
        name = "test",
        stage = "test",
        needs = ["build"],
        script = ["uv run pytest"],
    )

ci_job is a thin macro provided by rules_ci’s runtime that expands to a sh_test or genrule depending on artifacts.

Roadmap by version

Version	Adds
0.0.1 (this)	Scaffold: design doc, schema pins, Rust workspace skeleton, GitLab parser stub, aggregator stub, Bazel rule stubs. No Lean code yet.
0.1.0	Working GitLab parser → IR; aggregator Rust binary that replaces the savvi ci_analysis Python aggregator (same Markdown report); ci_yaml_aggregate rule.
0.2.0	github-parse. GitLab ↔ IR round-trip property tests.
0.3.0	gitlab-emit + github-emit. End-to-end ci-translate --from gitlab --to github works. Includes the Publish.Pages node (IR type landed in 0.0.1) — both emitters render a pages publish (see Pages — the first publish node).
0.4.0	bazel-emit + the ci_job runtime macro. GitLab → Bazel sh_test graphs. The neutral ci_pages(site) authoring macro lands here, superseding rules_gitlab’s gitlab_pages_job.
0.5.0	Lean 4 IR formalization + structural correctness theorems (level A above). Property tests are extracted/mirrored.
0.6.0+	Bisimulation theorems under abstract semantics (level B).

Refresh procedure

Every quarter, re-fetch the pinned schemas:

curl -fL https://gitlab.com/gitlab-org/gitlab-foss/-/raw/master/app/assets/javascripts/editor/schema/ci.json -o /tmp/gitlab-ci.json
shasum -a 256 /tmp/gitlab-ci.json
## paste into schemas/extensions.bzl

curl -fL https://json.schemastore.org/github-workflow.json -o /tmp/github.json
shasum -a 256 /tmp/github.json
## paste into schemas/extensions.bzl

Each pinning bump should be accompanied by a CHANGELOG entry listing any new schema features and whether they require IR extensions.

from docs/VERSIONING.md

Automated versioning + tag-push (rules_ci)

A WORKFLOW pushes pkg@x.y.z tags — never a dev, never the user. On merge to protected main, per discovered product, the pipeline computes the required SemVer bump from the PUBLIC SURFACE diff and pushes the tag under a bot identity; the existing idempotent publish lane fires on the tag. This replaces hand-maintained version bumps and manual changeset files with a deterministic, surface-driven decision (escalating only the genuinely-ambiguous cases to a judged verdict).

Pipeline

merge to main
   │
   ▼
release_artifacts aspect  ──►  per npm product: { name, version_source(package.json), surface(.d.ts*) }
   │
   ▼
version/surface.mjs  ──►  CURRENT surface (normalized exported decls + hash)   [per product]
   │                       fetch PREVIOUS surface (npm pack last tag → .d.ts, or stored artifact)
   ▼
version/diff.mjs    ──►  changes + DETERMINISTIC bump floor
   │                      • removed export → major   • added export → minor
   │                      • changed shape  → AMBIGUOUS
   ▼
version/escalate.mjs ──►  resolve ambiguous → bump  (conservative default, OR judged verdict)
   │
   ▼
version/version.mjs ──►  VersionDecision { from, to, bump, tag, rationale }   [0.x degrade]
   │
   ▼
tag-push (bot identity, tag-protection-admitted) ──►  publish lane fires on `pkg@x.y.z`

The deterministic core (BUILT + PROVEN — version/)

• surface.mjs — extracts the public surface from a package’s .d.ts entry via the TS compiler API: a sorted, comment/whitespace-NORMALIZED list of exported declarations ({name, kind, signature}) + a stable surface_hash. Cosmetic edits (doc comments, reformatting) are NOT surface changes. The .d.ts inputs come from the build graph (ReleaseArtifactInfo.surface, captured by the release_artifacts aspect).
• diff.mjs — diffs two surfaces → changes + a SemVer bump. DETERMINISTIC for add/remove (added→minor, removed→major); a shape CHANGE of an existing export is marked ambiguous (a text diff can’t reliably tell breaking from additive) and routed to escalation.
• escalate.mjs — the AMBIGUOUS-change seam. SAFE BY DEFAULT (no AI required): absent a backend, ambiguous → conservative FASTVERK_VERSION_AMBIGUOUS_DEFAULT (default major) so it never under-bumps. PRECISE WHEN WIRED: FASTVERK_VERSION_ESCALATE_CMD (the headless claude -p entrypoint) gets the ambiguous changes on stdin, returns {bump, rationale}.
• version.mjs — orchestrator: bump = max(deterministic, escalation), then applyBump with 0.x SemVer degradation (every @aion/* package is 0.x: breaking→minor, additive→patch; normal mapping once a package hits 1.0.0). Emits a VersionDecision.

Proven on version/fixtures/{base,add,remove,change}.d.ts: add→0.2.6, remove→0.3.0, change(no backend)→0.3.0 conservative, change(wired backend says minor)→0.2.6, no-change@1.4.0→1.4.0.

Schema — the DTOs ARE protos (fastverk.release.v1)

The surface/diff/decision DTOs cross the build→tool→tag boundary, so per “DTOs are protos” they are the canonical proto/fastverk/release/v1/release.proto messages (Surface, TsExport, Product, ReleaseManifest, SurfaceChange, SurfaceDiff, VersionDecision) — the schema of record, not ad-hoc JSON.

• Compiled HERMETICALLY by bazel — //proto/fastverk/release/v1:release_proto (rules_proto 7.1.0 + protobuf 33.4; protoc from the toolchain, never the system one). The build emits release_proto-descriptor-set.proto.bin, the single cross-language source of truth.
• The Node version/ tools serialize via that descriptor — version/proto.mjs loads the bazel-emitted descriptor set with protobufjs (no .proto re-parse, no codegen step) and does proto-wire encode/decode + verify at the I/O boundary. The tools keep ergonomic JS objects internally (lowercase enum strings); proto.mjs maps them to the proto messages (camelCase fields = the proto3-JSON canonical form; Bump/Op enum-name maps).
• Cross-language ready: a future Lean emit-boundary surface extractor consumes the same descriptor — add a Lean arm field to Surface (proto3 forward-compat) when it lands.
• Proven: surface.mjs --binary emits a Surface on the wire; Surface/SurfaceDiff/ VersionDecision all round-trip encode→decode, and verify() rejects malformed messages.

The escalation backend (GREENFIELD — designed, not built)

There is NO fastverk/mcp repo today (confirmed). The seam is ready; the backend is the next infra step:

• A small headless entrypoint: claude -p given ONLY the ambiguous changes + a strict JSON-schema’d {bump, rationale} output, scoped by an MCP ensemble (fastverk/build’s bazel query/cquery + surface introspection) so it answers from the graph, not guesses.
• Verdict is a pure function of the ambiguous-change set → cache by surface_hash pair.
• Baked into the CI image (infra/images → aion/build) and exposed as FASTVERK_VERSION_ESCALATE_CMD. Until then the conservative default keeps releases SAFE.

Tag-push + bot identity (GATED — outward config)

• The release lane (ci/aion-release.gitlab-ci.yml) runs on main, computes the decision, writes package.json version, and pushes pkg@x.y.z. The proven tag-push pattern (from platform/studio release.yml): git push origin <tag> under a token; on tag-collision append a timestamp suffix. The existing idempotent publish.mjs fires on the tag.
• Bot identity: a dedicated release-bot user (recommended) or the [[aion-carve-ci-token]] group-195 token, admitted by tag protection (v* / *@* tags pushable only by the bot). Tag protection + the bot user are the gated outward steps (no git tags exist in the carves yet; main is Maintainer-only).
• Previous-surface source: the lane npm packs the last published version and extracts its .d.ts for --previous (no rebuild-at-tag needed). Alternative: store the surface JSON as a release artifact per tag.

Rollout (gated)

1. Bake version/*.mjs + publish.mjs into the CI image (stop per-repo vendoring).
2. Add the release lane to the shared aion CI templates (include:-ed by every repo).
3. Stand up the escalation backend; set FASTVERK_VERSION_ESCALATE_CMD.
4. Create the release-bot identity + tag protection.
5. Pilot on one carve, then fan out via wave/forge.