From 438d6f7cc730eda8f44af4e97be3b610bd4791e9 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 15 Jul 2024 06:06:59 +0200
Subject: [PATCH] =?UTF-8?q?hol=5Flight:=202024-05-10=20=E2=86=92=202024-07?=
 =?UTF-8?q?-07?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ...004-Fix-compilation-with-camlp5-7.11.patch | 66 +++++++++++++++++++
 .../science/logic/hol_light/default.nix       | 15 ++---
 2 files changed, 71 insertions(+), 10 deletions(-)
 create mode 100644 pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch

diff --git a/pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch b/pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch
new file mode 100644
index 000000000000..2fc2b1544c44
--- /dev/null
+++ b/pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch
@@ -0,0 +1,66 @@
+From: Stephane Glondu <steph@glondu.net>
+Date: Wed, 12 Feb 2020 05:42:32 +0100
+Subject: Fix compilation with camlp5 7.11
+
+---
+ pa_j_4.xx_7.xx.ml | 17 +++++++++++------
+ 1 file changed, 11 insertions(+), 6 deletions(-)
+
+diff --git a/pa_j_4.xx_7.xx.ml b/pa_j_4.xx_7.xx.ml
+index 4f7ed60..e834058 100755
+--- a/pa_j/pa_j_4.xx_7.xx.ml
++++ b/pa_j/pa_j_4.xx_7.xx.ml
+@@ -410,9 +410,10 @@ and reloc_module_type floc sh =
+     | MtApp loc x1 x2 →
+         let loc = floc loc in
+         MtApp loc (self x1) (self x2)
+-    | MtFun loc x1 x2 x3 →
++    | MtFun loc x x3 →
+         let loc = floc loc in
+-        MtFun loc x1 (self x2) (self x3)
++        let x = vala_map (option_map (fun (x1, x2) -> (x1, self x2))) x in
++        MtFun loc x (self x3)
+     | MtLid loc x1 →
+         let loc = floc loc in
+         MtLid loc x1
+@@ -507,9 +508,10 @@ and reloc_module_expr floc sh =
+     | MeApp loc x1 x2 →
+         let loc = floc loc in
+         MeApp loc (self x1) (self x2)
+-    | MeFun loc x1 x2 x3 →
++    | MeFun loc x x3 →
+         let loc = floc loc in
+-        MeFun loc x1 (reloc_module_type floc sh x2) (self x3)
++        let x = vala_map (option_map (fun (x1, x2) -> (x1, reloc_module_type floc sh x2))) x in
++        MeFun loc x (self x3)
+     | MeStr loc x1 →
+         let loc = floc loc in
+         MeStr loc (vala_map (List.map (reloc_str_item floc sh)) x1)
+@@ -2007,7 +2009,7 @@ EXTEND
+       | -> <:vala< [] >> ] ]
+   ;
+   mod_binding:
+-    [ [ i = V UIDENT; me = mod_fun_binding -> (i, me) ] ]
++    [ [ i = V uidopt "uidopt"; me = mod_fun_binding -> (i, me) ] ]
+   ;
+   mod_fun_binding:
+     [ RIGHTA
+@@ -2070,7 +2072,7 @@ EXTEND
+           <:sig_item< value $lid:i$ : $t$ >> ] ]
+   ;
+   mod_decl_binding:
+-    [ [ i = V UIDENT; mt = module_declaration -> (i, mt) ] ]
++    [ [ i = V uidopt "uidopt"; mt = module_declaration -> (i, mt) ] ]
+   ;
+   module_declaration:
+     [ RIGHTA
+@@ -2092,6 +2094,9 @@ EXTEND
+       | "module"; i = V mod_ident ""; ":="; me = module_expr ->
+           <:with_constr< module $_:i$ := $me$ >> ] ]
+   ;
++  uidopt:
++    [ [ m = V UIDENT -> Some m ] ]
++  ;
+   (* Core expressions *)
+   expr:
+     [ "top" RIGHTA
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index 0e3dee4b0c0a..59389f11a282 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, findlib, num, zarith, camlp5, camlp-streams }:
+{ lib, stdenv, runtimeShell, fetchFromGitHub, ocaml, findlib, num, zarith, camlp5, camlp-streams }:
 
 let
   use_zarith = lib.versionAtLeast ocaml.version "4.14";
@@ -28,21 +28,16 @@ in
 
 stdenv.mkDerivation {
   pname = "hol_light";
-  version = "unstable-2024-05-10";
+  version = "unstable-2024-07-07";
 
   src = fetchFromGitHub {
     owner = "jrh13";
     repo = "hol-light";
-    rev = "d8366986e22555c4e4c8ff49667d646d15c35f14";
-    hash = "sha256-dN9X7yQlFof759I5lxxL4DxDe8V3XAhCRaryO9NabY4=";
+    rev = "16b184e30e7e3fe9add7d1ee93242323ed2e1726";
+    hash = "sha256-V0OtsmX5pa+CH3ZXmNG3juXwXZ5+A0k13eMCAfaRziQ=";
   };
 
-  patches = [
-    (fetchpatch {
-      url = "https://salsa.debian.org/ocaml-team/hol-light/-/raw/master/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch";
-      sha256 = "180qmxbrk3vb1ix7j77hcs8vsar91rs11s5mm8ir5352rz7ylicr";
-    })
-  ];
+  patches = [ ./0004-Fix-compilation-with-camlp5-7.11.patch ];
 
   strictDeps = true;