chore: upgrade Rocq 9.0 → 9.1

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")
 

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,
 )

rocq/extensions.bzl

@@ -1,24 +1,24 @@
 """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.
 """
 
 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
 _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,31 +305,33 @@ 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,
         )
 
         # coq-hammer - automated reasoning plugin
         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,
         )
 
         # coq-hammer-tactics - Hammer.Tactics library (separate from plugin)
         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)

rocq/private/smpl_repository.bzl

@@ -2,27 +2,27 @@
 
 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
 """
 
 _SMPL_REPO = "https://github.com/uds-psl/smpl"
 _DEFAULT_BRANCH = "rocq-9.0"
 
-# Nix expression to build smpl
-_SMPL_NIX_EXPR = '''
-{ pkgs ? import <nixpkgs> {} }:
+def _smpl_nix_expr(rocq_nix_attr):
+    """Generate nix expression to build smpl against a specific Rocq version."""
+    return '''
+{{ pkgs ? import <nixpkgs> {{}} }}:
 
 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.",
 )