diff --git a/MODULE.bazel b/MODULE.bazel index 46f0aed..941edbc 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -38,7 +38,7 @@ nix_repo.github( name = "nixpkgs", org = "NixOS", repo = "nixpkgs", - # nixos-unstable with Rocq 9.0.1, coq-hammer, coqutil (2026-04-01) + # nixos-unstable with Rocq 9.1.1, coq-hammer, coqutil (2026-04-01) commit = "6201e203d09599479a3b3450ed24fa81537ebc4e", sha256 = "", # Will be computed on first fetch ) @@ -47,12 +47,12 @@ use_repo(nix_repo, "nixpkgs") # Rocq toolchain extension - uses nixpkgs for hermetic Rocq/Coq rocq = use_extension("//rocq:extensions.bzl", "rocq") rocq.toolchain( - version = "9.0", # Rocq 9.0.1 (required for real RocqOfRust library) + version = "9.1", # Rocq 9.1.1 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 +# smpl is built from source (rocq-9.0 branch, works with 9.0+) 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") diff --git a/examples/rust_to_rocq/MODULE.bazel b/examples/rust_to_rocq/MODULE.bazel index 359207b..11802c0 100644 --- a/examples/rust_to_rocq/MODULE.bazel +++ b/examples/rust_to_rocq/MODULE.bazel @@ -27,7 +27,7 @@ nix_repo.github( name = "nixpkgs", org = "NixOS", repo = "nixpkgs", - # nixos-unstable with Rocq 9.0.1 (2026-04-01) + # nixos-unstable with Rocq 9.1.1 (2026-04-01) commit = "6201e203d09599479a3b3450ed24fa81537ebc4e", sha256 = "", ) @@ -36,7 +36,7 @@ use_repo(nix_repo, "nixpkgs") # Rocq toolchain rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq") rocq.toolchain( - version = "9.0", + version = "9.1", strategy = "nix", with_rocq_of_rust_deps = True, ) diff --git a/rocq/extensions.bzl b/rocq/extensions.bzl index ab4debe..d3d01e7 100644 --- a/rocq/extensions.bzl +++ b/rocq/extensions.bzl @@ -1,7 +1,7 @@ """Module extensions for using rules_rocq with bzlmod. Provides Rocq/Coq toolchain setup using nixpkgs for hermetic builds. -Supports Rocq 9.0.1+ and includes required external packages for rocq-of-rust. +Supports Rocq 9.0+ and includes required external packages for rocq-of-rust. This extension creates its own nixpkgs repository internally for bzlmod compatibility. """ @@ -9,7 +9,7 @@ This extension creates its own nixpkgs repository internally for bzlmod compatib load("@rules_nixpkgs_core//:nixpkgs.bzl", "nixpkgs_package", "nixpkgs_local_repository") load("//rocq/private:smpl_repository.bzl", "smpl_source") -# Default nixpkgs commit (nixos-unstable with Rocq 9.0.1) +# Default nixpkgs commit (nixos-unstable with Rocq 9.1.1) _DEFAULT_NIXPKGS_COMMIT = "6201e203d09599479a3b3450ed24fa81537ebc4e" # Tag classes for Rocq toolchain configuration @@ -17,8 +17,8 @@ _RocqToolchainTag = tag_class( doc = "Tags for defining Rocq toolchains", attrs = { "version": attr.string( - doc = "Rocq/Coq version to use (e.g., '9.0', '8.20')", - default = "9.0", + doc = "Rocq/Coq version to use (e.g., '9.1', '9.0', '8.20')", + default = "9.1", ), "strategy": attr.string( doc = "Tool acquisition strategy: 'nix' for hermetic nixpkgs", @@ -32,18 +32,32 @@ _RocqToolchainTag = tag_class( }, ) +# Map Rocq/Coq version to nixpkgs attribute paths. +# Each entry maps to (compiler_attr, coqPackages_set) so dependencies +# are resolved from the correct version-specific package set. +_VERSION_MAP = { + "9.1": ("coq_9_1", "coqPackages_9_1"), + "9.0": ("coq_9_0", "coqPackages_9_0"), + "8.20": ("coq_8_20", "coqPackages_8_20"), + "8.19": ("coq_8_19", "coqPackages_8_19"), + "8.18": ("coq_8_18", "coqPackages_8_18"), + "8.17": ("coq_8_17", "coqPackages_8_17"), + "8.16": ("coq_8_16", "coqPackages_8_16"), +} + def _get_rocq_attr(version): - """Map Rocq/Coq version to nixpkgs attribute path.""" - version_map = { - "9.0": "coq_9_0", - "8.20": "coq_8_20", - "8.19": "coq_8_19", - "8.18": "coq_8_18", - "8.17": "coq_8_17", - "8.16": "coq_8_16", - "latest": "coq", - } - return version_map.get(version, "coq_9_0") + """Map Rocq/Coq version to nixpkgs compiler attribute path.""" + entry = _VERSION_MAP.get(version) + if entry: + return entry[0] + return "coq_9_1" + +def _get_coq_packages(version): + """Map Rocq/Coq version to nixpkgs coqPackages set name.""" + entry = _VERSION_MAP.get(version) + if entry: + return entry[1] + return "coqPackages_9_1" # BUILD file content for the main Rocq toolchain package # Note: For Rocq 9.0+, the stdlib is a separate package (@rocq_stdlib) @@ -205,8 +219,8 @@ filegroup( ) ''' -# BUILD file for Rocq stdlib (separate from rocq-core in 9.0) -# Stdlib is at lib/coq/9.0/user-contrib/Stdlib +# BUILD file for Rocq stdlib (separate from rocq-core in 9.0+) +# Stdlib is at lib/coq/{version}/user-contrib/Stdlib _STDLIB_BUILD_FILE = ''' package(default_visibility = ["//visibility:public"]) @@ -245,10 +259,11 @@ def _rocq_impl(module_ctx): rocq_version = config.version with_deps = config.with_rocq_of_rust_deps else: - rocq_version = "9.0" + rocq_version = "9.1" with_deps = True rocq_attr = _get_rocq_attr(rocq_version) + coq_packages = _get_coq_packages(rocq_version) # Create internal nixpkgs repository for bzlmod compatibility # Extensions can't see repositories from other modules, so we define our own @@ -273,13 +288,14 @@ import (builtins.fetchTarball {{ build_file_content = _ROCQ_BUILD_FILE, ) - # Create Rocq stdlib (needed for Rocq 9.0) - # Rocq 9.0 has separate stdlib package - if rocq_version == "9.0": + # Create Rocq stdlib (separate package for Rocq 9.0+) + if rocq_version in ("9.0", "9.1", "9.2"): + # Use version-specific rocqPackages set for stdlib + stdlib_attr = "rocqPackages_{}.stdlib".format(rocq_version.replace(".", "_")) nixpkgs_package( name = "rocq_stdlib", repository = nixpkgs_repo, - attribute_path = "rocqPackages.stdlib", + attribute_path = stdlib_attr, build_file_content = _STDLIB_BUILD_FILE, ) @@ -289,7 +305,7 @@ import (builtins.fetchTarball {{ nixpkgs_package( name = "rocq_coqutil", repository = nixpkgs_repo, - attribute_path = "coqPackages.coqutil", + attribute_path = "{}.coqutil".format(coq_packages), build_file_content = _COQUTIL_BUILD_FILE, ) @@ -297,7 +313,7 @@ import (builtins.fetchTarball {{ nixpkgs_package( name = "rocq_hammer", repository = nixpkgs_repo, - attribute_path = "coqPackages.coq-hammer", + attribute_path = "{}.coq-hammer".format(coq_packages), build_file_content = _HAMMER_BUILD_FILE, ) @@ -305,15 +321,17 @@ import (builtins.fetchTarball {{ nixpkgs_package( name = "rocq_hammer_tactics", repository = nixpkgs_repo, - attribute_path = "coqPackages.coq-hammer-tactics", + attribute_path = "{}.coq-hammer-tactics".format(coq_packages), build_file_content = _HAMMER_TACTICS_BUILD_FILE, ) - # smpl - extensible simplification tactic (built from source for Rocq 9.0) - # The nixpkgs version only supports up to Coq 8.15 + # smpl - extensible simplification tactic (built from source) + # The nixpkgs version only supports up to Coq 8.15, so we build from + # the rocq-9.0 branch which declares rocq-core >= 9.0 (works with 9.1+) smpl_source( name = "rocq_smpl", branch = "rocq-9.0", + rocq_nix_attr = rocq_attr, ) # Return extension metadata (reproducible for caching) diff --git a/rocq/private/smpl_repository.bzl b/rocq/private/smpl_repository.bzl index 72538a3..eb394b8 100644 --- a/rocq/private/smpl_repository.bzl +++ b/rocq/private/smpl_repository.bzl @@ -2,7 +2,7 @@ smpl is a Coq/Rocq plugin providing an extensible tactic. The nixpkgs version only supports up to Coq 8.15, so we build from source -for Rocq 9.0 compatibility using nix-build. +for Rocq 9.0+ compatibility using nix-build. Source: https://github.com/uds-psl/smpl """ @@ -10,19 +10,19 @@ Source: https://github.com/uds-psl/smpl _SMPL_REPO = "https://github.com/uds-psl/smpl" _DEFAULT_BRANCH = "rocq-9.0" -# Nix expression to build smpl -_SMPL_NIX_EXPR = ''' -{ pkgs ? import {} }: +def _smpl_nix_expr(rocq_nix_attr): + """Generate nix expression to build smpl against a specific Rocq version.""" + return ''' +{{ pkgs ? import {{}} }}: let - # Use coq_9_0 to match the exact Rocq toolchain version - # coqPackages.coq may use a different default version - coq = pkgs.coq_9_0; + # Use version-specific Rocq to match the toolchain + coq = pkgs.{rocq_attr}; ocamlPackages = coq.ocamlPackages; in -pkgs.stdenv.mkDerivation { +pkgs.stdenv.mkDerivation {{ pname = "smpl"; - version = "rocq-9.0"; + version = "{rocq_attr}";'''.format(rocq_attr = rocq_nix_attr) + ''' src = ./.; @@ -99,8 +99,9 @@ def _smpl_source_impl(repository_ctx): _generate_sources_only_build(repository_ctx) return - # Write nix expression - repository_ctx.file("default.nix", _SMPL_NIX_EXPR) + # Write nix expression with version-specific Rocq attribute + rocq_nix_attr = repository_ctx.attr.rocq_nix_attr + repository_ctx.file("default.nix", _smpl_nix_expr(rocq_nix_attr)) # Build with nix-build using pinned nixpkgs commit for reproducibility repository_ctx.report_progress("Building smpl with nix-build (nixpkgs {})".format(nixpkgs_commit[:12])) @@ -283,6 +284,10 @@ smpl_source = repository_rule( default = "6201e203d09599479a3b3450ed24fa81537ebc4e", doc = "Nixpkgs commit hash for reproducible builds", ), + "rocq_nix_attr": attr.string( + default = "coq_9_1", + doc = "Nixpkgs attribute for the Rocq compiler (e.g., 'coq_9_1', 'coq_9_0')", + ), }, - doc = "Downloads and builds smpl from source for Rocq 9.0 using nix.", + doc = "Downloads and builds smpl from source for Rocq 9.0+ using nix.", )