Service commit (docker / nix / dune)

 - bump dune to 3.13 (needed for passing the --explain flag to menhir)
 - bump all provers subsubminor (in nix & Docker)
 - bump nix to 24.05 & fix compilation issues
 - revert OCaml to 4.14.2 in Docker

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))

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"}

flake.nix

@@ -4,17 +4,17 @@
 
     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 = {
       url = "github:CVC4/CVC4-archived/1.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 ]);
         };
       });
 }

scripts/docker/Dockerfile.base

@@ -28,7 +28,7 @@ WORKDIR /home/$user
 
 ENV OPAMYES=true OPAMVERBOSE=0 OPAMJOBS=4
 
-ARG OCAML_VERSION=5.2.0
+ARG OCAML_VERSION=4.14.2
 
 RUN \
 	opam init --disable-sandboxing --compiler=ocaml-base-compiler.${OCAML_VERSION}

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} && \