diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d1ad9d01a..7688d008b 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 d66af4206..fc0e38f60 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 77d38a85f..66285c9c1 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 {