diff --git a/dune-project b/dune-project index a8bc5091e..98438be35 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 3.6) +(lang dune 3.13) (using menhir 2.0) (using dune_site 0.1) @@ -16,7 +16,7 @@ (batteries (>= 3)) (camlp-streams (>= 5)) camlzip - (dune (>= 3.6)) + dune dune-build-info dune-site (ocaml-inifiles (>= 1.2)) diff --git a/easycrypt.opam b/easycrypt.opam index 4803cf34a..4a09b45a2 100644 --- a/easycrypt.opam +++ b/easycrypt.opam @@ -4,7 +4,7 @@ depends: [ "batteries" {>= "3"} "camlp-streams" {>= "5"} "camlzip" - "dune" {>= "3.6" & >= "3.6"} + "dune" {>= "3.13"} "dune-build-info" "dune-site" "ocaml-inifiles" {>= "1.2"} diff --git a/flake.lock b/flake.lock index a9f75b44d..d66af4206 100644 --- a/flake.lock +++ b/flake.lock @@ -3,11 +3,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1627913399, - "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=", + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", "owner": "edolstra", "repo": "flake-compat", - "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", "type": "github" }, "original": { @@ -21,11 +21,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1709126324, - "narHash": "sha256-q6EQdSeUZOG26WelxqkmR7kArjgWCdw5sfJVHPH/7j8=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "d465f4819400de7c8d874d50b982301f28a84605", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -35,12 +35,15 @@ } }, "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, "locked": { - "lastModified": 1638122382, - "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", "type": "github" }, "original": { @@ -52,11 +55,11 @@ "mirage-opam-overlays": { "flake": false, "locked": { - "lastModified": 1661959605, - "narHash": "sha256-CPTuhYML3F4J58flfp3ZbMNhkRkVFKmBEYBZY5tnQwA=", + "lastModified": 1710922379, + "narHash": "sha256-j4QREQDUf8oHOX7qg6wAOupgsNQoYlufxoPrgagD+pY=", "owner": "dune-universe", "repo": "mirage-opam-overlays", - "rev": "05f1c1823d891ce4d8adab91f5db3ac51d86dc0b", + "rev": "797cb363df3ff763c43c8fbec5cd44de2878757e", "type": "github" }, "original": { @@ -67,11 +70,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1682362401, - "narHash": "sha256-/UMUHtF2CyYNl4b60Z2y4wwTTdIWGKhj9H301EDcT9M=", + "lastModified": 1730785428, + "narHash": "sha256-Zwl8YgTVJTEum+L+0zVAWvXAGbWAuXHax3KzuejaDyo=", "owner": "nixos", "repo": "nixpkgs", - "rev": "884ac294018409e0d1adc0cae185439a44bd6b0b", + "rev": "4aa36568d413aca0ea84a1684d2d46f55dbabad7", "type": "github" }, "original": { @@ -92,11 +95,11 @@ "opam2json": "opam2json" }, "locked": { - "lastModified": 1706878465, - "narHash": "sha256-0k0KSkU7epRQshZZKsOpyE79lnwn/0q2VagzDhIeZpE=", + "lastModified": 1736955560, + "narHash": "sha256-9I42xwKXH7h+jQGJQ8t797j/mWylIItIljRLm44CHS8=", "owner": "tweag", "repo": "opam-nix", - "rev": "9f03f7e0664c369f25e614d3f3be74ea78b647fa", + "rev": "5f760f445d6693eb086327fa7d7ae8e43c906718", "type": "github" }, "original": { @@ -108,11 +111,11 @@ "opam-overlays": { "flake": false, "locked": { - "lastModified": 1654162756, - "narHash": "sha256-RV68fUK+O3zTx61iiHIoS0LvIk0E4voMp+0SwRg6G6c=", + "lastModified": 1726822209, + "narHash": "sha256-bwM18ydNT9fYq91xfn4gmS21q322NYrKwfq0ldG9GYw=", "owner": "dune-universe", "repo": "opam-overlays", - "rev": "c8f6ef0fc5272f254df4a971a47de7848cc1c8a4", + "rev": "f2bec38beca4aea9e481f2fd3ee319c519124649", "type": "github" }, "original": { @@ -124,11 +127,11 @@ "opam-repository": { "flake": false, "locked": { - "lastModified": 1705008664, - "narHash": "sha256-TTjTal49QK2U0yVOmw6rJhTGYM7tnj3Kv9DiEEiLt7E=", + "lastModified": 1736935757, + "narHash": "sha256-LNkGSkZJXJmxpUd+luDUIIV/1B5MZIBMTB1qZqypa4o=", "owner": "ocaml", "repo": "opam-repository", - "rev": "fa77046c6497f8ca32926acdb7eb1e61777d4c17", + "rev": "a8b00ead922e2049581ab16994586ed4ddbdb784", "type": "github" }, "original": { @@ -175,19 +178,19 @@ "type": "github" } }, - "prover_cvc5_1_0_5": { + "prover_cvc5_1_0_9": { "flake": false, "locked": { - "lastModified": 1678724158, - "narHash": "sha256-l+L59QLLrAEVkAZjhxICJpa+j+jr1k/7B61JlapXGRI=", + "lastModified": 1702998934, + "narHash": "sha256-AwUQHFftn51Xt6HtmDsWAdkOS8i64r2FhaHu31KYwZA=", "owner": "cvc5", "repo": "cvc5", - "rev": "4cb2ab9eb36f64295272a50f61dd1c62903aca4b", + "rev": "8fca72aebcb5293434c3207dca081a845ff8d6fe", "type": "github" }, "original": { "owner": "cvc5", - "ref": "cvc5-1.0.5", + "ref": "cvc5-1.0.9", "repo": "cvc5", "type": "github" } @@ -218,23 +221,23 @@ ], "opam-nix": "opam-nix", "prover_cvc4_1_8": "prover_cvc4_1_8", - "prover_cvc5_1_0_5": "prover_cvc5_1_0_5", + "prover_cvc5_1_0_9": "prover_cvc5_1_0_9", "prover_z3_4_12_6": "prover_z3_4_12_6", "stable": "stable" } }, "stable": { "locked": { - "lastModified": 1701282334, - "narHash": "sha256-MxCVrXY6v4QmfTwIysjjaX0XUhqBbxTWWB4HXtDYsdk=", + "lastModified": 1717179513, + "narHash": "sha256-vboIEwIQojofItm2xGCdZCzW96U85l9nDW3ifMuAIdM=", "owner": "nixos", "repo": "nixpkgs", - "rev": "057f9aecfb71c4437d2b27d3323df7f93c010b7e", + "rev": "63dacb46bf939521bdc93981b4cbb7ecb58427a0", "type": "github" }, "original": { "owner": "nixos", - "ref": "23.11", + "ref": "24.05", "repo": "nixpkgs", "type": "github" } @@ -253,6 +256,21 @@ "repo": "default", "type": "github" } + }, + "systems_2": { + "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 8fa63cb3e..e9a634360 100644 --- a/flake.nix +++ b/flake.nix @@ -4,8 +4,8 @@ flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:nixos/nixpkgs/23.11"; - stable.url = "github:nixos/nixpkgs/23.11"; + nixpkgs.url = "github:nixos/nixpkgs/24.05"; + stable.url = "github:nixos/nixpkgs/24.05"; nixpkgs.follows = "opam-nix/nixpkgs"; prover_cvc4_1_8 = { @@ -13,8 +13,8 @@ flake = false; }; - prover_cvc5_1_0_5 = { - url = "github:cvc5/cvc5/cvc5-1.0.5"; + prover_cvc5_1_0_9 = { + url = "github:cvc5/cvc5/cvc5-1.0.9"; flake = false; }; @@ -40,7 +40,7 @@ }; query = devPackagesQuery // { - ocaml-base-compiler = "4.14.1"; + ocaml-base-compiler = "4.14.2"; }; scope = on.buildOpamProject' { } ./. query; @@ -54,9 +54,12 @@ ''; doNixSupport = false; }); + conf-pkg-config = prev.conf-pkg-config.overrideAttrs (oa: { + nativeBuildInputs = oa.nativeBuildInputs ++ [pkgs.pkg-config]; + }); }; - scope' = scope.overrideScope' overlay; + scope' = scope.overrideScope overlay; # Packages from devPackagesQuery devPackages = builtins.attrValues @@ -75,15 +78,16 @@ src = inputs."${"prover_" + pkg + "_" + builtins.replaceStrings ["."] ["_"] version}"; }); - mkAltErgo = version: (on.queryToScope { } (query // { alt-ergo = version; })).alt-ergo; + 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.5"; - altErgo = mkAltErgo "2.4.2"; + cvc5 = mkProverPackage "cvc5" "1.0.9"; + altErgo = mkAltErgo "2.4.3"; provers = pkgs.symlinkJoin { name = "provers"; @@ -101,9 +105,9 @@ devShells.default = pkgs.mkShell { inputsFrom = [ scope'.easycrypt ]; buildInputs = - devPackages - ++ [ scope'.why3 packages.provers ] - ++ (with pkgs.python3Packages; [ pyyaml ]); + devPackages + ++ [ scope'.why3 packages.provers ] + ++ (with pkgs.python3Packages; [ pyyaml ]); }; }); } diff --git a/scripts/docker/Dockerfile.build b/scripts/docker/Dockerfile.build index 81c259f9f..d3d9ec776 100644 --- a/scripts/docker/Dockerfile.build +++ b/scripts/docker/Dockerfile.build @@ -57,7 +57,7 @@ RUN \ rm -f cvc5 RUN \ - version=4.13.0 && glibc=2.35 && \ + version=4.13.4 && glibc=2.35 && \ wget -O z3.zip https://github.com/Z3Prover/z3/releases/download/z3-${version}/z3-${version}-x64-glibc-${glibc}.zip && \ unzip -j z3.zip z3-${version}-x64-glibc-${glibc}/bin/z3 && \ sudo install -m 0755 z3 /usr/local/bin/z3-${version} && \