From 060becff9c6684392afd548e43e423f15ac9f833 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 15 Jul 2026 14:35:04 +0200 Subject: [PATCH] nix: repair flake for Nix 2.35 / macOS 26, modernize toolchain The flake had rotted against current toolchains: - `nixpkgs` declared both a URL and a `follows`; Nix >= 2.25 rejects the ambiguity (the `follows` was what the lock resolved all along). - The opam `conf-git` check had no git in its build environment; give it one via the overlay, like the existing `conf-pkg-config` fix. - opam-nix (2025-01) referenced `darwin.apple_sdk`, removed from nixpkgs, and its pinned nixpkgs shipped binaries that macOS 26's dyld rejects (duplicate LC_RPATH). Update opam-nix to 2026-06. - The pinned provers (z3 4.12.6, cvc4 1.8, cvc5 1.0.9) no longer compile with the clang 19 that comes with the newer nixpkgs. Take z3 (4.15.1) and cvc5 (1.3.0) directly from nixpkgs and drop cvc4 (archived upstream), removing the source pins and the mkProverPackage machinery. While at it, modernize the toolchain: OCaml 4.14.2 -> 5.4.1 and Alt-Ergo 2.4.3 -> 2.6.3, with opam-repository advanced to 2026-07-14 (this also moves why3 to 1.8.2). Alt-Ergo 2.6.3's dune build invokes codesign on macOS, so the overlay's darwin.sigtool fix is extended to it. ci: bump install-nix-action to v31 so CI exercises a current Nix (v26's would not have caught the input conflict), cachix-action to v17. --- .github/workflows/ci.yml | 4 +- flake.lock | 165 +++++++++++++++++++++------------------ flake.nix | 40 +++------- 3 files changed, 103 insertions(+), 106 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d1ad9d01a8..7688d008b4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -94,11 +94,11 @@ jobs: steps: - uses: actions/checkout@v4 - name: Setup Nix - uses: cachix/install-nix-action@v26 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable - name: Setup Cachix - uses: cachix/cachix-action@v14 + uses: cachix/cachix-action@v17 with: name: formosa-crypto authToken: '${{ secrets.CACHIX_WRITE_TOKEN }}' diff --git a/flake.lock b/flake.lock index d66af42062..fc0e38f60e 100644 --- a/flake.lock +++ b/flake.lock @@ -3,11 +3,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1696426674, - "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "lastModified": 1747046372, + "narHash": "sha256-CIVLLkVgvHYbgI2UpXvIIBJ12HWgX+fjA8Xf8PUmqCY=", "owner": "edolstra", "repo": "flake-compat", - "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "rev": "9100a0f413b0c601e0533d1d94ffd501ce2e7885", "type": "github" }, "original": { @@ -39,11 +39,11 @@ "systems": "systems_2" }, "locked": { - "lastModified": 1726560853, - "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -70,11 +70,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1730785428, - "narHash": "sha256-Zwl8YgTVJTEum+L+0zVAWvXAGbWAuXHax3KzuejaDyo=", + "lastModified": 1751792365, + "narHash": "sha256-J1kI6oAj25IG4EdVlg2hQz8NZTBNYvIS0l4wpr9KcUo=", "owner": "nixos", "repo": "nixpkgs", - "rev": "4aa36568d413aca0ea84a1684d2d46f55dbabad7", + "rev": "1fd8bada0b6117e6c7eb54aad5813023eed37ccb", "type": "github" }, "original": { @@ -84,22 +84,73 @@ "type": "github" } }, + "nixpkgs-llvm17": { + "locked": { + "lastModified": 1723734425, + "narHash": "sha256-GwSfzmTMpM+gAJHURHNRle6AX9nhhdZnC41tC4AkvO8=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "35e0ed8d1875d2303fab9930c6eb205654a2f6a3", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "35e0ed8d1875d2303fab9930c6eb205654a2f6a3", + "type": "github" + } + }, + "nixpkgs-python38": { + "locked": { + "lastModified": 1708815994, + "narHash": "sha256-hL7N/ut2Xu0NaDxDMsw2HagAjgDskToGiyZOWriiLYM=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "9a9dae8f6319600fa9aebde37f340975cab4b8c0", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "9a9dae8f6319600fa9aebde37f340975cab4b8c0", + "type": "github" + } + }, + "nixpkgs-python39": { + "locked": { + "lastModified": 1743938762, + "narHash": "sha256-UgFYn8sGv9B8PoFpUfCa43CjMZBl1x/ShQhRDHBFQdI=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "74a40410369a1c35ee09b8a1abee6f4acbedc059", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "74a40410369a1c35ee09b8a1abee6f4acbedc059", + "type": "github" + } + }, "opam-nix": { "inputs": { "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", "mirage-opam-overlays": "mirage-opam-overlays", "nixpkgs": "nixpkgs", + "nixpkgs-llvm17": "nixpkgs-llvm17", + "nixpkgs-python38": "nixpkgs-python38", + "nixpkgs-python39": "nixpkgs-python39", "opam-overlays": "opam-overlays", "opam-repository": "opam-repository", "opam2json": "opam2json" }, "locked": { - "lastModified": 1736955560, - "narHash": "sha256-9I42xwKXH7h+jQGJQ8t797j/mWylIItIljRLm44CHS8=", + "lastModified": 1782476416, + "narHash": "sha256-oFdLuHny6fe6kSOrOTN5Bfls+GisFiM8ytYrBQpGRog=", "owner": "tweag", "repo": "opam-nix", - "rev": "5f760f445d6693eb086327fa7d7ae8e43c906718", + "rev": "583fb2ed4db44fcda4f6222c554949503d50a352", "type": "github" }, "original": { @@ -111,11 +162,11 @@ "opam-overlays": { "flake": false, "locked": { - "lastModified": 1726822209, - "narHash": "sha256-bwM18ydNT9fYq91xfn4gmS21q322NYrKwfq0ldG9GYw=", + "lastModified": 1741116009, + "narHash": "sha256-Z0PIW82fHJFvAv/JYpAffnp2DaOjLhsPutqyIrORZd0=", "owner": "dune-universe", "repo": "opam-overlays", - "rev": "f2bec38beca4aea9e481f2fd3ee319c519124649", + "rev": "e031bb64e33bf93be963e9a38b28962e6e14381f", "type": "github" }, "original": { @@ -127,11 +178,11 @@ "opam-repository": { "flake": false, "locked": { - "lastModified": 1736935757, - "narHash": "sha256-LNkGSkZJXJmxpUd+luDUIIV/1B5MZIBMTB1qZqypa4o=", + "lastModified": 1784065055, + "narHash": "sha256-yT+DNlquArnWu8ZQ1uVEKE/HUuo7ZNwyOT8yvqiL30c=", "owner": "ocaml", "repo": "opam-repository", - "rev": "a8b00ead922e2049581ab16994586ed4ddbdb784", + "rev": "8b272f4f03d431daf02557fa2c4b788825c6aae2", "type": "github" }, "original": { @@ -145,14 +196,15 @@ "nixpkgs": [ "opam-nix", "nixpkgs" - ] + ], + "systems": "systems_3" }, "locked": { - "lastModified": 1671540003, - "narHash": "sha256-5pXfbUfpVABtKbii6aaI2EdAZTjHJ2QntEf0QD2O5AM=", + "lastModified": 1782276984, + "narHash": "sha256-rBGN9TERADPXiehNe1/9emO6QqYPrTwSoMdB+BVEWpM=", "owner": "tweag", "repo": "opam2json", - "rev": "819d291ea95e271b0e6027679de6abb4d4f7f680", + "rev": "88b2a71f6e2df38d3304d3900ee129f4e83048f8", "type": "github" }, "original": { @@ -161,57 +213,6 @@ "type": "github" } }, - "prover_cvc4_1_8": { - "flake": false, - "locked": { - "lastModified": 1592585967, - "narHash": "sha256-V6KShPLW6kFBJaNgqy98rjOxULmf5c8AmDwo9fclGuY=", - "owner": "CVC4", - "repo": "CVC4-archived", - "rev": "5247901077efbc7b9016ba35fded7a6ab459a379", - "type": "github" - }, - "original": { - "owner": "CVC4", - "ref": "1.8", - "repo": "CVC4-archived", - "type": "github" - } - }, - "prover_cvc5_1_0_9": { - "flake": false, - "locked": { - "lastModified": 1702998934, - "narHash": "sha256-AwUQHFftn51Xt6HtmDsWAdkOS8i64r2FhaHu31KYwZA=", - "owner": "cvc5", - "repo": "cvc5", - "rev": "8fca72aebcb5293434c3207dca081a845ff8d6fe", - "type": "github" - }, - "original": { - "owner": "cvc5", - "ref": "cvc5-1.0.9", - "repo": "cvc5", - "type": "github" - } - }, - "prover_z3_4_12_6": { - "flake": false, - "locked": { - "lastModified": 1708814107, - "narHash": "sha256-X4wfPWVSswENV0zXJp/5u9SQwGJWocLKJ/CNv57Bt+E=", - "owner": "z3prover", - "repo": "z3", - "rev": "fa2c0e027894a8d55d2b841e27cbeecc99692a3f", - "type": "github" - }, - "original": { - "owner": "z3prover", - "ref": "z3-4.12.6", - "repo": "z3", - "type": "github" - } - }, "root": { "inputs": { "flake-utils": "flake-utils", @@ -220,9 +221,6 @@ "nixpkgs" ], "opam-nix": "opam-nix", - "prover_cvc4_1_8": "prover_cvc4_1_8", - "prover_cvc5_1_0_9": "prover_cvc5_1_0_9", - "prover_z3_4_12_6": "prover_z3_4_12_6", "stable": "stable" } }, @@ -271,6 +269,21 @@ "repo": "default", "type": "github" } + }, + "systems_3": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index 77d38a85ff..66285c9c11 100644 --- a/flake.nix +++ b/flake.nix @@ -4,24 +4,9 @@ flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:nixos/nixpkgs/24.05"; stable.url = "github:nixos/nixpkgs/24.05"; nixpkgs.follows = "opam-nix/nixpkgs"; - prover_cvc4_1_8 = { - url = "github:CVC4/CVC4-archived/1.8"; - flake = false; - }; - - prover_cvc5_1_0_9 = { - url = "github:cvc5/cvc5/cvc5-1.0.9"; - flake = false; - }; - - prover_z3_4_12_6 = { - url = "github:z3prover/z3/z3-4.12.6"; - flake = false; - }; }; outputs = { self, flake-utils, opam-nix, nixpkgs, ... }@inputs: @@ -40,7 +25,7 @@ }; query = devPackagesQuery // { - ocaml-base-compiler = "4.14.2"; + ocaml-base-compiler = "5.4.1"; }; scope = on.buildOpamProject' { } ./. query; @@ -57,6 +42,13 @@ conf-pkg-config = prev.conf-pkg-config.overrideAttrs (oa: { nativeBuildInputs = oa.nativeBuildInputs ++ [pkgs.pkg-config]; }); + conf-git = prev.conf-git.overrideAttrs (oa: { + nativeBuildInputs = oa.nativeBuildInputs ++ [pkgs.git]; + }); + alt-ergo = prev.alt-ergo.overrideAttrs (oa: { + nativeBuildInputs = oa.nativeBuildInputs + ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [ pkgs.darwin.sigtool ]; + }); }; scope' = scope.overrideScope overlay; @@ -71,27 +63,19 @@ paths = [ scope'.${package} scope'.why3 ]; }; - # Create provers packages - mkProverPackage = pkg: version: - pkgs.${pkg}.overrideAttrs (_: { - inherit version; - src = inputs."${"prover_" + pkg + "_" + builtins.replaceStrings ["."] ["_"] version}"; - }); - mkAltErgo = version: ((on.queryToScope { } (query // { alt-ergo = version; })).overrideScope overlay).alt-ergo; in rec { legacyPackages = scope'; packages = rec { - z3 = mkProverPackage "z3" "4.12.6"; - cvc4 = mkProverPackage "cvc4" "1.8"; - cvc5 = mkProverPackage "cvc5" "1.0.9"; - altErgo = mkAltErgo "2.4.3"; + z3 = pkgs.z3; + cvc5 = pkgs.cvc5; + altErgo = mkAltErgo "2.6.3"; provers = pkgs.symlinkJoin { name = "provers"; - paths = [ altErgo z3 cvc4 cvc5 ]; + paths = [ altErgo z3 cvc5 ]; }; with_provers = pkgs.symlinkJoin {