diff --git a/MODULE.bazel b/MODULE.bazel index 10ae0f8..de613b8 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -38,10 +38,10 @@ nix_repo = use_extension( ) nix_repo.github( name = "nixpkgs", - org = "NixOS", - repo = "nixpkgs", # nixos-unstable with Rocq 9.0.1, coq-hammer, coqutil (2026-04-01) commit = "6201e203d09599479a3b3450ed24fa81537ebc4e", + org = "NixOS", + repo = "nixpkgs", sha256 = "", # Will be computed on first fetch ) use_repo(nix_repo, "nixpkgs") @@ -49,14 +49,18 @@ use_repo(nix_repo, "nixpkgs") # Rocq toolchain extension - uses nixpkgs for hermetic Rocq/Coq rocq = use_extension("//rocq:extensions.bzl", "rocq") rocq.toolchain( + strategy = "nix", # Hermetic nix-based installation version = "9.0", # Rocq 9.0.1 (required for real RocqOfRust library) - strategy = "nix", # Hermetic nix-based installation with_rocq_of_rust_deps = True, # Include coqutil, hammer, smpl ) + # smpl is built from source (rocq-9.0 branch) since nixpkgs only has up to Coq 8.15 # rocq_stdlib is the separate stdlib package for Rocq 9.0 # hammer_tactics is a separate package from hammer (plugin vs library) -use_repo(rocq, "rocq_toolchains", "rocq_stdlib", "rocq_coqutil", "rocq_hammer", "rocq_hammer_tactics", "rocq_smpl") +# flocq/interval/coquelicot/gappa_bin/gappalib enable machine-checked +# floating-point error-bound proofs (#37); gappalib is built from source +# against Flocq, same as smpl is built from source against Rocq 9.0 +use_repo(rocq, "rocq_coquelicot", "rocq_coqutil", "rocq_flocq", "rocq_gappa_bin", "rocq_gappalib", "rocq_hammer", "rocq_hammer_tactics", "rocq_interval", "rocq_smpl", "rocq_stdlib", "rocq_toolchains") # Register Rocq toolchain register_toolchains("@rocq_toolchains//:all") @@ -101,7 +105,7 @@ rocq_of_rust.toolchain( # Uses pinned default: 877dd65142b3c5217ce6ae043ff49c8f540eb8a5 use_real_library = True, # Full library with coqutil + hammer + smpl ) -use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_build") +use_repo(rocq_of_rust, "rocq_of_rust_build", "rocq_of_rust_toolchains") # Register rocq-of-rust toolchain register_toolchains("@rocq_of_rust_toolchains//:toolchain") diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index a8c2eb2..fa8c173 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -19,14 +19,16 @@ artifacts: - id: REQ-002 type: requirement title: The toolchain shall support machine-checked floating-point error-bound proofs, kernel-replaying every Gappa certificate - status: draft + status: implemented priority: must description: > - Add Flocq (fp model), Coq-Gappa + the `gappa` binary (rounding-error - layer), and Coq-Interval (approximation-error layer) to the toolchain - flake, pinned against the bundled Rocq version. Any rule built on top of - Gappa must satisfy CC-002 — the Gappa-emitted proof term is always - replayed through the Rocq kernel, never trusted as-is. + Add Flocq (fp model), the `gappa` binary (rounding-error layer), + gappalib-coq (Gappa's Rocq support library, built from source against + Flocq — nixpkgs has no `coq-gappa` package at this pin), and Coq-Interval + + Coquelicot (approximation-error layer) to the toolchain flake, pinned + against the bundled Rocq version. Any rule built on top of Gappa must + satisfy CC-002 — the Gappa-emitted proof term is always replayed through + the Rocq kernel, never trusted as-is. fields: category: functional upstream-ref: "pulseengine/rules_rocq_rust#37" @@ -76,16 +78,27 @@ artifacts: capability. fields: decision: > - Add coq-flocq, coq-gappa (+ the gappa binary), coq-interval, and - coq-coquelicot to the Nix-pinned toolchain flake, exposing their - .vo/include paths so `rocq_library` can depend on them (or a thin - `gappa_proof` rule wrapping the gappa-to-Rocq flow). A complete kernel - bound = Gappa (rounding, semi-automatic via interval arithmetic + - rewriting) + Coq-Interval (approximation, Taylor-model/interval bounds - on the minimax remainder) + Flocq (the underlying fp model) — and - whatever wraps Gappa must always kernel-check its emitted Flocq proof - term, never accept Gappa's own certificate-generation success as - sufficient (see the controller-constraint on gappa-wrapping rules). + Add coq-flocq, coq-interval, and coq-coquelicot to the Nix-pinned + toolchain flake via nixpkgs (coqPackages.flocq/interval/coquelicot, + already built against the exact same Rocq 9.0.1 as the rest of the + toolchain), plus the standalone `gappa` binary (nixpkgs `gappa`, an + external CLI, not a Coq plugin). nixpkgs has no `coq-gappa`/ + gappalib-coq package at this pin, so gappalib-coq (Gappa's Rocq + support library — the `Gappa.Gappa_library` that Gappa's `-Bcoq` + output `Require Import`s) is built from source against Flocq, the + same way `smpl` is already built from source for this Rocq version + (see gappalib_repository.bzl). A `gappa_proof` Bazel macro + (rocq:defs.bzl) wraps the gappa-to-Rocq flow: it runs `gappa -Bcoq` + in a genrule, then always compiles the emitted `.v` with + `rocq_library` — there is no separate "gappa succeeded" status, + only a normal coqc build that fails if the kernel rejects the proof. + A complete kernel bound = Gappa (rounding, semi-automatic via + interval arithmetic + rewriting) + Coq-Interval (approximation, + Taylor-model/interval bounds on the minimax remainder) + Flocq (the + underlying fp model) — and whatever wraps Gappa must always + kernel-check its emitted Flocq proof term, never accept Gappa's own + certificate-generation success as sufficient (see the + controller-constraint on gappa-wrapping rules). rationale: > Gappa is semi-automatic and emits a Flocq/Rocq proof term the kernel checks — dramatically less manual labor than hand-written Rocq for the @@ -108,16 +121,20 @@ artifacts: - id: FEAT-001 type: feature title: Machine-checked FP error-bound proofs (Flocq + Gappa + Coq-Interval) - status: draft + status: implemented description: > Toolchain capability requested in #37, enabling a raise-assurance proof on top of relay's existing exhaustive-enumeration empirical bound. + Verified via `bazel test //examples/gappa_proof:rounding_bound_test`, + which exercises the full chain: a `.gappa` rounding-bound statement, + Gappa's `-Bcoq` codegen, and a real Rocq kernel check of the emitted + proof term against gappalib-coq/Flocq — PASSED. fields: - phase: future + phase: phase-1 acceptance-criteria: - - "Toolchain flake provides coq-flocq, coq-gappa (+ gappa binary), coq-interval, coq-coquelicot, pinned against the bundled Rocq version" - - "rocq_library (or a new gappa_proof rule) can depend on the new packages' .vo/include paths" - - "A minimal example proves one f32 rounding bound end-to-end, kernel-checked by Rocq, as the template for relay's kernels" + - "Toolchain flake provides flocq, gappa (binary), gappalib-coq, interval, coquelicot, pinned against the bundled Rocq version -- DONE (rocq/extensions.bzl, rocq/private/gappalib_repository.bzl)" + - "rocq_library (or a new gappa_proof rule) can depend on the new packages' .vo/include paths -- DONE (gappa_proof macro, rocq/defs.bzl)" + - "A minimal example proves one f32 rounding bound end-to-end, kernel-checked by Rocq, as the template for relay's kernels -- DONE (examples/gappa_proof, bazel test PASSED)" links: - type: satisfies target: REQ-002 diff --git a/examples/gappa_proof/BUILD.bazel b/examples/gappa_proof/BUILD.bazel new file mode 100644 index 0000000..0871e5f --- /dev/null +++ b/examples/gappa_proof/BUILD.bazel @@ -0,0 +1,19 @@ +# Minimal machine-checked floating-point error-bound proof (#37 / FEAT-001). +# +# Template for relay's flight-math kernels: a `.gappa` rounding-bound +# statement, compiled through Gappa's `-Bcoq` backend and kernel-checked by +# Rocq via gappa_proof (rocq:defs.bzl) -- never trusting Gappa's certificate +# on its own (rivet CC-002). + +load("@rules_rocq_rust//rocq:defs.bzl", "gappa_proof", "rocq_proof_test") + +gappa_proof( + name = "rounding_bound", + src = "rounding_bound.gappa", +) + +rocq_proof_test( + name = "rounding_bound_test", + srcs = [], + deps = [":rounding_bound"], +) diff --git a/examples/gappa_proof/rounding_bound.gappa b/examples/gappa_proof/rounding_bound.gappa new file mode 100644 index 0000000..03e5013 --- /dev/null +++ b/examples/gappa_proof/rounding_bound.gappa @@ -0,0 +1,13 @@ +# Minimal machine-checked floating-point error-bound proof (#37 / FEAT-001). +# +# Claim: rounding any x in [1, 2] to the nearest ieee_32 float introduces an +# absolute error of at most 2^-24 (one ULP at that exponent). +# +# `gappa -Bcoq` turns this statement into a Rocq proof script built on top of +# Flocq (via gappalib-coq's Gappa_library); see rocq/defs.bzl's gappa_proof +# macro, which always kernel-checks the emitted script with coqc rather than +# trusting Gappa's own certificate-generation success (rivet CC-002). + +@rnd = float; + +{ x in [1,2] -> |rnd(x) - x| <= 1b-24 } diff --git a/rocq/defs.bzl b/rocq/defs.bzl index 9b4d5fa..6ed2982 100644 --- a/rocq/defs.bzl +++ b/rocq/defs.bzl @@ -4,3 +4,37 @@ load("//rocq/private:rocq.bzl", _rocq_library = "rocq_library", _rocq_proof_test rocq_library = _rocq_library rocq_proof_test = _rocq_proof_test + +def gappa_proof(name, src, deps = [], extra_flags = [], visibility = None): + """Runs `gappa -Bcoq` on a `.gappa` source and kernel-checks the result. + + Gappa establishes a floating-point rounding-error bound outside Rocq and + emits a Flocq/Rocq proof term as its certificate. Per rivet CC-002, that + certificate is never trusted on its own: this macro always compiles the + emitted proof term with `rocq_library`, so the target fails exactly like + any other Rocq proof if the kernel rejects what Gappa produced. + + Args: + name: name of the resulting rocq_library target. + src: the `.gappa` input file. + deps: rocq_library deps for the generated proof (e.g. other rocq_library + targets); Flocq and Gappa's own support library are already + available toolchain-wide and don't need to be listed here. + extra_flags: extra flags forwarded to coqc, as in rocq_library. + visibility: visibility for the resulting rocq_library target. + """ + generated = name + "_generated.v" + native.genrule( + name = name + "_gen", + srcs = [src], + outs = [generated], + cmd = "$(location @rocq_gappa_bin//:gappa) -Bcoq $(location %s) > $@" % src, + tools = ["@rocq_gappa_bin//:gappa"], + ) + rocq_library( + name = name, + srcs = [generated], + deps = deps, + extra_flags = extra_flags, + visibility = visibility, + ) diff --git a/rocq/extensions.bzl b/rocq/extensions.bzl index ab4debe..e04bb03 100644 --- a/rocq/extensions.bzl +++ b/rocq/extensions.bzl @@ -6,7 +6,8 @@ Supports Rocq 9.0.1+ and includes required external packages for rocq-of-rust. This extension creates its own nixpkgs repository internally for bzlmod compatibility. """ -load("@rules_nixpkgs_core//:nixpkgs.bzl", "nixpkgs_package", "nixpkgs_local_repository") +load("@rules_nixpkgs_core//:nixpkgs.bzl", "nixpkgs_local_repository", "nixpkgs_package") +load("//rocq/private:gappalib_repository.bzl", "gappalib_source") load("//rocq/private:smpl_repository.bzl", "smpl_source") # Default nixpkgs commit (nixos-unstable with Rocq 9.0.1) @@ -102,6 +103,10 @@ rocq_toolchain_info( hammer_tactics_ocaml_plugins = "@rocq_hammer_tactics//:ocaml_plugins", smpl = "@rocq_smpl//:smpl", smpl_ocaml_plugins = "@rocq_smpl//:ocaml_plugins", + flocq = "@rocq_flocq//:flocq", + interval = "@rocq_interval//:interval", + coquelicot = "@rocq_coquelicot//:coquelicot", + gappalib = "@rocq_gappalib//:gappalib", ) # Register as toolchain @@ -205,6 +210,59 @@ filegroup( ) ''' +# BUILD file for Flocq (floating-point formalization library) +_FLOCQ_BUILD_FILE = ''' +package(default_visibility = ["//visibility:public"]) + +filegroup( + name = "flocq", + srcs = glob([ + "lib/coq/**/*.vo", + "lib/coq/**/*.glob", + ], allow_empty = True), +) +''' + +# BUILD file for Coq-Interval (interval arithmetic / approximation-error bounds) +_INTERVAL_BUILD_FILE = ''' +package(default_visibility = ["//visibility:public"]) + +filegroup( + name = "interval", + srcs = glob([ + "lib/coq/**/*.vo", + "lib/coq/**/*.glob", + ], allow_empty = True), +) +''' + +# BUILD file for Coquelicot (real analysis library, Coq-Interval's dependency) +_COQUELICOT_BUILD_FILE = ''' +package(default_visibility = ["//visibility:public"]) + +filegroup( + name = "coquelicot", + srcs = glob([ + "lib/coq/**/*.vo", + "lib/coq/**/*.glob", + ], allow_empty = True), +) +''' + +# BUILD file for the standalone gappa binary (external rounding/approximation prover) +# Gappa is not a Coq plugin -- it's an external CLI whose `-Bcoq` mode emits a +# Rocq proof script (see gappa_proof in coq_of_rust:defs.bzl / rocq:defs.bzl, +# and rivet CC-002: the emitted script is always kernel-checked, never trusted +# as-is). +_GAPPA_BIN_BUILD_FILE = ''' +package(default_visibility = ["//visibility:public"]) + +filegroup( + name = "gappa", + srcs = ["bin/gappa"], +) +''' + # BUILD file for Rocq stdlib (separate from rocq-core in 9.0) # Stdlib is at lib/coq/9.0/user-contrib/Stdlib _STDLIB_BUILD_FILE = ''' @@ -233,6 +291,7 @@ def _rocq_impl(module_ctx): Includes optional dependencies for rocq-of-rust (coqutil, hammer, smpl). Creates its own nixpkgs repository for bzlmod compatibility. """ + # Collect toolchain configurations from all modules toolchains = [] for mod in module_ctx.modules: @@ -316,6 +375,50 @@ import (builtins.fetchTarball {{ branch = "rocq-9.0", ) + # Flocq - floating-point formalization library (#37) + nixpkgs_package( + name = "rocq_flocq", + repository = nixpkgs_repo, + attribute_path = "coqPackages.flocq", + build_file_content = _FLOCQ_BUILD_FILE, + ) + + # Coq-Interval - approximation-error (minimax remainder) bounds (#37) + nixpkgs_package( + name = "rocq_interval", + repository = nixpkgs_repo, + attribute_path = "coqPackages.interval", + build_file_content = _INTERVAL_BUILD_FILE, + ) + + # Coquelicot - real analysis library, Coq-Interval's dependency (#37) + nixpkgs_package( + name = "rocq_coquelicot", + repository = nixpkgs_repo, + attribute_path = "coqPackages.coquelicot", + build_file_content = _COQUELICOT_BUILD_FILE, + ) + + # gappa - standalone rounding-error prover binary (#37). nixpkgs has no + # coq-gappa/gappalib-coq package for this Rocq version, only the CLI; + # the matching Rocq support library is built from source below. + nixpkgs_package( + name = "rocq_gappa_bin", + repository = nixpkgs_repo, + attribute_path = "gappa", + build_file_content = _GAPPA_BIN_BUILD_FILE, + ) + + # gappalib-coq - Gappa's Rocq support library, built from source + # against this toolchain's Flocq (see gappalib_repository.bzl for why + # nixpkgs can't provide this directly, and CC-002 for why the emitted + # proof term must always be kernel-checked rather than trusted as-is) + gappalib_source( + name = "rocq_gappalib", + version = "1.10.0", + nixpkgs_commit = _DEFAULT_NIXPKGS_COMMIT, + ) + # Return extension metadata (reproducible for caching) return module_ctx.extension_metadata(reproducible = True) diff --git a/rocq/private/gappalib_repository.bzl b/rocq/private/gappalib_repository.bzl new file mode 100644 index 0000000..8ec4d76 --- /dev/null +++ b/rocq/private/gappalib_repository.bzl @@ -0,0 +1,158 @@ +"""Repository rule for building gappalib-coq from source using nix. + +gappalib-coq is Gappa's Rocq/Coq support library: Gappa's `-Bcoq` backend +emits a proof script that `Require Import Gappa.Gappa_library`, built on top +of Flocq. nixpkgs has no `coq-gappa`/`gappalib-coq` package -- only the +standalone `gappa` binary -- so this is built from source the same way +`smpl` is (see smpl_repository.bzl), for the same reason: nixpkgs's Coq +package set doesn't cover it for this Rocq version. + +The interactive `gappa` tactic plugin (src/Gappa_tactic.v, an OCaml ML +plugin invoked as `Declare ML Module "coq-gappa.tactic"`) is intentionally +excluded from the build. This toolchain drives Gappa as an external CLI +(`gappa -Bcoq`) whose emitted proof term is always replayed through the Rocq +kernel by a normal rocq_library compile (see rivet CC-002) -- it never needs +the in-Coq tactic, and building the ML plugin would require the same +findlib/META/.cmxs machinery as the Hammer and smpl plugins for no payoff. + +Source: https://gitlab.inria.fr/gappa/coq +""" + +_GAPPALIB_REPO = "https://gitlab.inria.fr/gappa/coq" +_DEFAULT_VERSION = "1.10.0" + +# Nix expression to build gappalib-coq against the toolchain's pinned Flocq. +_GAPPALIB_NIX_EXPR = ''' +{ pkgs ? import {} }: + +let + # Use coq_9_0 to match the exact Rocq toolchain version, and its matching + # Flocq build (coqPackages.flocq is built against the same coq_9_0 in this + # nixpkgs snapshot -- see rocq/extensions.bzl's rocq_flocq package). + coq = pkgs.coq_9_0; + flocq = pkgs.coqPackages.flocq; +in +pkgs.stdenv.mkDerivation { + pname = "gappalib-coq"; + version = "1.10.0"; + + src = ./.; + + nativeBuildInputs = [ coq ]; + buildInputs = [ coq flocq ]; + + buildPhase = \'\' + export COQBIN="${coq}/bin/" + { + echo "-R src Gappa" + echo "-I src" + echo "-Q ${flocq}/lib/coq/${coq.coq-version}/user-contrib/Flocq Flocq" + for f in src/*.v; do + [ "$(basename "$f")" = "Gappa_tactic.v" ] && continue + echo "$f" + done + } > _CoqProject + ${coq}/bin/coq_makefile -f _CoqProject -o Makefile.coq + make -f Makefile.coq -j$NIX_BUILD_CORES + \'\'; + + installPhase = \'\' + mkdir -p $out/lib/coq/${coq.coq-version}/user-contrib/Gappa + cp src/*.vo src/*.glob $out/lib/coq/${coq.coq-version}/user-contrib/Gappa/ + \'\'; +} +''' + +def _gappalib_source_impl(repository_ctx): + """Download and build gappalib-coq from source using nix-build. + + gappalib-coq is a pure .v theory library (no ML plugin needed for our + use), so unlike smpl this only needs a .vo build, not a native plugin. + """ + version = repository_ctx.attr.version + sha256 = repository_ctx.attr.sha256 + nixpkgs_commit = repository_ctx.attr.nixpkgs_commit + + repository_ctx.report_progress("Downloading gappalib-coq source ({})".format(version)) + + url = "{}/-/archive/gappalib-coq-{v}/coq-gappalib-coq-{v}.tar.gz".format( + _GAPPALIB_REPO, + v = version, + ) + + download_kwargs = { + "url": url, + "stripPrefix": "coq-gappalib-coq-{}".format(version), + } + if sha256: + download_kwargs["sha256"] = sha256 + + repository_ctx.download_and_extract(**download_kwargs) + + nix_build = repository_ctx.which("nix-build") + if not nix_build: + fail( + "gappalib_source requires nix-build to compile gappalib-coq " + + "against this toolchain's pinned Flocq. Install Nix (see README " + + "Prerequisites) -- there is no non-Nix fallback for this package.", + ) + + repository_ctx.file("default.nix", _GAPPALIB_NIX_EXPR) + + repository_ctx.report_progress( + "Building gappalib-coq with nix-build (nixpkgs {})".format(nixpkgs_commit[:12]), + ) + + nix_expr = "import ./default.nix {{ pkgs = import (fetchTarball \"https://github.com/NixOS/nixpkgs/archive/{}.tar.gz\") {{}}; }}".format(nixpkgs_commit) + + build_result = repository_ctx.execute( + [str(nix_build), "--no-out-link", "-E", nix_expr], + timeout = 600, + ) + + if build_result.return_code != 0: + fail("nix-build failed for gappalib-coq: {}".format(build_result.stderr)) + + nix_store_path = build_result.stdout.strip() + repository_ctx.report_progress("gappalib-coq built at {}".format(nix_store_path)) + + repository_ctx.symlink(nix_store_path, "nix-out") + + build_content = '''# Generated BUILD.bazel for gappalib-coq (nix-built) +# gappalib-coq is Gappa's Rocq/Coq support library, built on top of Flocq. + +package(default_visibility = ["//visibility:public"]) + +filegroup( + name = "gappalib", + srcs = glob([ + "nix-out/lib/coq/**/*.vo", + "nix-out/lib/coq/**/*.glob", + ], allow_empty = True), +) + +filegroup( + name = "theories_src", + srcs = glob(["src/**/*.v"]), +) +''' + repository_ctx.file("BUILD.bazel", build_content) + +gappalib_source = repository_rule( + implementation = _gappalib_source_impl, + attrs = { + "version": attr.string( + default = _DEFAULT_VERSION, + doc = "gappalib-coq release tag to use", + ), + "sha256": attr.string( + default = "", + doc = "SHA256 of the source archive", + ), + "nixpkgs_commit": attr.string( + default = "6201e203d09599479a3b3450ed24fa81537ebc4e", + doc = "Nixpkgs commit hash for reproducible builds", + ), + }, + doc = "Downloads and builds gappalib-coq from source, against this toolchain's pinned Flocq.", +) diff --git a/rocq/toolchain.bzl b/rocq/toolchain.bzl index 3ad87d9..be814ab 100644 --- a/rocq/toolchain.bzl +++ b/rocq/toolchain.bzl @@ -67,6 +67,30 @@ def _rocq_toolchain_info_impl(ctx): if path: extra_libs.append((ctx.files.smpl, "smpl", path)) + # Flocq - floating-point formalization library + if ctx.files.flocq: + path = _find_lib_path(ctx.files.flocq, "/Flocq/", "Flocq") + if path: + extra_libs.append((ctx.files.flocq, "Flocq", path)) + + # Coq-Interval - interval arithmetic / approximation-error bounds + if ctx.files.interval: + path = _find_lib_path(ctx.files.interval, "/Interval/", "Interval") + if path: + extra_libs.append((ctx.files.interval, "Interval", path)) + + # Coquelicot - real analysis library (Coq-Interval's dependency) + if ctx.files.coquelicot: + path = _find_lib_path(ctx.files.coquelicot, "/Coquelicot/", "Coquelicot") + if path: + extra_libs.append((ctx.files.coquelicot, "Coquelicot", path)) + + # gappalib-coq - Gappa's Rocq support library (built from source against Flocq) + if ctx.files.gappalib: + path = _find_lib_path(ctx.files.gappalib, "/Gappa/", "Gappa") + if path: + extra_libs.append((ctx.files.gappalib, "Gappa", path)) + # Compute OCAMLPATH for findlib resolution (needed for Hammer plugins) # Includes the coq lib path and all OCaml plugin site-lib paths ocaml_paths = [] @@ -82,6 +106,7 @@ def _rocq_toolchain_info_impl(ctx): for plugin_files in [ctx.files.hammer_ocaml_plugins, ctx.files.hammer_tactics_ocaml_plugins, ctx.files.smpl_ocaml_plugins]: if plugin_files: ocaml_plugin_files.extend(plugin_files) + # Find site-lib directory from the META file paths for f in plugin_files: if "/site-lib/" in f.path: @@ -153,6 +178,22 @@ rocq_toolchain_info = rule( allow_files = True, doc = "smpl OCaml findlib plugin files (optional)", ), + "flocq": attr.label( + allow_files = True, + doc = "Flocq library .vo files (optional)", + ), + "interval": attr.label( + allow_files = True, + doc = "Coq-Interval library .vo files (optional)", + ), + "coquelicot": attr.label( + allow_files = True, + doc = "Coquelicot library .vo files (optional)", + ), + "gappalib": attr.label( + allow_files = True, + doc = "gappalib-coq (Gappa's Rocq support library) .vo files (optional)", + ), }, doc = "Provides Rocq toolchain information", )