feat: use rules_nixpkgs for hermetic Coq toolchain #17
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Switch from attempting to download Rocq Platform binaries (which are only available for macOS ARM64 and Windows) to using nixpkgs for hermetic Coq installation. This provides: - Cross-platform support (Linux x86_64/arm64, macOS x86_64/arm64) - Hermetic builds via nix - Multiple Coq versions (8.20, 8.19, 8.18, etc.) Changes: - Add rules_nixpkgs_core dependency to MODULE.bazel - Configure nixpkgs repository with nixos-24.11 stable channel - Create rocq_nix_toolchain.bzl using nixpkgs_package - Update extensions.bzl to use nix-based toolchain - Simplify MODULE.bazel (remove broken OCaml/coq_of_rust extensions) - Fix tool_registry.bzl and rocq_toolchain.bzl syntax errors - Add toolchain_type to rocq/BUILD.bazel - Rewrite README with nix installation instructions BREAKING CHANGE: Users must install nix for the toolchain to work. See README.md for installation instructions.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Summary
Switch from attempting to download Rocq Platform binaries to using nixpkgs for hermetic Coq installation.
Why nixpkgs?
The Rocq Platform only provides pre-built binaries for:
No binaries for: Linux (any arch), macOS Intel
nixpkgs provides Coq packages for all platforms:
Changes
rules_nixpkgs_coredependencyrocq_nix_toolchain.bzlusingnixpkgs_packageBreaking Change
Users must install nix for the toolchain to work:
How it works
Test plan
bazel query //rocq/...works