From ffdae3c26f7f962237b25d63ba3f37ca62bfeda8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 1 Oct 2026 07:09:36 +0200
Subject: [PATCH] =?UTF-8?q?compcert:=203.17=20=E2=86=92=203.18?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

rocqPackages.VST: 2.16 → 2.17
---
 pkgs/development/rocq-modules/VST/default.nix     |  2 ++
 .../development/rocq-modules/compcert/default.nix | 15 +++++++++++++++
 pkgs/top-level/all-packages.nix                   |  2 +-
 pkgs/top-level/coq-packages.nix                   |  4 ++++
 pkgs/top-level/rocq-packages.nix                  |  4 ++++
 5 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/pkgs/development/rocq-modules/VST/default.nix b/pkgs/development/rocq-modules/VST/default.nix
index f8e0067d591c..2da9d9128ed6 100644
--- a/pkgs/development/rocq-modules/VST/default.nix
+++ b/pkgs/development/rocq-modules/VST/default.nix
@@ -38,6 +38,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.coq-version [
+      (case (range "9.1" "9.2") "2.17")
       (case (range "9.0" "9.1") "2.16")
       (case (range "8.19" "8.20") "2.15")
       (case (range "8.15" "8.19") "2.14")
@@ -46,6 +47,7 @@ mkCoqDerivation {
       (case (range "8.13" "8.15") "2.9")
       (case (range "8.12" "8.13") "2.8")
     ] null;
+  release."2.17".hash = "sha256-iDrX3uA6yOilwtg/9hIVx7e9U18pA2h5TXBh0bvBQkY=";
   release."2.16".hash = "sha256-/IlFLiojtuENHE9d+j55Z2rYw5HUkltwVim75w/UFVE=";
   release."2.15".hash = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";
   release."2.14".hash = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
diff --git a/pkgs/development/rocq-modules/compcert/default.nix b/pkgs/development/rocq-modules/compcert/default.nix
index 33bcd8bc337a..eb0ffd2a1051 100644
--- a/pkgs/development/rocq-modules/compcert/default.nix
+++ b/pkgs/development/rocq-modules/compcert/default.nix
@@ -46,6 +46,7 @@ let
       in
       with lib.versions;
       lib.switch coq.version [
+        (case (range "8.15" "9.2") "3.18")
         (case (range "8.15" "9.1") "3.17")
         (case (range "8.14" "8.20") "3.15")
         (case (isEq "8.13") "3.10")
@@ -65,6 +66,7 @@ let
       "3.15".hash = "sha256-QFTueGZd0hAWUj+c5GZL/AyNpfN4FuJiIzCICmwRXJ8=";
       "3.16".hash = "sha256-Ep8bcSFs3Cu+lV5qgo89JJU2vh4TTq66Or0c4evo3gM=";
       "3.17".hash = "sha256-RRc39FUe2sHQdO/ybwA3B7o31qfxcUkgah6I20i0ElE=";
+      "3.18".hash = "sha256-WadkhdtAgh+Tz8RxHT7NEV8RMeBBXxzJ1pLQPs94vfo=";
     };
 
     strictDeps = true;
@@ -333,6 +335,19 @@ let
               })
             ];
           }
+          {
+            cases = [
+              (_: true)
+              (isEq "3.18")
+            ];
+            out = [
+              # Fix version number
+              (fetchpatch {
+                url = "https://github.com/AbsInt/CompCert/commit/8135de0cc006f094e4a96aff9bb76cf716c9065a.patch";
+                hash = "sha256-vqbS7rMjO2+vrBhvG+JGCHpsGZyrBoAYS+JOaXdcnMg=";
+              })
+            ];
+          }
         ]
         [ ];
   });
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index d625247bf874..9f76b211981d 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -3128,7 +3128,7 @@ with pkgs;
     ocamlPackages = ocaml-ng.ocamlPackages_4_14;
   };
 
-  inherit (coqPackages_9_0) compcert;
+  inherit (coqPackages_9_2) compcert;
 
   corretto11 = javaPackages.compiler.corretto11;
   corretto17 = javaPackages.compiler.corretto17;
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 5bf2eb0ca15c..4657ec7e7a5c 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -263,6 +263,10 @@ let
             version =
               with lib.versions;
               lib.switch self.coq.version [
+                {
+                  case = range "8.19" "9.0";
+                  out = "3.17";
+                }
                 {
                   case = range "8.15" "8.18";
                   out = "3.13.1";
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index 8a8fd3fcaf55..78af819bd3a0 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -259,6 +259,10 @@ let
             version =
               with lib.versions;
               lib.switch self.coq.version [
+                {
+                  case = range "8.19" "9.0";
+                  out = "3.17";
+                }
                 {
                   case = range "8.15" "8.18";
                   out = "3.13.1";