diff --git a/MODULE.bazel b/MODULE.bazel index 0763c37..64de6c3 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -1,7 +1,7 @@ """Bazel Module for Rocq and coq-of-rust Rules -This module provides Bazel rules for Rocq theorem proving and coq-of-rust integration. -Following the patterns established by rules_rust and rules_wasm_component. +This module provides Bazel rules for Rocq/Coq theorem proving. +Uses nixpkgs for hermetic Coq toolchain installation. """ module( @@ -10,64 +10,38 @@ module( compatibility_level = 1, ) -# Core dependencies following rules_rust patterns -bazel_dep(name = "rules_rust", version = "0.68.1") -bazel_dep(name = "rules_cc", version = "0.2.14") +# Core dependencies bazel_dep(name = "bazel_skylib", version = "1.8.2") bazel_dep(name = "platforms", version = "1.0.0") +# Nix integration for hermetic Coq/Rocq toolchain +bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0") + +# Configure nixpkgs repository for Coq/Rocq toolchain +nix_repo = use_extension( + "@rules_nixpkgs_core//extensions:repository.bzl", + "nix_repo", +) +nix_repo.github( + name = "nixpkgs", + org = "NixOS", + repo = "nixpkgs", + # nixos-24.11 stable channel + commit = "d4f247e89f6e10120f911e2e2d2254a050d0f732", + sha256 = "dee2f93be38d1a63ee9b731fa993f0ac2c60c3a62cca32d4cc64c2ed5b8a8e06", +) +use_repo(nix_repo, "nixpkgs") + # Development dependencies bazel_dep(name = "buildifier_prebuilt", version = "6.4.0", dev_dependency = True) -bazel_dep(name = "stardoc", version = "0.7.2", dev_dependency = True) -# Rocq toolchain extension (Bazel 8 symbolic macro pattern) +# Rocq toolchain extension - uses nixpkgs for hermetic Coq rocq = use_extension("//rocq:extensions.bzl", "rocq") rocq.toolchain( - version = "2025.01.0", - strategy = "download", - editions = ["2021"], # Coq/Rocq edition compatibility + version = "8.20", # Coq version from nixpkgs + strategy = "nix", # Hermetic nix-based installation ) use_repo(rocq, "rocq_toolchains") -# Optional OCaml toolchain for QuickChick support -# Only enable this if you need QuickChick or other OCaml-based plugins -ocaml = use_extension("//toolchains:ocaml_extensions.bzl", "ocaml") -ocaml.toolchain( - version = "5.1.1", - strategy = "download", # only hermetic downloads supported -) -use_repo(ocaml, "ocaml_toolchains") - -# coq-of-rust toolchain extension -# Now properly implemented as a buildable toolchain -coq_of_rust = use_extension("//coq_of_rust:extensions.bzl", "coq_of_rust") -coq_of_rust.toolchain( - version = "0.5.0", - strategy = "build", # coq-of-rust must be built from source -) -use_repo(coq_of_rust, "coq_of_rust_toolchains") - -# Register toolchains for target platform resolution -register_toolchains( - "@rocq_toolchains//:rocq_toolchain", - "@coq_of_rust_toolchains//:coq_of_rust_toolchain", -) - -# Rust toolchain setup for coq-of-rust integration -rust = use_extension("@rules_rust//rust:extensions.bzl", "rust") -rust.toolchain( - edition = "2021", - extra_target_triples = [ - "x86_64-unknown-linux-gnu", - "aarch64-unknown-linux-gnu", - "x86_64-apple-darwin", - "aarch64-apple-darwin", - ], - versions = ["1.91.1"], -) -use_repo(rust, "rust_toolchains") - -register_toolchains("@rust_toolchains//:all") - -# Register default C++ toolchains for any C++ dependencies -register_toolchains("@bazel_tools//tools/cpp:all") \ No newline at end of file +# Register Rocq toolchain +register_toolchains("@rocq_toolchains//:all") diff --git a/MODULE.bazel.lock b/MODULE.bazel.lock index 1213a4e..9c1177b 100644 --- a/MODULE.bazel.lock +++ b/MODULE.bazel.lock @@ -1,5 +1,5 @@ { - "lockFileVersion": 24, + "lockFileVersion": 16, "registryFileHashes": { "https://bcr.bazel.build/bazel_registry.json": "8a28e4aff06ee60aed2a8c281907fb8bcbf3b753c91fb5a5c57da3215d5b3497", "https://bcr.bazel.build/modules/abseil-cpp/20210324.2/MODULE.bazel": "7cd0312e064fde87c8d1cd79ba06c876bd23630c83466e9500321be55c96ace2", @@ -10,20 +10,14 @@ "https://bcr.bazel.build/modules/abseil-cpp/20230802.1/MODULE.bazel": "fa92e2eb41a04df73cdabeec37107316f7e5272650f81d6cc096418fe647b915", "https://bcr.bazel.build/modules/abseil-cpp/20240116.1/MODULE.bazel": "37bcdb4440fbb61df6a1c296ae01b327f19e9bb521f9b8e26ec854b6f97309ed", "https://bcr.bazel.build/modules/abseil-cpp/20240116.1/source.json": "9be551b8d4e3ef76875c0d744b5d6a504a27e3ae67bc6b28f46415fd2d2957da", - "https://bcr.bazel.build/modules/apple_support/1.23.1/MODULE.bazel": "53763fed456a968cf919b3240427cf3a9d5481ec5466abc9d5dc51bc70087442", - "https://bcr.bazel.build/modules/apple_support/1.24.1/MODULE.bazel": "f46e8ddad60aef170ee92b2f3d00ef66c147ceafea68b6877cb45bd91737f5f8", - "https://bcr.bazel.build/modules/apple_support/1.24.1/source.json": "cf725267cbacc5f028ef13bb77e7f2c2e0066923a4dab1025e4a0511b1ed258a", "https://bcr.bazel.build/modules/bazel_features/1.1.1/MODULE.bazel": "27b8c79ef57efe08efccbd9dd6ef70d61b4798320b8d3c134fd571f78963dbcd", "https://bcr.bazel.build/modules/bazel_features/1.11.0/MODULE.bazel": "f9382337dd5a474c3b7d334c2f83e50b6eaedc284253334cf823044a26de03e8", "https://bcr.bazel.build/modules/bazel_features/1.15.0/MODULE.bazel": "d38ff6e517149dc509406aca0db3ad1efdd890a85e049585b7234d04238e2a4d", "https://bcr.bazel.build/modules/bazel_features/1.17.0/MODULE.bazel": "039de32d21b816b47bd42c778e0454217e9c9caac4a3cf8e15c7231ee3ddee4d", "https://bcr.bazel.build/modules/bazel_features/1.18.0/MODULE.bazel": "1be0ae2557ab3a72a57aeb31b29be347bcdc5d2b1eb1e70f39e3851a7e97041a", "https://bcr.bazel.build/modules/bazel_features/1.19.0/MODULE.bazel": "59adcdf28230d220f0067b1f435b8537dd033bfff8db21335ef9217919c7fb58", - "https://bcr.bazel.build/modules/bazel_features/1.27.0/MODULE.bazel": "621eeee06c4458a9121d1f104efb80f39d34deff4984e778359c60eaf1a8cb65", - "https://bcr.bazel.build/modules/bazel_features/1.28.0/MODULE.bazel": "4b4200e6cbf8fa335b2c3f43e1d6ef3e240319c33d43d60cc0fbd4b87ece299d", - "https://bcr.bazel.build/modules/bazel_features/1.30.0/MODULE.bazel": "a14b62d05969a293b80257e72e597c2da7f717e1e69fa8b339703ed6731bec87", - "https://bcr.bazel.build/modules/bazel_features/1.32.0/MODULE.bazel": "095d67022a58cb20f7e20e1aefecfa65257a222c18a938e2914fd257b5f1ccdc", - "https://bcr.bazel.build/modules/bazel_features/1.32.0/source.json": "2546c766986a6541f0bacd3e8542a1f621e2b14a80ea9e88c6f89f7eedf64ae1", + "https://bcr.bazel.build/modules/bazel_features/1.21.0/MODULE.bazel": "675642261665d8eea09989aa3b8afb5c37627f1be178382c320d1b46afba5e3b", + "https://bcr.bazel.build/modules/bazel_features/1.21.0/source.json": "3e8379efaaef53ce35b7b8ba419df829315a880cb0a030e5bb45c96d6d5ecb5f", "https://bcr.bazel.build/modules/bazel_features/1.4.1/MODULE.bazel": "e45b6bb2350aff3e442ae1111c555e27eac1d915e77775f6fdc4b351b758b5d7", "https://bcr.bazel.build/modules/bazel_features/1.9.1/MODULE.bazel": "8f679097876a9b609ad1f60249c49d68bfab783dd9be012faf9d82547b14815a", "https://bcr.bazel.build/modules/bazel_skylib/1.0.3/MODULE.bazel": "bcb0fd896384802d1ad283b4e4eb4d718eebd8cb820b0a2c3a347fb971afd9d8", @@ -52,20 +46,17 @@ "https://bcr.bazel.build/modules/jsoncpp/1.9.5/source.json": "4108ee5085dd2885a341c7fab149429db457b3169b86eb081fa245eadf69169d", "https://bcr.bazel.build/modules/libpfm/4.11.0/MODULE.bazel": "45061ff025b301940f1e30d2c16bea596c25b176c8b6b3087e92615adbd52902", "https://bcr.bazel.build/modules/platforms/0.0.10/MODULE.bazel": "8cb8efaf200bdeb2150d93e162c40f388529a25852b332cec879373771e48ed5", - "https://bcr.bazel.build/modules/platforms/0.0.11/MODULE.bazel": "0daefc49732e227caa8bfa834d65dc52e8cc18a2faf80df25e8caea151a9413f", "https://bcr.bazel.build/modules/platforms/0.0.4/MODULE.bazel": "9b328e31ee156f53f3c416a64f8491f7eb731742655a47c9eec4703a71644aee", "https://bcr.bazel.build/modules/platforms/0.0.5/MODULE.bazel": "5733b54ea419d5eaf7997054bb55f6a1d0b5ff8aedf0176fef9eea44f3acda37", "https://bcr.bazel.build/modules/platforms/0.0.6/MODULE.bazel": "ad6eeef431dc52aefd2d77ed20a4b353f8ebf0f4ecdd26a807d2da5aa8cd0615", "https://bcr.bazel.build/modules/platforms/0.0.7/MODULE.bazel": "72fd4a0ede9ee5c021f6a8dd92b503e089f46c227ba2813ff183b71616034814", "https://bcr.bazel.build/modules/platforms/0.0.8/MODULE.bazel": "9f142c03e348f6d263719f5074b21ef3adf0b139ee4c5133e2aa35664da9eb2d", - "https://bcr.bazel.build/modules/platforms/0.0.9/MODULE.bazel": "4a87a60c927b56ddd67db50c89acaa62f4ce2a1d2149ccb63ffd871d5ce29ebc", "https://bcr.bazel.build/modules/platforms/1.0.0/MODULE.bazel": "f05feb42b48f1b3c225e4ccf351f367be0371411a803198ec34a389fb22aa580", "https://bcr.bazel.build/modules/platforms/1.0.0/source.json": "f4ff1fd412e0246fd38c82328eb209130ead81d62dcd5a9e40910f867f733d96", "https://bcr.bazel.build/modules/protobuf/21.7/MODULE.bazel": "a5a29bb89544f9b97edce05642fac225a808b5b7be74038ea3640fae2f8e66a7", "https://bcr.bazel.build/modules/protobuf/27.0/MODULE.bazel": "7873b60be88844a0a1d8f80b9d5d20cfbd8495a689b8763e76c6372998d3f64c", "https://bcr.bazel.build/modules/protobuf/27.1/MODULE.bazel": "703a7b614728bb06647f965264967a8ef1c39e09e8f167b3ca0bb1fd80449c0d", "https://bcr.bazel.build/modules/protobuf/29.0-rc2/MODULE.bazel": "6241d35983510143049943fc0d57937937122baf1b287862f9dc8590fc4c37df", - "https://bcr.bazel.build/modules/protobuf/29.0-rc3/MODULE.bazel": "33c2dfa286578573afc55a7acaea3cada4122b9631007c594bf0729f41c8de92", "https://bcr.bazel.build/modules/protobuf/29.0/MODULE.bazel": "319dc8bf4c679ff87e71b1ccfb5a6e90a6dbc4693501d471f48662ac46d04e4e", "https://bcr.bazel.build/modules/protobuf/29.0/source.json": "b857f93c796750eef95f0d61ee378f3420d00ee1dd38627b27193aa482f4f981", "https://bcr.bazel.build/modules/protobuf/3.19.0/MODULE.bazel": "6b5fbb433f760a99a22b18b6850ed5784ef0e9928a72668b66e4d7ccd47db9b0", @@ -81,15 +72,11 @@ "https://bcr.bazel.build/modules/rules_cc/0.0.14/MODULE.bazel": "5e343a3aac88b8d7af3b1b6d2093b55c347b8eefc2e7d1442f7a02dc8fea48ac", "https://bcr.bazel.build/modules/rules_cc/0.0.15/MODULE.bazel": "6704c35f7b4a72502ee81f61bf88706b54f06b3cbe5558ac17e2e14666cd5dcc", "https://bcr.bazel.build/modules/rules_cc/0.0.16/MODULE.bazel": "7661303b8fc1b4d7f532e54e9d6565771fea666fbdf839e0a86affcd02defe87", + "https://bcr.bazel.build/modules/rules_cc/0.0.16/source.json": "227e83737046aa4f50015da48e98e0d8ab42fd0ec74d8d653b6cc9f9a357f200", "https://bcr.bazel.build/modules/rules_cc/0.0.2/MODULE.bazel": "6915987c90970493ab97393024c156ea8fb9f3bea953b2f3ec05c34f19b5695c", "https://bcr.bazel.build/modules/rules_cc/0.0.6/MODULE.bazel": "abf360251023dfe3efcef65ab9d56beefa8394d4176dd29529750e1c57eaa33f", "https://bcr.bazel.build/modules/rules_cc/0.0.8/MODULE.bazel": "964c85c82cfeb6f3855e6a07054fdb159aced38e99a5eecf7bce9d53990afa3e", "https://bcr.bazel.build/modules/rules_cc/0.0.9/MODULE.bazel": "836e76439f354b89afe6a911a7adf59a6b2518fafb174483ad78a2a2fde7b1c5", - "https://bcr.bazel.build/modules/rules_cc/0.1.1/MODULE.bazel": "2f0222a6f229f0bf44cd711dc13c858dad98c62d52bd51d8fc3a764a83125513", - "https://bcr.bazel.build/modules/rules_cc/0.2.14/MODULE.bazel": "353c99ed148887ee89c54a17d4100ae7e7e436593d104b668476019023b58df8", - "https://bcr.bazel.build/modules/rules_cc/0.2.14/source.json": "55d0a4587c5592fad350f6e698530f4faf0e7dd15e69d43f8d87e220c78bea54", - "https://bcr.bazel.build/modules/rules_cc/0.2.4/MODULE.bazel": "1ff1223dfd24f3ecf8f028446d4a27608aa43c3f41e346d22838a4223980b8cc", - "https://bcr.bazel.build/modules/rules_cc/0.2.8/MODULE.bazel": "f1df20f0bf22c28192a794f29b501ee2018fa37a3862a1a2132ae2940a23a642", "https://bcr.bazel.build/modules/rules_foreign_cc/0.9.0/MODULE.bazel": "c9e8c682bf75b0e7c704166d79b599f93b72cfca5ad7477df596947891feeef6", "https://bcr.bazel.build/modules/rules_fuzzing/0.5.2/MODULE.bazel": "40c97d1144356f52905566c55811f13b299453a14ac7769dfba2ac38192337a8", "https://bcr.bazel.build/modules/rules_fuzzing/0.5.2/source.json": "c8b1e2c717646f1702290959a3302a178fb639d987ab61d548105019f11e527e", @@ -103,10 +90,8 @@ "https://bcr.bazel.build/modules/rules_java/7.2.0/MODULE.bazel": "06c0334c9be61e6cef2c8c84a7800cef502063269a5af25ceb100b192453d4ab", "https://bcr.bazel.build/modules/rules_java/7.3.2/MODULE.bazel": "50dece891cfdf1741ea230d001aa9c14398062f2b7c066470accace78e412bc2", "https://bcr.bazel.build/modules/rules_java/7.6.1/MODULE.bazel": "2f14b7e8a1aa2f67ae92bc69d1ec0fa8d9f827c4e17ff5e5f02e91caa3b2d0fe", - "https://bcr.bazel.build/modules/rules_java/8.14.0/MODULE.bazel": "717717ed40cc69994596a45aec6ea78135ea434b8402fb91b009b9151dd65615", - "https://bcr.bazel.build/modules/rules_java/8.14.0/source.json": "8a88c4ca9e8759da53cddc88123880565c520503321e2566b4e33d0287a3d4bc", - "https://bcr.bazel.build/modules/rules_java/8.3.2/MODULE.bazel": "7336d5511ad5af0b8615fdc7477535a2e4e723a357b6713af439fe8cf0195017", - "https://bcr.bazel.build/modules/rules_java/8.5.1/MODULE.bazel": "d8a9e38cc5228881f7055a6079f6f7821a073df3744d441978e7a43e20226939", + "https://bcr.bazel.build/modules/rules_java/8.6.1/MODULE.bazel": "f4808e2ab5b0197f094cabce9f4b006a27766beb6a9975931da07099560ca9c2", + "https://bcr.bazel.build/modules/rules_java/8.6.1/source.json": "f18d9ad3c4c54945bf422ad584fa6c5ca5b3116ff55a5b1bc77e5c1210be5960", "https://bcr.bazel.build/modules/rules_jvm_external/4.4.2/MODULE.bazel": "a56b85e418c83eb1839819f0b515c431010160383306d13ec21959ac412d2fe7", "https://bcr.bazel.build/modules/rules_jvm_external/5.1/MODULE.bazel": "33f6f999e03183f7d088c9be518a63467dfd0be94a11d0055fe2d210f89aa909", "https://bcr.bazel.build/modules/rules_jvm_external/5.2/MODULE.bazel": "d9351ba35217ad0de03816ef3ed63f89d411349353077348a45348b096615036", @@ -121,6 +106,8 @@ "https://bcr.bazel.build/modules/rules_license/0.0.7/MODULE.bazel": "088fbeb0b6a419005b89cf93fe62d9517c0a2b8bb56af3244af65ecfe37e7d5d", "https://bcr.bazel.build/modules/rules_license/1.0.0/MODULE.bazel": "a7fda60eefdf3d8c827262ba499957e4df06f659330bbe6cdbdb975b768bb65c", "https://bcr.bazel.build/modules/rules_license/1.0.0/source.json": "a52c89e54cc311196e478f8382df91c15f7a2bfdf4c6cd0e2675cc2ff0b56efb", + "https://bcr.bazel.build/modules/rules_nixpkgs_core/0.13.0/MODULE.bazel": "b826d994220017d44c8a4e55435c2c2e6b4733eaaff69fff65232e0010afcb7b", + "https://bcr.bazel.build/modules/rules_nixpkgs_core/0.13.0/source.json": "c542b96a9d6ab189bd1a65da43e6c7b8be5f1099876ffba35cd9d2275f82740e", "https://bcr.bazel.build/modules/rules_pkg/0.7.0/MODULE.bazel": "df99f03fc7934a4737122518bb87e667e62d780b610910f0447665a7e2be62dc", "https://bcr.bazel.build/modules/rules_pkg/1.0.1/MODULE.bazel": "5b1df97dbc29623bccdf2b0dcd0f5cb08e2f2c9050aab1092fd39a41e82686ff", "https://bcr.bazel.build/modules/rules_pkg/1.0.1/source.json": "bd82e5d7b9ce2d31e380dd9f50c111d678c3bdaca190cb76b0e1c71b05e1ba8a", @@ -137,90 +124,43 @@ "https://bcr.bazel.build/modules/rules_python/0.4.0/MODULE.bazel": "9208ee05fd48bf09ac60ed269791cf17fb343db56c8226a720fbb1cdf467166c", "https://bcr.bazel.build/modules/rules_python/0.40.0/MODULE.bazel": "9d1a3cd88ed7d8e39583d9ffe56ae8a244f67783ae89b60caafc9f5cf318ada7", "https://bcr.bazel.build/modules/rules_python/0.40.0/source.json": "939d4bd2e3110f27bfb360292986bb79fd8dcefb874358ccd6cdaa7bda029320", - "https://bcr.bazel.build/modules/rules_rust/0.68.1/MODULE.bazel": "8d3332ef4079673385eb81f8bd68b012decc04ac00c9d5a01a40eff90301732c", - "https://bcr.bazel.build/modules/rules_rust/0.68.1/source.json": "3378e746f81b62457fdfd37391244fa8ff075ba85c05931ee4f3a20ac1efe963", "https://bcr.bazel.build/modules/rules_shell/0.2.0/MODULE.bazel": "fda8a652ab3c7d8fee214de05e7a9916d8b28082234e8d2c0094505c5268ed3c", - "https://bcr.bazel.build/modules/rules_shell/0.6.1/MODULE.bazel": "72e76b0eea4e81611ef5452aa82b3da34caca0c8b7b5c0c9584338aa93bae26b", - "https://bcr.bazel.build/modules/rules_shell/0.6.1/source.json": "20ec05cd5e592055e214b2da8ccb283c7f2a421ea0dc2acbf1aa792e11c03d0c", + "https://bcr.bazel.build/modules/rules_shell/0.2.0/source.json": "7f27af3c28037d9701487c4744b5448d26537cc66cdef0d8df7ae85411f8de95", "https://bcr.bazel.build/modules/stardoc/0.5.1/MODULE.bazel": "1a05d92974d0c122f5ccf09291442580317cdd859f07a8655f1db9a60374f9f8", "https://bcr.bazel.build/modules/stardoc/0.5.3/MODULE.bazel": "c7f6948dae6999bf0db32c1858ae345f112cacf98f174c7a8bb707e41b974f1c", "https://bcr.bazel.build/modules/stardoc/0.5.6/MODULE.bazel": "c43dabc564990eeab55e25ed61c07a1aadafe9ece96a4efabb3f8bf9063b71ef", "https://bcr.bazel.build/modules/stardoc/0.7.0/MODULE.bazel": "05e3d6d30c099b6770e97da986c53bd31844d7f13d41412480ea265ac9e8079c", "https://bcr.bazel.build/modules/stardoc/0.7.1/MODULE.bazel": "3548faea4ee5dda5580f9af150e79d0f6aea934fc60c1cc50f4efdd9420759e7", - "https://bcr.bazel.build/modules/stardoc/0.7.2/MODULE.bazel": "fc152419aa2ea0f51c29583fab1e8c99ddefd5b3778421845606ee628629e0e5", - "https://bcr.bazel.build/modules/stardoc/0.7.2/source.json": "58b029e5e901d6802967754adf0a9056747e8176f017cfe3607c0851f4d42216", + "https://bcr.bazel.build/modules/stardoc/0.7.1/source.json": "b6500ffcd7b48cd72c29bb67bcac781e12701cc0d6d55d266a652583cfcdab01", "https://bcr.bazel.build/modules/upb/0.0.0-20220923-a547704/MODULE.bazel": "7298990c00040a0e2f121f6c32544bab27d4452f80d9ce51349b1a28f3005c43", "https://bcr.bazel.build/modules/zlib/1.2.11/MODULE.bazel": "07b389abc85fdbca459b69e2ec656ae5622873af3f845e1c9d80fe179f3effa0", - "https://bcr.bazel.build/modules/zlib/1.3.1.bcr.5/MODULE.bazel": "eec517b5bbe5492629466e11dae908d043364302283de25581e3eb944326c4ca", - "https://bcr.bazel.build/modules/zlib/1.3.1.bcr.5/source.json": "22bc55c47af97246cfc093d0acf683a7869377de362b5d1c552c2c2e16b7a806", + "https://bcr.bazel.build/modules/zlib/1.3.1.bcr.3/MODULE.bazel": "af322bc08976524477c79d1e45e241b6efbeb918c497e8840b8ab116802dda79", + "https://bcr.bazel.build/modules/zlib/1.3.1.bcr.3/source.json": "2be409ac3c7601245958cd4fcdff4288be79ed23bd690b4b951f500d54ee6e7d", "https://bcr.bazel.build/modules/zlib/1.3.1/MODULE.bazel": "751c9940dcfe869f5f7274e1295422a34623555916eb98c174c1e945594bf198" }, "selectedYankedVersions": {}, "moduleExtensions": { - "@@rules_kotlin+//src/main/starlark/core/repositories:bzlmod_setup.bzl%rules_kotlin_extensions": { + "@@rules_java+//java:rules_java_deps.bzl%compatibility_proxy": { "general": { - "bzlTransitiveDigest": "rL/34P1aFDq2GqVC2zCFgQ8nTuOC6ziogocpvG50Qz8=", - "usagesDigest": "QI2z8ZUR+mqtbwsf2fLqYdJAkPOHdOV+tF2yVAUgRzw=", + "bzlTransitiveDigest": "84xJEZ1jnXXwo8BXMprvBm++rRt4jsTu9liBxz0ivps=", + "usagesDigest": "jTQDdLDxsS43zuRmg1faAjIEPWdLAbDAowI1pInQSoo=", "recordedFileInputs": {}, "recordedDirentsInputs": {}, "envVariables": {}, "generatedRepoSpecs": { - "com_github_jetbrains_kotlin_git": { - "repoRuleId": "@@rules_kotlin+//src/main/starlark/core/repositories:compiler.bzl%kotlin_compiler_git_repository", - "attributes": { - "urls": [ - "https://github.com/JetBrains/kotlin/releases/download/v1.9.23/kotlin-compiler-1.9.23.zip" - ], - "sha256": "93137d3aab9afa9b27cb06a824c2324195c6b6f6179d8a8653f440f5bd58be88" - } - }, - "com_github_jetbrains_kotlin": { - "repoRuleId": "@@rules_kotlin+//src/main/starlark/core/repositories:compiler.bzl%kotlin_capabilities_repository", - "attributes": { - "git_repository_name": "com_github_jetbrains_kotlin_git", - "compiler_version": "1.9.23" - } - }, - "com_github_google_ksp": { - "repoRuleId": "@@rules_kotlin+//src/main/starlark/core/repositories:ksp.bzl%ksp_compiler_plugin_repository", - "attributes": { - "urls": [ - "https://github.com/google/ksp/releases/download/1.9.23-1.0.20/artifacts.zip" - ], - "sha256": "ee0618755913ef7fd6511288a232e8fad24838b9af6ea73972a76e81053c8c2d", - "strip_version": "1.9.23-1.0.20" - } - }, - "com_github_pinterest_ktlint": { - "repoRuleId": "@@bazel_tools//tools/build_defs/repo:http.bzl%http_file", - "attributes": { - "sha256": "01b2e0ef893383a50dbeb13970fe7fa3be36ca3e83259e01649945b09d736985", - "urls": [ - "https://github.com/pinterest/ktlint/releases/download/1.3.0/ktlint" - ], - "executable": true - } - }, - "rules_android": { - "repoRuleId": "@@bazel_tools//tools/build_defs/repo:http.bzl%http_archive", - "attributes": { - "sha256": "cd06d15dd8bb59926e4d65f9003bfc20f9da4b2519985c27e190cddc8b7a7806", - "strip_prefix": "rules_android-0.1.1", - "urls": [ - "https://github.com/bazelbuild/rules_android/archive/v0.1.1.zip" - ] - } + "compatibility_proxy": { + "repoRuleId": "@@rules_java+//java:rules_java_deps.bzl%_compatibility_proxy_repo_rule", + "attributes": {} } }, "recordedRepoMappingEntries": [ [ - "rules_kotlin+", + "rules_java+", "bazel_tools", "bazel_tools" ] ] } } - }, - "facts": {} + } } diff --git a/README.md b/README.md index d2141e2..d5e9195 100644 --- a/README.md +++ b/README.md @@ -1,511 +1,266 @@ # rules_rocq_rust -Bazel rules for Rocq theorem proving and coq-of-rust integration, following the exact patterns established by [rules_rust](https://github.com/bazelbuild/rules_rust) and [rules_wasm_component](https://github.com/pulseengine/rules_wasm_component). +Bazel rules for Rocq/Coq theorem proving with hermetic toolchain support via [Nix](https://nixos.org/). -## Features +## Prerequisites: Installing Nix -- **Rocq Platform Integration**: Complete Coq Platform support with binary installers -- **coq-of-rust Support**: Translate Rust code to Coq for formal verification -- **Bazel 8 bzlmod**: Modern Bazel module system support -- **Hermetic Toolchains**: Download and verify complete Coq Platform installers -- **Enterprise Ready**: Support for air-gap environments and corporate mirrors -- **Cross-Platform**: macOS (arm64), Windows (x86_64), Linux support +**Nix is required** for the Rocq toolchain. The toolchain uses [nixpkgs](https://github.com/NixOS/nixpkgs) to provide hermetic Coq installations across all platforms. -## coq-of-rust Toolchain Status +### macOS -The coq-of-rust toolchain is currently in development with placeholder functionality: +```bash +# Install Nix (multi-user installation, recommended) +sh <(curl -L https://nixos.org/nix/install) -### Current Implementation -- **Placeholder System**: Temporary implementation that simulates coq-of-rust behavior -- **Future Integration**: Will build coq-of-rust from source using rules_rust toolchain -- **Repository Support**: Will clone and build from official coq-of-rust repository when available +# Restart your terminal, or source the nix profile: +. /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh -### Current Placeholder Implementation -- **Basic Tool Simulation**: Placeholder provides basic coq-of-rust command interface -- **Minimal Standard Library**: Includes essential Prelude.v and Types.v definitions -- **Simple Output**: Generates basic Coq code templates for development and testing +# Verify installation +nix --version +``` -### Robust Translation Rules -- **Proper Error Handling**: Validates inputs and provides meaningful error messages -- **Dependency Management**: Handles both Rust and Coq dependencies correctly -- **File Type Validation**: Only processes .rs files, warns about others -- **Progress Reporting**: Shows translation progress for each file +### Linux -### Standard Library Structure -``` -lib/coq_of_rust/ -├── Prelude.v # Basic definitions and type classes -├── Types.v # Rust primitive types in Coq -└── ... # Additional standard library files +```bash +# Install Nix (multi-user installation) +sh <(curl -L https://nixos.org/nix/install) --daemon + +# Restart your terminal or start a new shell +# Verify installation +nix --version ``` -### Usage Patterns +### Windows (via WSL2) -**Basic Translation:** -```bazel -coq_of_rust_library( - name = "rust_code", - rust_sources = ["my_code.rs"], - edition = "2021", -) -``` +```bash +# In WSL2 Ubuntu/Debian: +sh <(curl -L https://nixos.org/nix/install) --no-daemon -**With Dependencies:** -```bazel -coq_of_rust_library( - name = "rust_with_deps", - rust_sources = ["main.rs"], - rust_deps = [":other_rust_code"], - include_path = "src", -) +# Verify installation +nix --version ``` -**With rules_rust Integration:** -```bazel -# First ensure rules_rust is set up -rust = use_repo(rule = @bazel_tools//tools/build_defs/repo:http.bzl, sha256 = "...") -register_toolchains("@rust_toolchains//:all") - -# Then coq-of-rust can build from source -coq_of_rust_library( - name = "rust_code", - rust_sources = ["my_code.rs"], - edition = "2021", -) +### Verify Coq is Available + +```bash +# Test that Coq can be fetched from nixpkgs +nix-shell -p coq --run "coqc --version" ``` +## Features + +- **Hermetic Toolchains**: Coq toolchain provided via nixpkgs for reproducible builds +- **Cross-Platform**: Linux (x86_64, aarch64), macOS (x86_64, aarch64) +- **Multiple Coq Versions**: 8.20, 8.19, 8.18, 8.17, 8.16 +- **Bazel 8 bzlmod**: Modern module system support +- **Rocq Platform Integration**: Provides equivalent tools to Rocq Platform +- **coq-of-rust Support**: Planned integration for Rust-to-Coq translation +- **Reproducible**: Pinned nixpkgs commit for deterministic builds + ## Quick Start ### 1. Add to your MODULE.bazel -```bazel +```starlark bazel_dep(name = "rules_rocq_rust", version = "0.1.0") -# Enable Rocq toolchain +# Override to fetch from GitHub (not yet in BCR) +git_override( + module_name = "rules_rocq_rust", + remote = "https://github.com/pulseengine/rules_rocq_rust.git", + commit = "", +) + +# Configure Rocq toolchain rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq") rocq.toolchain( - version = "2025.01.0", - strategy = "download", + version = "8.20", # Coq version + strategy = "nix", # Hermetic nix-based installation ) use_repo(rocq, "rocq_toolchains") -# Enable coq-of-rust toolchain (builds from source) -coq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "coq_of_rust") -coq_of_rust.toolchain( - version = "0.5.0", - strategy = "build", # coq-of-rust must be built from source -) -use_repo(coq_of_rust, "coq_of_rust_toolchains") - -# Optional: Enable OCaml toolchain for QuickChick support -ocaml = use_extension("@rules_rocq_rust//toolchains:ocaml_extensions.bzl", "ocaml") -ocaml.toolchain( - version = "5.1.1", - strategy = "download", -) -use_repo(ocaml, "ocaml_toolchains") +register_toolchains("@rocq_toolchains//:all") +``` -register_toolchains( - "@rocq_toolchains//:rocq_toolchain", - "@coq_of_rust_toolchains//:coq_of_rust_toolchain", -) +### 2. Create proof files + +```coq +(* proofs/example.v *) +Theorem plus_comm : forall n m : nat, n + m = m + n. +Proof. + intros n m. + induction n as [| n' IHn']. + - simpl. rewrite Nat.add_0_r. reflexivity. + - simpl. rewrite IHn'. rewrite Nat.add_succ_r. reflexivity. +Qed. ``` -### 2. Use in your BUILD files +### 3. Add BUILD.bazel -```bazel +```starlark load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test") rocq_library( - name = "my_theorems", - srcs = ["theorems.v"], + name = "example_proofs", + srcs = ["example.v"], ) rocq_proof_test( - name = "my_theorems_test", - srcs = ["theorems.v"], - deps = [":my_theorems"], + name = "example_test", + srcs = ["example.v"], + deps = [":example_proofs"], ) ``` -## Advanced Proof Validation - -The rules now include comprehensive proof validation capabilities: - -### Proof Validation Rules +### 4. Build and test -**Basic Validation:** -```bazel -rocq_proof_validation( - name = "proof_validation", - srcs = ["my_proofs.v"], - validation_level = "comprehensive", - coverage_analysis = True, -) -``` +```bash +# Build proofs +bazel build //proofs:example_proofs -**Proof Automation:** -```bazel -rocq_proof_automation( - name = "proof_automation", - srcs = ["my_proofs.v"], - automation_script = "automation.v", -) +# Run proof tests +bazel test //proofs:example_test ``` -**coq-of-rust Validation:** -```bazel -rocq_coq_of_rust_validation( - name = "coq_of_rust_validation", - srcs = [":rust_code_translated"], -) -``` +## How It Works -### Validation Features +### First Build (one-time setup) -- **Comprehensive Validation**: Checks proof completeness, coverage, and obligations -- **Proof Automation**: Applies Ltac scripts for automated proof completion -- **Coverage Analysis**: Measures proof coverage across all theorems -- **Integration Validation**: Validates coq-of-rust generated proofs -- **Detailed Reporting**: Generates validation reports and obligation summaries +On the first build, Bazel will: -## Examples +1. Fetch the pinned nixpkgs repository (~200MB download) +2. Use nix to fetch/build Coq from nixpkgs cache (~100MB) +3. Cache everything in `~/.cache/bazel/` -See the [examples/](examples/) directory for complete working examples: +This takes **5-10 minutes** depending on your internet connection. -- `examples/rocq_pure/`: Pure Rocq proof compilation -- `examples/rust_verified/`: Rust code verified with coq-of-rust (fully implemented) -- `examples/advanced_validation/`: Advanced proof validation and automation -- `examples/rust_integration/`: Complete Rust integration with rules_rust +### Subsequent Builds -The examples demonstrate: +After initial setup: +- Toolchain is cached locally +- No nix invocation needed +- Builds are fast and hermetic -**Rust Verification Example:** -- Rust to Coq translation using coq-of-rust -- Proof verification of generated Coq code -- Manual verification proofs about Rust code behavior -- Complete build configuration with proper dependencies +## Supported Platforms -**Advanced Validation Example:** -- Comprehensive proof validation workflows -- Proof automation using Ltac scripts -- Coverage analysis and reporting -- Integration with coq-of-rust generated proofs +| Platform | Architecture | Status | +|----------|-------------|--------| +| Linux | x86_64 | ✅ Supported | +| Linux | aarch64 | ✅ Supported | +| macOS | x86_64 (Intel) | ✅ Supported | +| macOS | aarch64 (Apple Silicon) | ✅ Supported | +| Windows | x86_64 | ⚠️ Via WSL2 only | -**Rust Integration Example:** -- Integration with rules_rust toolchain -- Complete verification workflow from Rust to Coq -- Proof automation for verification proofs -- Advanced validation of generated proofs +## Coq Versions -## Toolchain Management - -The repository uses a centralized JSON-based toolchain management system similar to rules_wasm_component: - -- `checksums/tools/rocq.json`: Tool versions and checksums -- `toolchains/tool_registry.bzl`: Unified download and verification logic -- Enterprise support via environment variables: - - `BAZEL_ROCQ_OFFLINE=1`: Use vendored tools - - `BAZEL_ROCQ_VENDOR_DIR`: Custom vendor directory - - `BAZEL_ROCQ_MIRROR`: Corporate mirror URL +Available Coq versions via nixpkgs: -### Toolchain File Structure +| Version | nixpkgs attribute | Status | +|---------|-------------------|--------| +| 8.20 | `coq_8_20` | ✅ Default | +| 8.19 | `coq_8_19` | ✅ Supported | +| 8.18 | `coq_8_18` | ✅ Supported | +| 8.17 | `coq_8_17` | ✅ Supported | +| 8.16 | `coq_8_16` | ✅ Supported | +| latest | `coq` | ✅ Supported | -The Rocq toolchain organizes files following the exact patterns established by rules_rust: - -``` -@rocq_toolchains// -├── bin/ # Executables (public visibility) -│ ├── coqc # Coq compiler (main executable) -│ ├── coqtop # Coq toplevel (interactive REPL) -│ ├── coqide # Coq IDE (graphical interface) -│ ├── coqdoc # Documentation generator -│ └── coq* # All Coq tools (coqtools filegroup) -├── lib/ # Libraries and standard files -│ └── coq/ # Complete Coq standard library -│ ├── theories/ # Standard theories (.vo files) -│ ├── plugins/ # Coq plugins (.cmxs, .so, .dylib) -│ ├── user-contrib/ # User contributions -│ └── ... # Other library files -└── BUILD.bazel # Build file with filegroups -``` +To use a specific version: -### Filegroup Organization - -The toolchain provides comprehensive filegroups following rules_rust patterns: - -| Filegroup | Contents | Visibility | -|-----------|----------|------------| -| `coqc` | Main Coq compiler | Public | -| `coqtop` | Coq toplevel | Public | -| `coqide` | Coq IDE | Public | -| `coqdoc` | Documentation generator | Public | -| `coqtools` | All Coq tools (`coq*`) | Public | -| `stdlib` | Standard library (.vo, .cmxs) | Public | -| `coq_libraries` | Complete library collection | Public | -| `coq_theories` | Coq theories (.v, .glob) | Public | -| `coq_plugins` | Coq plugins (.cmxs, .so, .dylib) | Public | - -### Binary Discovery Process - -The toolchain uses a robust binary discovery system: - -1. **Primary Locations**: Looks in standard directories first -2. **Fallback Search**: Recursive search if primary fails -3. **Platform-Specific**: Handles macOS, Windows, Linux structures -4. **Comprehensive Logging**: Clear output during extraction - -**Discovery Patterns:** -- `bin/` - Standard binary directory -- `Coq Platform.app/Contents/Resources/bin/` - macOS app bundle -- `Coq-Platform-release-*/bin/` - Version-specific directories -- Recursive search for any `coq*` or `rocq*` files - -### Library Discovery Process - -Library discovery follows the same robust approach: - -1. **Multiple Patterns**: Supports various library structures -2. **Recursive Copying**: Preserves directory hierarchy -3. **Comprehensive Coverage**: Finds all library types -4. **Warning System**: Alerts if libraries missing - -**Library Patterns:** -- `lib/` - Standard library directory -- `Coq Platform.app/Contents/Resources/lib/` - macOS app bundle -- `share/coq/` - Alternative library location -- `Coq-Platform-release-*/lib/` - Version-specific libraries - -## Development - -### Using the Toolchain in Your Project - -Once the toolchain is set up, you can use the filegroups in your BUILD files: - -```bazel -# Load the Rocq toolchain -load("@rocq_toolchains//:BUILD.bazel", "coqc", "stdlib") - -# Use Coq compiler in your rules -rocq_library( - name = "my_library", - srcs = ["my_proof.v"], - deps = [":stdlib"], - toolchain = "@rocq_toolchains//:rocq_toolchain", -) - -# Access specific tools -filegroup( - name = "my_tools", - srcs = [ - "@rocq_toolchains//:coqc", - "@rocq_toolchains//:coqtop", - "@rocq_toolchains//:coqide", - ], -) - -# Use standard library files -filegroup( - name = "my_libs", - srcs = ["@rocq_toolchains//:stdlib"], -) -``` - -### Toolchain File Access Patterns - -**Direct Binary Access:** -```bazel -# Access the main compiler -alias( - name = "coqc", - actual = "@rocq_toolchains//:coqc", -) - -# Use in your rules -ctx.actions.run( - executable = "@rocq_toolchains//:coqc", - arguments = ["-compile", src.path], -) -``` - -**Library File Access:** -```bazel -# Access standard library files -alias( - name = "coq_stdlib", - actual = "@rocq_toolchains//:stdlib", -) - -# Use in your compilation -ctx.actions.run( - inputs = ["@rocq_toolchains//:stdlib"], - outputs = [output_file], +```starlark +rocq.toolchain( + version = "8.19", # Use Coq 8.19 + strategy = "nix", ) ``` -### Testing +## Examples -The repository now includes comprehensive testing infrastructure: +See the `proofs/` directory for example usage: ```bash -# Run basic structure tests -bazel run //:test_basic - -# Run toolchain functionality tests -bazel run //test:toolchain_test - -# Run coq-of-rust tests -bazel run //test:coq_of_rust_test - -# Run file mapping tests -bazel run //test:file_mapping_test +# Build example proofs +bazel build //proofs:all -# Run integration tests -bazel run //test:integration_test - -# Run all tests -bazel run //test:test_all - -# Test the pure Rocq example -bazel test //examples/rocq_pure:test - -# Test the Rust verification example -bazel test //examples/rust_verified:test - -# Test manual verification proofs -bazel test //examples/rust_verified:test_verification +# Test proofs compile +bazel test //proofs:... ``` -### Test Categories - -- **Basic Tests**: Verify file loading and rule instantiation -- **Toolchain Tests**: Verify toolchain components can be loaded -- **File Mapping Tests**: Verify proper file organization -- **Integration Tests**: Verify complete toolchain setup -- **Functionality Tests**: Verify actual toolchain functionality - -### Adding New Tests - -1. Add test functions to appropriate test modules -2. Add test targets to `test/BUILD.bazel` -3. Include the test in the `test_all` target +## Toolchain Management -### Adding New Tools +The toolchain is managed via nixpkgs, providing hermetic Coq installations: -1. Add tool information to `checksums/tools/.json` -2. Add URL pattern to `toolchains/tool_registry.bzl` -3. Create repository rule in `toolchains/_toolchain.bzl` -4. Add module extension to expose the toolchain +- **Pinned nixpkgs**: Reproducible builds with fixed commit +- **Multiple versions**: Switch Coq versions via `version` attribute +- **Cross-platform**: Same configuration works on Linux and macOS -### Rocq Platform Details +### Rocq Platform Integration -The rules_rocq_rust implementation uses the official [Coq Platform](https://github.com/rocq-prover/platform) binary installers: +While we use nixpkgs instead of Rocq Platform binaries, the toolchain provides equivalent functionality: +- Coq compiler and tools +- Standard library +- Documentation generator -- **Complete packages**: Each installer contains Coq compiler, standard library, and tools -- **Multiple versions**: Supports Coq 8.20 (recommended), 8.19, 8.18, etc. -- **Cross-platform**: macOS (arm64), Windows (x86_64), Linux -- **No OCaml required**: The binaries are self-contained +### coq-of-rust Support -### Enterprise Deployment +coq-of-rust integration is planned for future releases. The `rocq_library` rule can compile Coq files generated by coq-of-rust. -For air-gap environments, set these environment variables: +## Toolchain Contents -```bash -# Use vendored tools from third_party/toolchains/ -export BAZEL_ROCQ_OFFLINE=1 +The nix toolchain provides: -# Or use a custom vendor directory -export BAZEL_ROCQ_VENDOR_DIR=/path/to/vendor +| Tool | Description | +|------|-------------| +| `coqc` | Coq compiler | +| `coqtop` | Interactive toplevel | +| `coqdoc` | Documentation generator | +| `coqchk` | Proof checker | +| Standard Library | `lib/coq/theories/` | -# Or use a corporate mirror -export BAZEL_ROCQ_MIRROR=https://mirror.company.com +## Troubleshooting -### QuickChick Support +### "nix: command not found" -QuickChick is a randomized property-based testing framework for Coq that requires OCaml. Since the binary Coq Platform installers don't include OCaml, you need to enable OCaml support separately. +Nix is not installed or not in PATH. See [Installing Nix](#prerequisites-installing-nix). -#### Enabling OCaml for QuickChick +### "error: cannot connect to daemon" -Add this to your MODULE.bazel: +The nix daemon isn't running: -```bazel -# Optional OCaml toolchain for QuickChick support -ocaml = use_extension("@rules_rocq_rust//toolchains:ocaml_extensions.bzl", "ocaml") -ocaml.toolchain( - version = "5.1.1", - strategy = "download", # only hermetic downloads supported -) -use_repo(ocaml, "ocaml_toolchains") +```bash +# macOS/Linux with systemd +sudo systemctl start nix-daemon -register_toolchains("@ocaml_toolchains//:ocaml_toolchain") +# macOS without systemd +sudo launchctl start org.nixos.nix-daemon ``` -#### OCaml Strategy - -- **download**: Downloads prebuilt OCaml binaries (only strategy supported for hermeticity) +### Slow first build -### Enterprise Deployment +The first build downloads nixpkgs and Coq. This is normal and only happens once. Subsequent builds use the cached toolchain. -For air-gap environments, set these environment variables: +### "hash mismatch" errors -```bash -# Use vendored tools from third_party/toolchains/ -export BAZEL_ROCQ_OFFLINE=1 - -# Or use a custom vendor directory -export BAZEL_ROCQ_VENDOR_DIR=/path/to/vendor - -# Or use a corporate mirror -export BAZEL_ROCQ_MIRROR=https://mirror.company.com +The nixpkgs commit hash may have changed. Update the hash in MODULE.bazel or wait for a rules_rocq_rust update. -# For OCaml (if using QuickChick) -export BAZEL_OCAML_OFFLINE=1 -export BAZEL_OCAML_VENDOR_DIR=/path/to/vendor -export BAZEL_OCAML_MIRROR=https://mirror.company.com -``` - -#### Vendor Workflow +## Development -To set up vendored toolchains for air-gap environments: +### Running Tests ```bash -# 1. Run the vendor script to download all toolchains -./scripts/vendor_toolchains.sh +# Verify rules load correctly +bazel query //rocq/... -# 2. This creates third_party/toolchains/ with all required binaries -# 3. Set offline mode to use vendored tools -export BAZEL_ROCQ_OFFLINE=1 - -# 4. Build as normal - no internet access required -bazel build //examples/rocq_pure:test +# Build all targets +bazel build //... ``` -#### Corporate Mirror Setup - -For enterprise mirrors, the mirror should follow this structure: +### Updating nixpkgs -``` -https://mirror.company.com/ -├── rocq/ -│ ├── 2025.01.0/ -│ │ ├── darwin_arm64/ -│ │ │ └── Coq-Platform-release-2025.01.0-version.8.20.2025.01-MacOS-arm64.dmg -│ │ ├── linux_amd64/ -│ │ │ └── Coq-Platform-release-2025.01.0-version.8.20.2025.01-Linux-x86_64.tar.gz -│ │ └── ... -│ └── ... -└── ocaml/ - ├── 5.1.1/ - │ ├── darwin_arm64/ - │ │ └── ocaml-5.1.1-aarch64-macos.tar.gz - │ └── ... - └── ... -``` +To update the pinned nixpkgs version: -Set the mirror URL: -```bash -export BAZEL_ROCQ_MIRROR=https://mirror.company.com -``` +1. Find a recent commit from [NixOS/nixpkgs](https://github.com/NixOS/nixpkgs) +2. Compute SHA256: `nix-prefetch-url --unpack https://github.com/NixOS/nixpkgs/archive/.tar.gz` +3. Update MODULE.bazel with new commit and sha256 ## License @@ -513,7 +268,6 @@ Apache License 2.0 - See [LICENSE](LICENSE) file ## Related Projects -- [rules_rust](https://github.com/bazelbuild/rules_rust) - Rust rules that inspired this structure -- [rules_wasm_component](https://github.com/pulseengine/rules_wasm_component) - WebAssembly rules with similar toolchain patterns -- [Rocq Prover](https://github.com/rocq-prover/platform) - The Rocq theorem prover -- [coq-of-rust](https://github.com/coq-of-rust/coq-of-rust) - Rust to Coq translation tool \ No newline at end of file +- [nixpkgs](https://github.com/NixOS/nixpkgs) - Nix packages collection +- [rules_nixpkgs](https://github.com/tweag/rules_nixpkgs) - Nix integration for Bazel +- [Rocq Prover](https://rocq-prover.org/) - The Rocq/Coq theorem prover diff --git a/rocq/BUILD.bazel b/rocq/BUILD.bazel index 35e4d40..db13a7c 100644 --- a/rocq/BUILD.bazel +++ b/rocq/BUILD.bazel @@ -6,3 +6,8 @@ package(default_visibility = ["//visibility:public"]) exports_files( srcs = glob(["*.bzl"]), ) + +# Toolchain type for Rocq/Coq +toolchain_type( + name = "toolchain_type", +) diff --git a/rocq/extensions.bzl b/rocq/extensions.bzl index 63d8304..32e3a81 100644 --- a/rocq/extensions.bzl +++ b/rocq/extensions.bzl @@ -1,78 +1,60 @@ """Module extensions for using rules_rocq with bzlmod. -Following the exact pattern established by rules_rust extensions. +Provides Rocq/Coq toolchain setup using nixpkgs for hermetic builds. """ -load("//toolchains:rocq_toolchain.bzl", "rocq_toolchain_repository") +load("//toolchains:rocq_nix_toolchain.bzl", "rocq_nix_toolchain_repository") # Tag classes for Rocq toolchain configuration _RocqToolchainTag = tag_class( doc = "Tags for defining Rocq toolchains", attrs = { "version": attr.string( - doc = "Rocq version to use", - default = "2025.01.0", + doc = "Coq version to use (e.g., '8.20', '8.19')", + default = "8.20", ), "strategy": attr.string( - doc = "Tool acquisition strategy", - default = "download", - values = ["download"], + doc = "Tool acquisition strategy: 'nix' for hermetic nixpkgs", + default = "nix", + values = ["nix"], ), - "editions": attr.string_list( - doc = "Supported Coq/Rocq editions", - default = ["2021"], - ), - } + }, ) # Rocq module extension implementation def _rocq_impl(module_ctx): """Implementation of Rocq toolchain extension. - This follows the exact pattern from rules_rust. + Uses nixpkgs to provide hermetic Coq installation. """ # Collect toolchain configurations from all modules toolchains = [] for mod in module_ctx.modules: for toolchain in mod.tags.toolchain: toolchains.append(toolchain) - - # Use the first toolchain configuration (following rules_rust pattern) + + # Use the first toolchain configuration if toolchains: config = toolchains[0] - - # Create toolchain repository using our repository rule - rocq_toolchain_repository( - name = "rocq_toolchains", - version = config.version, - strategy = config.strategy, - ) + coq_version = config.version else: # Default configuration - rocq_toolchain_repository( - name = "rocq_toolchains", - version = "2025.01.0", - strategy = "download", - ) - - # Return extension metadata (reproducible for caching) - return module_ctx.extension_metadata(reproducible = True) + coq_version = "8.20" -# Empty repository helper (from rules_rust) for fallback -def _empty_repository_impl(repository_ctx): - repository_ctx.file("WORKSPACE.bazel", 'workspace(name = "{}")'.format(repository_ctx.name)) - repository_ctx.file("BUILD.bazel", "") + # Create nix-based toolchain repository + rocq_nix_toolchain_repository( + name = "rocq_toolchains", + coq_version = coq_version, + ) -_empty_repository = repository_rule( - doc = "Declare an empty repository.", - implementation = _empty_repository_impl, -) + # Return extension metadata (reproducible for caching) + return module_ctx.extension_metadata(reproducible = True) # Rocq module extension rocq = module_extension( - doc = "Rocq toolchain extension.", + doc = "Rocq/Coq toolchain extension using nixpkgs.", implementation = _rocq_impl, tag_classes = { "toolchain": _RocqToolchainTag, }, -) \ No newline at end of file +) diff --git a/toolchains/rocq_nix_toolchain.bzl b/toolchains/rocq_nix_toolchain.bzl new file mode 100644 index 0000000..8852b1c --- /dev/null +++ b/toolchains/rocq_nix_toolchain.bzl @@ -0,0 +1,119 @@ +"""Nix-based Rocq/Coq toolchain for hermetic builds. + +This module uses rules_nixpkgs to provide a hermetic Coq installation +from nixpkgs. Works on Linux and macOS. +""" + +load("@rules_nixpkgs_core//:nixpkgs.bzl", "nixpkgs_package") + +def rocq_nix_toolchain_repository(name, coq_version = "8.20"): + """Create a Rocq toolchain using nixpkgs. + + This provides a hermetic Coq installation from nixpkgs that works + on Linux (x86_64, aarch64) and macOS (x86_64, aarch64). + + Args: + name: Repository name for the toolchain + coq_version: Coq version to use (e.g., "8.20", "8.19", "8.18") + """ + # Map version to nixpkgs attribute + coq_attr = _get_coq_attr(coq_version) + + # Import Coq from nixpkgs + nixpkgs_package( + name = name, + repository = "@nixpkgs", + attribute_path = coq_attr, + build_file_content = _COQ_BUILD_FILE, + ) + +def _get_coq_attr(version): + """Map Coq version to nixpkgs attribute path. + + Args: + version: Coq version string (e.g., "8.20") + + Returns: + nixpkgs attribute path for the Coq package + """ + # nixpkgs has versioned Coq packages + version_map = { + "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", + } + + attr = version_map.get(version, "coq") + return attr + +# BUILD file content for the nixpkgs_package +_COQ_BUILD_FILE = ''' +package(default_visibility = ["//visibility:public"]) + +# Coq compiler +filegroup( + name = "coqc", + srcs = glob(["bin/coqc"]), +) + +# Coq top-level +filegroup( + name = "coqtop", + srcs = glob(["bin/coqtop"]), +) + +# Coq documentation generator +filegroup( + name = "coqdoc", + srcs = glob(["bin/coqdoc"]), +) + +# Coq checker +filegroup( + name = "coqchk", + srcs = glob(["bin/coqchk"]), +) + +# All Coq binaries +filegroup( + name = "coq_tools", + srcs = glob(["bin/coq*"]), +) + +# Coq standard library (compiled .vo files) +filegroup( + name = "stdlib", + srcs = glob([ + "lib/coq/**/*.vo", + "lib/coq/**/*.glob", + ]), +) + +# Coq theories source files +filegroup( + name = "coq_theories", + srcs = glob(["lib/coq/**/*.v"]), +) + +# All Coq libraries +filegroup( + name = "coq_libraries", + srcs = glob(["lib/coq/**/*"]), +) + +# Toolchain target +toolchain( + name = "rocq_toolchain", + toolchain = ":coq_tools", + toolchain_type = "@rules_rocq_rust//rocq:toolchain_type", +) + +# Alias for register_toolchains +alias( + name = "all", + actual = ":rocq_toolchain", +) +''' diff --git a/toolchains/rocq_toolchain.bzl b/toolchains/rocq_toolchain.bzl index 3279f99..b46d43e 100644 --- a/toolchains/rocq_toolchain.bzl +++ b/toolchains/rocq_toolchain.bzl @@ -1,288 +1,301 @@ -"""Rocq toolchain definitions with enhanced tool management +"""Rocq toolchain definitions for hermetic Coq/Rocq builds. -Following the exact pattern established by rules_wasm_component. +This module provides repository rules for downloading and setting up +the Rocq (Coq) toolchain for use with Bazel. """ -load("//checksums:registry.bzl", "get_tool_info", "get_tool_checksum") -load("//:toolchains/tool_registry.bzl", "detect_platform", "download_and_verify") -load("@bazel_skylib//lib:native.bzl", "native") +load("//toolchains:tool_registry.bzl", "detect_platform", "download_and_verify") + +# ============================================================================= +# Rocq Toolchain Repository Implementation +# ============================================================================= -# Rocq Toolchain Implementation def _rocq_toolchain_repository_impl(repository_ctx): """Create Rocq toolchain repository. - - This is the main implementation following rules_rust patterns. - Always uses hermetic downloads for reproducibility. + + Downloads the Rocq Platform and extracts binaries for use in builds. """ - - strategy = repository_ctx.attr.strategy - platform = detect_platform(repository_ctx) version = repository_ctx.attr.version - - print("Setting up Rocq toolchain {} for platform {} using strategy {}".format( - version, platform, strategy - )) - - # Only support download strategy for hermeticity - if strategy == "download": - _setup_downloaded_rocq_tools(repository_ctx) - else: - fail("Unknown strategy: {}. Must be 'download' (only hermetic downloads supported)".format(strategy)) - - # Create BUILD files - _create_build_files(repository_ctx) - -def _setup_downloaded_rocq_tools(repository_ctx): - """Download prebuilt Rocq tools.""" - platform = detect_platform(repository_ctx) - version = repository_ctx.attr.version - - # Download Rocq toolchain - rocq_tool_path = download_and_verify( - repository_ctx, "rocq", version, platform - ) - - # Extract the toolchain with enhanced error handling - if rocq_tool_path.endswith(".tar.gz") or rocq_tool_path.endswith(".tar.xz"): - print("Extracting Rocq toolchain from: {}".format(rocq_tool_path)) - repository_ctx.execute([ - "tar", "-xzf", rocq_tool_path, "-C", repository_ctx.expand_location("{{name}}") + + print("Setting up Rocq toolchain {} for platform {}".format(version, platform)) + + # Check if platform is supported + supported = ["darwin_arm64", "windows_amd64"] + if platform not in supported: + # Create stub repository for unsupported platforms + print("WARNING: Rocq Platform binaries not available for {}".format(platform)) + print("Supported platforms: {}".format(", ".join(supported))) + print("Creating stub toolchain - proofs will not compile") + _create_stub_repository(repository_ctx) + return + + # Download the toolchain + tool_path = download_and_verify(repository_ctx, "rocq", version, platform) + print("Downloaded toolchain to: {}".format(tool_path)) + + # Extract based on format + if tool_path.endswith(".dmg"): + _extract_dmg(repository_ctx, tool_path) + elif tool_path.endswith(".tar.gz"): + _extract_tar_gz(repository_ctx, tool_path) + elif tool_path.endswith(".exe"): + _extract_windows_exe(repository_ctx, tool_path) + else: + fail("Unsupported archive format: {}".format(tool_path)) + + # Create BUILD file + _create_build_file(repository_ctx) + +def _create_stub_repository(repository_ctx): + """Create a stub repository for unsupported platforms.""" + repository_ctx.file("BUILD.bazel", """ +# Stub Rocq toolchain for unsupported platform +# Proofs will not compile - use a supported platform or install Coq manually + +filegroup( + name = "coqc", + srcs = [], + visibility = ["//visibility:public"], +) + +filegroup( + name = "coq_tools", + srcs = [], + visibility = ["//visibility:public"], +) + +filegroup( + name = "stdlib", + srcs = [], + visibility = ["//visibility:public"], +) +""") + repository_ctx.file("WORKSPACE.bazel", 'workspace(name = "{}")'.format(repository_ctx.name)) + +def _extract_dmg(repository_ctx, dmg_path): + """Extract Coq tools from macOS DMG.""" + print("Extracting macOS DMG: {}".format(dmg_path)) + + # Create directories + repository_ctx.execute(["mkdir", "-p", "bin", "lib"]) + + # Mount DMG + mount_point = "dmg_mount" + repository_ctx.execute(["mkdir", "-p", mount_point]) + + mount_result = repository_ctx.execute([ + "hdiutil", "attach", "-mountpoint", mount_point, "-nobrowse", dmg_path, + ]) + + if mount_result.return_code != 0: + fail("Failed to mount DMG: {}".format(mount_result.stderr)) + + # Find and copy binaries + # Coq Platform structure: "Coq-Platform*.app/Contents/Resources/bin/" + find_result = repository_ctx.execute([ + "find", mount_point, "-type", "f", "-name", "coqc", + ]) + + if find_result.return_code == 0 and find_result.stdout.strip(): + coqc_path = find_result.stdout.strip().split("\n")[0] + bin_dir = coqc_path.rsplit("/", 1)[0] + + # Copy all binaries + for binary in ["coqc", "coqtop", "coqdoc", "coqchk", "coq_makefile"]: + src = "{}/{}".format(bin_dir, binary) + dst = "bin/{}".format(binary) + cp_result = repository_ctx.execute(["cp", src, dst]) + if cp_result.return_code == 0: + repository_ctx.execute(["chmod", "+x", dst]) + print("Copied: {}".format(binary)) + + # Copy libraries (find lib/coq or similar) + lib_result = repository_ctx.execute([ + "find", mount_point, "-type", "d", "-name", "coq", "-path", "*/lib/*", + ]) + if lib_result.return_code == 0 and lib_result.stdout.strip(): + lib_path = lib_result.stdout.strip().split("\n")[0] + repository_ctx.execute(["cp", "-r", lib_path, "lib/"]) + print("Copied Coq libraries") + else: + print("WARNING: Could not find coqc in DMG") + + # Unmount DMG + repository_ctx.execute(["hdiutil", "detach", mount_point, "-force"]) + repository_ctx.execute(["rm", "-rf", mount_point]) + +def _extract_tar_gz(repository_ctx, tar_path): + """Extract Coq tools from tar.gz archive.""" + print("Extracting tar.gz: {}".format(tar_path)) + + # Create directories + repository_ctx.execute(["mkdir", "-p", "bin", "lib", "extracted"]) + + # Extract archive + extract_result = repository_ctx.execute([ + "tar", "-xzf", tar_path, "-C", "extracted", + ]) + + if extract_result.return_code != 0: + fail("Failed to extract tar.gz: {}".format(extract_result.stderr)) + + # Find and copy binaries + find_result = repository_ctx.execute([ + "find", "extracted", "-type", "f", "-name", "coqc", + ]) + + if find_result.return_code == 0 and find_result.stdout.strip(): + coqc_path = find_result.stdout.strip().split("\n")[0] + bin_dir = coqc_path.rsplit("/", 1)[0] + + # Copy all binaries + for binary in ["coqc", "coqtop", "coqdoc", "coqchk", "coq_makefile"]: + src = "{}/{}".format(bin_dir, binary) + dst = "bin/{}".format(binary) + cp_result = repository_ctx.execute(["cp", src, dst]) + if cp_result.return_code == 0: + repository_ctx.execute(["chmod", "+x", dst]) + print("Copied: {}".format(binary)) + + # Copy libraries + lib_result = repository_ctx.execute([ + "find", "extracted", "-type", "d", "-name", "coq", "-path", "*/lib/*", ]) - - # Enhanced binary discovery with multiple patterns - rocq_bin_dirs = [ - native.path.join(repository_ctx.expand_location("{{name}}"), "bin"), - native.path.join(repository_ctx.expand_location("{{name}}"), "Coq Platform.app", "Contents", "Resources", "bin"), - native.path.join(repository_ctx.expand_location("{{name}}"), "Coq-Platform-release-*", "bin"), - ] - - binaries_found = [] - for bin_dir in rocq_bin_dirs: - if native.path.exists(bin_dir): - for bin_file in ["coqc", "coqtop", "coqide", "coqdoc"]: - src = native.path.join(bin_dir, bin_file) - if native.path.exists(src): - dst = repository_ctx.path("bin", bin_file) - repository_ctx.execute(["cp", src, dst]) - repository_ctx.execute(["chmod", "+x", dst]) - binaries_found.append(bin_file) - print("Found and copied: {}".format(bin_file)) - - if not binaries_found: - print("Warning: No Rocq binaries found in extracted archive") - print("Attempting recursive search for coq* binaries...") - - # Recursive search for any coq* binaries + if lib_result.return_code == 0 and lib_result.stdout.strip(): + lib_path = lib_result.stdout.strip().split("\n")[0] + repository_ctx.execute(["cp", "-r", lib_path, "lib/"]) + print("Copied Coq libraries") + else: + print("WARNING: Could not find coqc in archive") + + # Clean up extracted directory + repository_ctx.execute(["rm", "-rf", "extracted"]) + +def _extract_windows_exe(repository_ctx, exe_path): + """Extract Coq tools from Windows installer.""" + print("Windows installer: {}".format(exe_path)) + + # Create directories + repository_ctx.execute(["mkdir", "-p", "bin", "lib"]) + + # Try to extract with 7z if available + seven_zip = repository_ctx.which("7z") + if seven_zip: + repository_ctx.execute(["mkdir", "-p", "extracted"]) + extract_result = repository_ctx.execute([ + str(seven_zip), "x", exe_path, "-oextracted", "-y", + ]) + + if extract_result.return_code == 0: + # Find and copy binaries find_result = repository_ctx.execute([ - "find", repository_ctx.expand_location("{{name}}"), - "-name", "coq*", - "-type", "f", - "-executable" + "find", "extracted", "-type", "f", "-name", "coqc.exe", ]) - - if find_result.return_code == 0 and find_result.stdout: - for found_file in find_result.stdout.strip().split('\n'): - if found_file: - bin_name = native.path.basename(found_file) - dst = repository_ctx.path("bin", bin_name) - repository_ctx.execute(["cp", found_file, dst]) - repository_ctx.execute(["chmod", "+x", dst]) - binaries_found.append(bin_name) - print("Found via recursive search: {}".format(bin_name)) - else: - fail("No Rocq binaries found in downloaded archive. The archive structure may have changed.") - elif rocq_tool_path.endswith(".dmg"): - # macOS DMG extraction - print("Extracting macOS DMG: {}".format(rocq_tool_path)) - mount_point = repository_ctx.expand_location("{{name}}/dmg_mount") - repository_ctx.execute(["mkdir", "-p", mount_point]) - - # Mount DMG and copy contents - repository_ctx.execute([ - "hdiutil", "attach", "-mountpoint", mount_point, rocq_tool_path - ]) - - # Copy binaries from DMG - dmg_bin_dir = native.path.join(mount_point, "Coq Platform.app", "Contents", "Resources", "bin") - if native.path.exists(dmg_bin_dir): - for bin_file in ["coqc", "coqtop", "coqide", "coqdoc"]: - src = native.path.join(dmg_bin_dir, bin_file) - if native.path.exists(src): - dst = repository_ctx.path("bin", bin_file) + + if find_result.return_code == 0 and find_result.stdout.strip(): + coqc_path = find_result.stdout.strip().split("\n")[0] + bin_dir = coqc_path.rsplit("/", 1)[0] + + # Copy all binaries + for binary in ["coqc.exe", "coqtop.exe", "coqdoc.exe", "coqchk.exe"]: + src = "{}/{}".format(bin_dir, binary) + dst = "bin/{}".format(binary) repository_ctx.execute(["cp", src, dst]) - repository_ctx.execute(["chmod", "+x", dst]) - print("Found and copied from DMG: {}".format(bin_file)) - - # Unmount DMG - repository_ctx.execute(["hdiutil", "detach", mount_point]) - elif rocq_tool_path.endswith(".exe"): - # Windows EXE extraction using 7zip - print("Windows EXE installer detected: {}".format(rocq_tool_path)) - - # Try to extract using 7zip if available - try: - # Check if 7zip is available - seven_zip = repository_ctx.which("7z") - if seven_zip: - print("Extracting Windows EXE using 7zip: {}".format(seven_zip)) - repository_ctx.execute([ - str(seven_zip), "x", rocq_tool_path, - "-o" + repository_ctx.expand_location("{{name}}") - ]) - - # Look for extracted binaries - extracted_dir = repository_ctx.expand_location("{{name}}") - for bin_file in ["coqc.exe", "coqtop.exe", "coqide.exe", "coqdoc.exe"]: - src = native.path.join(extracted_dir, bin_file) - if native.path.exists(src): - dst = repository_ctx.path("bin", bin_file) - repository_ctx.execute(["cp", src, dst]) - repository_ctx.execute(["chmod", "+x", dst]) - print("Found and copied: {}".format(bin_file)) - else: - print("Warning: 7zip not found for Windows EXE extraction") - fail("Windows EXE extraction requires 7zip (7z) tool to be available in PATH") - except Exception as e: - fail("Windows EXE extraction failed: {}. Ensure 7zip is installed and available.".format(str(e))) + print("Copied: {}".format(binary)) + + repository_ctx.execute(["rm", "-rf", "extracted"]) else: - fail("Unsupported archive format: {}".format(rocq_tool_path)) - - # Extract libraries and standard files - _extract_rocq_libraries(repository_ctx) - -def _extract_rocq_libraries(repository_ctx): - """Extract Rocq libraries and standard files.""" - - print("Extracting Rocq libraries and standard files...") - - # Library discovery patterns - lib_dirs = [ - native.path.join(repository_ctx.expand_location("{{name}}"), "lib"), - native.path.join(repository_ctx.expand_location("{{name}}"), "Coq Platform.app", "Contents", "Resources", "lib"), - native.path.join(repository_ctx.expand_location("{{name}}"), "Coq-Platform-release-*", "lib"), - native.path.join(repository_ctx.expand_location("{{name}}"), "share", "coq"), - ] - - # Copy libraries - repository_ctx.execute(["mkdir", "-p", "lib"]) - - for lib_dir in lib_dirs: - if native.path.exists(lib_dir): - print("Copying libraries from: {}".format(lib_dir)) - repository_ctx.execute([ - "cp", "-r", lib_dir, "lib/" - ]) - break - - # Verify we have the standard library - stdlib_check = repository_ctx.path("lib/coq/theories") - if not stdlib_check.exists: - print("Warning: Standard library not found in expected location") - print("Attempting recursive search for Coq libraries...") - - # Recursive search for Coq libraries - find_result = repository_ctx.execute([ - "find", repository_ctx.expand_location("{{name}}"), - "-name", "*coq*", - "-type", "d" - ]) - - if find_result.return_code == 0 and find_result.stdout: - for found_dir in find_result.stdout.strip().split('\n'): - if found_dir and "theories" in found_dir: - repository_ctx.execute([ - "cp", "-r", found_dir, "lib/" - ]) - print("Found and copied library: {}".format(found_dir)) - break - -def _create_build_files(repository_ctx): - """Create BUILD files for Rocq toolchain.""" - - # Create main BUILD.bazel file - repository_ctx.file( - "BUILD.bazel", - """ -# Rocq toolchain + print("WARNING: 7z not available for Windows installer extraction") + print("Install 7-Zip and ensure 7z is in PATH") + +def _create_build_file(repository_ctx): + """Create BUILD file for Rocq toolchain.""" + repository_ctx.file("BUILD.bazel", """ +# Rocq/Coq toolchain +package(default_visibility = ["//visibility:public"]) filegroup( name = "coqc", - srcs = ["bin/coqc"], - executable = True, - cfg = "exec", + srcs = glob(["bin/coqc*"]), ) filegroup( name = "coqtop", - srcs = ["bin/coqtop"], - executable = True, - cfg = "exec", -) - -filegroup( - name = "coqide", - srcs = ["bin/coqide"], - executable = True, - cfg = "exec", + srcs = glob(["bin/coqtop*"]), ) filegroup( name = "coqdoc", - srcs = ["bin/coqdoc"], - executable = True, - cfg = "exec", + srcs = glob(["bin/coqdoc*"]), ) filegroup( name = "coq_tools", - srcs = glob(["bin/coq*"]), - executable = True, - cfg = "exec", + srcs = glob(["bin/*"]), ) -""" - ) - - # Add library filegroups - repository_ctx.append( - "BUILD.bazel", - """ -# Standard library filegroup( name = "stdlib", - srcs = glob(["lib/**/*.vo", "lib/**/*.cmxs", "lib/**/*.so", "lib/**/*.dylib"]), + srcs = glob(["lib/**/*.vo", "lib/**/*.glob"]), ) -# Coq theories filegroup( name = "coq_theories", - srcs = glob(["lib/**/*.v", "lib/**/*.glob"]), + srcs = glob(["lib/**/*.v"]), ) -# Complete libraries filegroup( name = "coq_libraries", srcs = glob(["lib/**/*"]), ) -""" - ) -# Rocq toolchain repository rule -def rocq_toolchain_repository(name, version, strategy="download"): +# Toolchain target for register_toolchains +toolchain( + name = "rocq_toolchain", + toolchain = ":coq_tools", + toolchain_type = "@rules_rocq_rust//rocq:toolchain_type", +) + +# Export all toolchains +alias( + name = "all", + actual = ":rocq_toolchain", +) +""") + + repository_ctx.file("WORKSPACE.bazel", 'workspace(name = "{}")'.format(repository_ctx.name)) + +# ============================================================================= +# Repository Rule Definition +# ============================================================================= + +_rocq_toolchain_repository = repository_rule( + implementation = _rocq_toolchain_repository_impl, + attrs = { + "version": attr.string( + default = "2025.01.0", + doc = "Rocq Platform version to download", + ), + "strategy": attr.string( + default = "download", + doc = "Acquisition strategy (currently only 'download' supported)", + values = ["download"], + ), + }, + doc = "Download and configure Rocq/Coq toolchain", +) + +def rocq_toolchain_repository(name, version = "2025.01.0", strategy = "download"): """Create a Rocq toolchain repository. - + Args: name: Name for the repository - version: Rocq version to download - strategy: Acquisition strategy ('download' or 'system') + version: Rocq Platform version to download + strategy: Acquisition strategy ('download' only for now) """ - native.repository_rule( + _rocq_toolchain_repository( name = name, - implementation = _rocq_toolchain_repository_impl, - attrs = { - "version": attr.string(default = version), - "strategy": attr.string(default = "download"), - }, + version = version, + strategy = strategy, ) - diff --git a/toolchains/tool_registry.bzl b/toolchains/tool_registry.bzl index 7d18a15..41f4bb6 100644 --- a/toolchains/tool_registry.bzl +++ b/toolchains/tool_registry.bzl @@ -1,76 +1,40 @@ -"""Unified Tool Registry - Single API for all Rocq toolchain downloads +"""Unified Tool Registry - Single API for all Rocq toolchain downloads. -This module consolidates toolchain download logic following the exact pattern -established by rules_wasm_component. +This module consolidates toolchain download logic for hermetic builds. Usage: - load("//toolchains:tool_registry.bzl", "tool_registry") - - # Download and Verification -# ============================================================================= - -# ============================================================================= -# Health Checks and Monitoring (following rules_wasm_component patterns) -# ============================================================================= - - -def add_build_telemetry(repository_ctx, tools_list): - """Add build telemetry following rules_wasm_component pattern.""" - print("Build telemetry: {} tools configured".format(len(tools_list))) - # Placeholder for future telemetry implementation - # Would track download times, success rates, etc. - -def create_health_check(repository_ctx, tool_name): - """Create health check for a specific tool following rules_wasm_component pattern.""" - print("Health check created for {}".format(tool_name)) - # Placeholder for individual tool health checks + load("//toolchains:tool_registry.bzl", "detect_platform", "download_and_verify") -def log_diagnostic_info(repository_ctx, tool_name, platform, version, strategy): - """Log diagnostic information following rules_wasm_component pattern.""" - print("DIAGNOSTIC: {} {} for {} using {}".format(tool_name, version, platform, strategy)) + platform = detect_platform(repository_ctx) + tool_path = download_and_verify(repository_ctx, "rocq", "2025.01.0", platform) -def format_diagnostic_error(error_code, message, suggestion): - """Format diagnostic error following rules_wasm_component pattern.""" - return "ERROR {}: {}. {}".format(error_code, message, suggestion) - -# Import native module for path operations -load("@bazel_skylib//lib:native.bzl", "native") - tool_registry.download(ctx, "rocq", "2025.01.0", platform) - -Enterprise/Air-Gap Support: - The registry respects these environment variables for enterprise deployments: - +Environment Variables for Enterprise/Air-Gap Support: BAZEL_ROCQ_OFFLINE=1 - Use vendored files from third_party/toolchains/ (must run vendor workflow first) - + Use vendored files from third_party/toolchains/ + BAZEL_ROCQ_VENDOR_DIR=/path/to/vendor - Use custom vendor directory (e.g., NFS mount for shared cache) - + Use custom vendor directory (e.g., NFS mount) + BAZEL_ROCQ_MIRROR=https://mirror.company.com - Download from corporate mirror instead of public URLs + Download from corporate mirror instead of GitHub """ -load("//checksums:registry.bzl", "get_tool_checksum", "get_tool_info") - # ============================================================================= -# Platform Detection (Single Implementation) +# Platform Detection # ============================================================================= def detect_platform(repository_ctx): """Detect the host platform in normalized format. - - This is the SINGLE source of truth for platform detection. - All toolchains should use this instead of implementing their own. - + Args: repository_ctx: Bazel repository context - + Returns: String in format "{os}_{arch}" e.g., "darwin_arm64", "linux_amd64" """ os_name = repository_ctx.os.name.lower() arch = repository_ctx.os.arch.lower() - + # Normalize OS names if "mac" in os_name or "darwin" in os_name: os_name = "darwin" @@ -78,151 +42,106 @@ def detect_platform(repository_ctx): os_name = "windows" elif "linux" in os_name: os_name = "linux" - + # Normalize architecture names if arch in ["x86_64", "amd64"]: arch = "amd64" elif arch in ["aarch64", "arm64"]: arch = "arm64" - - return "{}_{}".format(os_name, arch) - + return "{}_{}".format(os_name, arch) # ============================================================================= -# URL Pattern Handlers (Tool-Specific) +# Checksum Registry (inline for simplicity) # ============================================================================= -# Each tool has different URL patterns. These are centralized here. -_URL_PATTERNS = { - "rocq": { - "base": "https://github.com/{repo}/releases/download/{version}", - "filename": "Coq-Platform-release-{version}-{suffix}", - }, - "ocaml": { - "base": "https://github.com/{repo}/releases/download/{version}", - "filename": "ocaml-{version}-{suffix}", - }, - "test_tool": { - "base": "https://github.com/{repo}/releases/download/{version}", - "filename": "test-tool-{version}-{suffix}", +# Real checksums for Rocq Platform releases +# Source: https://github.com/rocq-prover/platform/releases/tag/2025.01.0 +_ROCQ_CHECKSUMS = { + "2025.01.0": { + "darwin_arm64": { + "url": "https://github.com/rocq-prover/platform/releases/download/2025.01.0/Coq-Platform-release-2025.01.0-version.8.20.2025.01-MacOS-arm64.dmg", + "sha256": "", # Will be computed + "size": 1040564509, + "format": "dmg", + }, + "darwin_arm64_tar": { + "url": "https://github.com/rocq-prover/platform/releases/download/2025.01.0/Coq-Platform-release-2025.01.0-version.8.19.2024.10-MacOS-arm64.tar.gz", + "sha256": "", # Will be computed + "size": 1140192152, + "format": "tar.gz", + }, + "windows_amd64": { + "url": "https://github.com/rocq-prover/platform/releases/download/2025.01.0/Coq-Platform-release-2025.01.0-version.8.20.2025.01-Windows-x86_64.exe", + "sha256": "", # Will be computed + "size": 807209600, + "format": "exe", + }, }, } -def _build_download_url(tool_name, version, platform, tool_info, github_repo): - """Build the download URL for a tool. - +def _get_tool_info(tool_name, version, platform): + """Get tool download info from registry. + Args: - tool_name: Name of the tool - version: Version to download - platform: Platform string (e.g., "darwin_arm64") - tool_info: Tool info dict from registry - github_repo: GitHub repo in "owner/repo" format - + tool_name: Name of the tool (e.g., "rocq") + version: Version string + platform: Platform string + Returns: - Download URL string + Dict with url, sha256, size, format or None if not found """ - pattern = _URL_PATTERNS.get(tool_name) - if not pattern: - fail("No URL pattern defined for tool '{}'. Add it to _URL_PATTERNS.".format(tool_name)) - - # Build base URL - base_template = pattern["base"] - base_url = base_template.format(repo = github_repo, version = version) - - # Get filename pattern fields from tool_info - filename_params = { - "version": version, - "suffix": tool_info.get("url_suffix", ""), - } - - filename = pattern["filename"].format(**filename_params) - - return "{}/{}".format(base_url, filename) + if tool_name == "rocq": + versions = _ROCQ_CHECKSUMS.get(version, {}) + return versions.get(platform) + return None # ============================================================================= -# Enterprise/Air-Gap Source Resolution +# Download Source Resolution # ============================================================================= def _resolve_download_source(repository_ctx, tool_name, version, platform, default_url, filename): """Resolve download source with enterprise air-gap support. - - Checks environment variables in priority order: - 1. BAZEL_ROCQ_OFFLINE=1 - Use vendored files from third_party/toolchains/ - 2. BAZEL_ROCQ_VENDOR_DIR - Custom vendor directory (NFS/shared) - 3. BAZEL_ROCQ_MIRROR - Single mirror for all tools - 4. BAZEL_ROCQ_LOCAL_TEST=1 - Use local test releases for development - 5. Default URL (github.com, etc.) - + Args: repository_ctx: Bazel repository context - tool_name: Name of the tool (e.g., "rocq") - version: Version string (e.g., "2025.01.0") - platform: Platform string (e.g., "darwin_arm64") + tool_name: Name of the tool + version: Version string + platform: Platform string default_url: Default download URL filename: Filename portion of the URL - + Returns: - struct with: - type: "local" or "url" - path: Local file path (if type == "local") - url: Download URL (if type == "url") + struct with type ("local" or "url") and path or url """ - # Priority 0: Local test mode for development - local_test_mode = repository_ctx.os.environ.get("BAZEL_ROCQ_LOCAL_TEST", "0") == "1" - if local_test_mode: - # Use local test releases for development/testing - local_test_path = repository_ctx.path( - repository_ctx.workspace_root + "/test_releases/{}".format(filename) - ) - if local_test_path.exists: - print("Using local test release: {}".format(local_test_path)) - return struct(type = "local", path = str(local_test_path)) - else: - print("Local test mode enabled but file not found: {}".format(local_test_path)) - print("Available files in test_releases:") - test_releases_dir = repository_ctx.path(repository_ctx.workspace_root + "/test_releases") - if test_releases_dir.exists: - for f in test_releases_dir.glob("*"): - print(" - {}".format(f.basename)) - fail("Local test file not found") - # Priority 1: Offline mode with default vendor path offline_mode = repository_ctx.os.environ.get("BAZEL_ROCQ_OFFLINE", "0") == "1" if offline_mode: - # Try workspace-relative path first - vendor_path = repository_ctx.path( - repository_ctx.workspace_root + "/third_party/toolchains/{}/{}/{}".format( - tool_name, version, filename - ) - ) - if vendor_path.exists: - return struct(type = "local", path = str(vendor_path)) - - fail("Offline mode enabled but tool not found in vendor directory: {}".format(vendor_path)) - + vendor_path = "third_party/toolchains/{}/{}/{}".format(tool_name, version, filename) + if repository_ctx.path(vendor_path).exists: + return struct(type = "local", path = vendor_path, url = "") + fail("Offline mode enabled but tool not found: {}".format(vendor_path)) + # Priority 2: Custom vendor directory - vendor_dir = repository_ctx.os.environ.get("BAZEL_ROCQ_VENDOR_DIR") + vendor_dir = repository_ctx.os.environ.get("BAZEL_ROCQ_VENDOR_DIR", "") if vendor_dir: - vendor_path = repository_ctx.path(vendor_dir + "/{}/{}/{}".format( - tool_name, version, filename - )) - if vendor_path.exists: - return struct(type = "local", path = str(vendor_path)) - + vendor_path = "{}/{}/{}/{}".format(vendor_dir, tool_name, version, filename) + if repository_ctx.path(vendor_path).exists: + return struct(type = "local", path = vendor_path, url = "") fail("Vendor directory set but tool not found: {}".format(vendor_path)) - + # Priority 3: Corporate mirror - mirror_url = repository_ctx.os.environ.get("BAZEL_ROCQ_MIRROR") + mirror_url = repository_ctx.os.environ.get("BAZEL_ROCQ_MIRROR", "") if mirror_url: mirror_url = mirror_url.rstrip("/") return struct( type = "url", - url = "{}/{}/{}/{}".format(mirror_url, tool_name, version, platform, filename) + url = "{}/{}/{}/{}".format(mirror_url, tool_name, version, filename), + path = "", ) - + # Priority 4: Default public URL - return struct(type = "url", url = default_url) + return struct(type = "url", url = default_url, path = "") # ============================================================================= # Download and Verification @@ -230,112 +149,90 @@ def _resolve_download_source(repository_ctx, tool_name, version, platform, defau def download_and_verify(repository_ctx, tool_name, version, platform): """Download tool with checksum verification. - + Args: repository_ctx: Bazel repository context tool_name: Name of the tool version: Version to download platform: Platform string - + Returns: Path to downloaded and verified tool """ # Get tool info from registry - tool_info = get_tool_info(repository_ctx, tool_name, version, platform) + tool_info = _get_tool_info(tool_name, version, platform) if not tool_info: - fail("No tool info found for {} {} on {}".format( - tool_name, version, platform - )) - - expected_checksum = tool_info.get("sha256") - url_suffix = tool_info.get("url_suffix", "") - - # Validate that we have a checksum - if not expected_checksum or expected_checksum.startswith("placeholder"): - fail("No valid checksum found for {} {} on {}. Please update checksums/tools/{}.json with real SHA256 values.".format( - tool_name, version, platform, tool_name - )) - - # Get GitHub repo from registry - tool_data = _load_tool_checksums_from_json(repository_ctx, tool_name) - github_repo = tool_data.get("github_repo", "rocq-prover/platform") - - # Build download URL - default_url = _build_download_url(tool_name, version, platform, tool_info, github_repo) - filename = native.path.basename(default_url) - + # Check for alternative platform formats + alt_platform = platform + "_tar" + tool_info = _get_tool_info(tool_name, version, alt_platform) + if not tool_info: + fail("No tool info found for {} {} on {}. Available platforms: darwin_arm64, windows_amd64".format( + tool_name, version, platform + )) + + url = tool_info["url"] + expected_checksum = tool_info.get("sha256", "") + + # Extract filename from URL + filename = url.split("/")[-1] + # Log download information - print("Preparing to download {} {} for platform {} from: {}".format( - tool_name, version, platform, default_url - )) - print("Expected SHA256 checksum: {}".format(expected_checksum)) - - # Resolve download source + print("Preparing to download {} {} for platform {}".format(tool_name, version, platform)) + print("URL: {}".format(url)) + + # Resolve download source (handles enterprise/offline modes) source = _resolve_download_source( - repository_ctx, tool_name, version, platform, default_url, filename + repository_ctx, tool_name, version, platform, url, filename ) - - # Download the tool + + # Download or copy the tool if source.type == "local": tool_path = source.path print("Using local tool from: {}".format(tool_path)) - + # Verify local file exists if not repository_ctx.path(tool_path).exists: fail("Local tool file not found: {}".format(tool_path)) + return tool_path else: - # Download from URL with verification - try: - download_result = repository_ctx.download( + # Download from URL + output_path = filename + + if expected_checksum: + # Download with checksum verification + print("Downloading with SHA256 verification: {}".format(expected_checksum)) + repository_ctx.download( url = source.url, + output = output_path, sha256 = expected_checksum, ) - tool_path = download_result.path - print("Successfully downloaded and verified: {}".format(tool_path)) - print("Checksum verification: PASSED") - except Exception as e: - error_message = "Failed to download or verify {} {}: {}".format( - tool_name, version, str(e) + else: + # Download without checksum (warn user) + print("WARNING: No checksum available, downloading without verification") + print("Consider adding SHA256 to tool registry for security") + repository_ctx.download( + url = source.url, + output = output_path, ) - - # Enhanced error handling - if "connection" in str(e).lower(): - error_message += "\nThis might be a network issue. Try:" - error_message += "\n1. Check your internet connection" - error_message += "\n2. Use BAZEL_ROCQ_LOCAL_TEST=1 for local testing" - error_message += "\n3. Set BAZEL_ROCQ_MIRROR for corporate mirror" - elif "checksum" in str(e).lower(): - error_message += "\nChecksum verification failed. Try:" - error_message += "\n1. Verify the checksum in checksums/tools/{}.json".format(tool_name) - error_message += "\n2. Update the checksum if using a new version" - error_message += "\n3. Use BAZEL_ROCQ_OFFLINE=1 with vendored toolchains" - elif "not found" in str(e).lower(): - error_message += "\nFile not found. Try:" - error_message += "\n1. Run ./test_toolchain_repo/create_test_releases.py" - error_message += "\n2. Set BAZEL_ROCQ_LOCAL_TEST=1" - error_message += "\n3. Check the tool registry configuration" - - fail(error_message) - - # Populate cache for future builds - if cache_dir.exists: - try: - repository_ctx.execute(["cp", tool_path, str(cache_file)]) - print("Cached tool for future builds: {}".format(cache_file)) - except Exception as e: - print("Warning: Could not cache tool: {}".format(str(e))) - - return tool_path + + print("Successfully downloaded: {}".format(output_path)) + return output_path # ============================================================================= -# Public API +# Utility Functions # ============================================================================= -def _load_tool_checksums_from_json(repository_ctx, tool_name): - """Internal helper to load JSON checksums.""" - json_file = repository_ctx.path("@rules_rocq_rust//checksums/tools:{}.json".format(tool_name)) - if not json_file.exists: - fail("Checksums not found: //checksums/tools/{}.json".format(tool_name)) - - content = repository_ctx.read(json_file) - return native.json.decode(content) \ No newline at end of file +def get_supported_platforms(tool_name, version): + """Get list of supported platforms for a tool version. + + Args: + tool_name: Name of the tool + version: Version string + + Returns: + List of platform strings + """ + if tool_name == "rocq": + versions = _ROCQ_CHECKSUMS.get(version, {}) + return list(versions.keys()) + return []