nix: repair flake for Nix 2.35 / macOS 26, take provers from nixpkgs

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,
  re-pinning opam-repository to the previous revision so the OCaml
  package set (4.14.2, why3 1.8.0) is unchanged.
- 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.
- 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.

Author: strub

.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 }}'

flake.lock

@@ -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:
@@ -57,6 +42,9 @@
           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];
+          });
         };
 
         scope' = scope.overrideScope overlay;
@@ -71,27 +59,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";
+          z3 = pkgs.z3;
+          cvc5 = pkgs.cvc5;
           altErgo = mkAltErgo "2.4.3";
 
           provers = pkgs.symlinkJoin {
             name = "provers";
-            paths = [ altErgo z3 cvc4 cvc5 ];
+            paths = [ altErgo z3 cvc5 ];
           };
 
           with_provers = pkgs.symlinkJoin {