From d3babf24b7873f597ba43f4534a49657ccf47685 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Fri, 22 Mar 2024 08:27:34 +0100
Subject: =?UTF-8?q?compcert:=20make=20compatible=20with=20Coq=208.18?=
 =?UTF-8?q?=E2=80=938.19?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 pkgs/development/coq-modules/compcert/default.nix | 23 +++++++++++++++++++----
 pkgs/top-level/all-packages.nix                   |  2 +-
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index 68a839cc4e8b..769017d4e282 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -29,7 +29,7 @@ compcert = mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   defaultVersion =  with lib.versions; lib.switch coq.version [
-      { case = range "8.14" "8.17"; out = "3.13.1"; }
+      { case = range "8.14" "8.19"; out = "3.13.1"; }
       { case = isEq "8.13"        ; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
       { case = range "8.8" "8.11"; out = "3.8"; }
@@ -170,12 +170,27 @@ compcert.overrideAttrs (o:
           })
         ];
       }
-      { cases = [ (isEq "8.17") (isEq "3.13") ];
+      { cases = [ (range "8.17" "8.19") (isEq "3.13") ];
         out = [
           # Support for Coq 8.17.0 & Coq 8.17.1
           (fetchpatch {
-            url = "https://github.com/AbsInt/CompCert/commit/030a0fafe6a1a315bb13c5276e0af536e4f713ce.patch";
-            hash = "sha256-iRdmgYuun1wp6chRoDy99KKmFyvY79NGWzrltyQaW1o=";
+            url = "https://github.com/AbsInt/CompCert/commit/2e04d986bdae578186e40330842878559a550402.patch";
+            hash = "sha256-2ZRAjUUSScJI8ogWFTnukCUnJdLWGvyOPyfIVlHL4ig=";
+          })
+          # Support for Coq 8.18.0
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/28218c5663cba36c6078ca342335d4e55c412bd7.patch";
+            hash = "sha256-aAatUMO26oZwFYGh1BXYWxbTuyOgU8BAKMGDS5796hM=";
+          })
+          # MenhirLib update
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/9f3d7b6eb99377ad4689cd57563c484c57baa457.patch";
+            hash = "sha256-paofdSBxP/JFoBSiO1OI+mjKRI3UCanXRh/drzYt93E=";
+          })
+          # Support for Coq 8.19.0 & Coq 8.19.1
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/a2e4ed62fc558d565366845f9d135bd7db5e23c4.patch";
+            hash = "sha256-ufk0bokuayLfkSvK3cK4E9iXU5eZpp9d/ETSa/zCfMg=";
           })
         ];
       }
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 4c3c4b570d99..46cb413f7c58 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -15542,7 +15542,7 @@ with pkgs;
     ocamlPackages = ocaml-ng.ocamlPackages_4_14;
   };
 
-  inherit (coqPackages_8_17) compcert;
+  inherit (coqPackages) compcert;
 
   computecpp-unwrapped = callPackage ../development/compilers/computecpp { };
   computecpp = wrapCCWith rec {
-- 
cgit v1.2.3