From 50d9adfa8aad8ea8144ce9fb907faec0faa350f5 Mon Sep 17 00:00:00 2001
From: "Aaron L. Zeng" <me@bcc32.com>
Date: Wed, 20 Jul 2022 00:15:30 -0400
Subject: [PATCH] Fix coqPackages.serapi version 8.15 for
 ocamlPackages.janeStreet version 0.15

This is a follow-up to #166033 adding a patch for coqPackages.serapi
so that it builds successfully with the new Jane Street OCaml
packages.  I did not upstream this patch because
upstream (coq-serapi-v8.16) already includes commits mentioning Jane
Street 0.15 compatibility with a similar patch.
---
 .../coq-modules/serapi/default.nix            |  6 +-
 .../coq-modules/serapi/janestreet-0.15.patch  | 80 +++++++++++++++++++
 2 files changed, 85 insertions(+), 1 deletion(-)
 create mode 100644 pkgs/development/coq-modules/serapi/janestreet-0.15.patch

diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix
index b3bff95b5eaf..65643fc2ea69 100644
--- a/pkgs/development/coq-modules/serapi/default.nix
+++ b/pkgs/development/coq-modules/serapi/default.nix
@@ -27,6 +27,8 @@ in
 
   useDune2 = true;
 
+  patches = [ ./janestreet-0.15.patch ];
+
   propagatedBuildInputs =
     with coq.ocamlPackages; [
       cmdliner
@@ -76,5 +78,7 @@ in
     then [
       ./8.12.0+0.12.1.patch
     ]
-    else [];
+    else [
+      ./janestreet-0.15.patch
+    ];
 })
diff --git a/pkgs/development/coq-modules/serapi/janestreet-0.15.patch b/pkgs/development/coq-modules/serapi/janestreet-0.15.patch
new file mode 100644
index 000000000000..7879c667d374
--- /dev/null
+++ b/pkgs/development/coq-modules/serapi/janestreet-0.15.patch
@@ -0,0 +1,80 @@
+diff --git a/serlib/ser_constr.ml b/serlib/ser_constr.ml
+index 69b2077..47fa06a 100644
+--- a/serlib/ser_constr.ml
++++ b/serlib/ser_constr.ml
+@@ -99,11 +99,13 @@ type 'constr pcase_branch =
+ let map_pcase_branch f (bi, c) = (bi, f c)
+ 
+ type 'types pcase_return =
+-  [%import: 'constr Constr.pcase_return]
++  [%import: 'types Constr.pcase_return]
+   [@@deriving sexp,yojson]
+ 
+ let map_pcase_return f (bi, c) = (bi, f c)
+ 
++type 'a identity = 'a [@@deriving sexp,yojson]
++
+ type _constr =
+   | Rel       of int
+   | Var       of Names.Id.t
+@@ -126,7 +128,7 @@ type _constr =
+   | Float     of Float64.t
+   | Array     of Univ.Instance.t * _constr array * _constr * _types
+ [@@deriving sexp,yojson]
+-and _types = _constr
++and _types = _constr identity
+ [@@deriving sexp,yojson]
+ 
+ let rec _constr_put (c : constr) : _constr =
+diff --git a/serlib/ser_locus.ml b/serlib/ser_locus.ml
+index 1f74ebc..cdcfc99 100644
+--- a/serlib/ser_locus.ml
++++ b/serlib/ser_locus.ml
+@@ -57,7 +57,7 @@ type clause_atom =
+   [%import: Locus.clause_atom]
+   [@@deriving sexp]
+ 
+-type concrete_clause =
++type 'id concrete_clause =
+   [%import: 'id Locus.clause_expr]
+   [@@deriving sexp]
+ 
+@@ -65,7 +65,7 @@ type hyp_location =
+   [%import: Locus.clause_atom]
+   [@@deriving sexp]
+ 
+-type goal_location =
++type 'id goal_location =
+   [%import: 'id Locus.clause_expr]
+   [@@deriving sexp]
+ 
+@@ -73,7 +73,7 @@ type simple_clause =
+   [%import: Locus.clause_atom]
+   [@@deriving sexp]
+ 
+-type 'a or_like_first =
++type 'id or_like_first =
+   [%import: 'id Locus.clause_expr]
+   [@@deriving sexp]
+ 
+diff --git a/serlib/ser_stdlib.ml b/serlib/ser_stdlib.ml
+index fdb1720..3907548 100644
+--- a/serlib/ser_stdlib.ml
++++ b/serlib/ser_stdlib.ml
+@@ -16,6 +16,16 @@
+ open Sexplib.Conv
+ 
+ type nonrec 'a ref = 'a ref
++let ref = ref
++let ( ! ) = ( ! )
++let ( := ) = ( := )
++
++module Option = struct
++  type 'a t = 'a option =
++    | None
++    | Some of 'a
++  [@@deriving sexp]
++end
+ 
+ let ref_of_sexp = ref_of_sexp
+ let sexp_of_ref = sexp_of_ref