coqPackages.serapi: patch to fix COQPATH issue

SerAPI was interpreting paths as relative to the Coq root.

4 files changed, 111 insertions, 0 deletions

diff --git a/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch b/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch
new file mode 100644
index 00000000000..c3434f697ff
--- /dev/null
+++ b/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch
@@ -0,0 +1,34 @@
+diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
+index 17cbb98..1fd85a0 100644
+--- a/serapi/serapi_paths.ml
++++ b/serapi/serapi_paths.ml
+@@ -23,10 +23,10 @@
+ let coq_loadpath_default ~implicit ~coq_path =
+   let open Mltop in
+   let mk_path prefix = coq_path ^ "/" ^ prefix in
+-  let mk_lp ~ml ~root ~dir ~implicit =
++  let mk_lp ~ml ~root ~dir ~implicit ~absolute =
+     { recursive = true;
+       path_spec = VoPath {
+-          unix_path = mk_path dir;
++          unix_path = if absolute then dir else mk_path dir;
+           coq_path  = root;
+           has_ml    = ml;
+           implicit;
+@@ -35,10 +35,12 @@ let coq_loadpath_default ~implicit ~coq_path =
+   (* in 8.8 we can use Libnames.default_* *)
+   let coq_root     = Names.DirPath.make [Libnames.coq_root] in
+   let default_root = Libnames.default_root_prefix in
+-  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins";
+-   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories";
+-   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib";
+-  ]
++  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins" ~absolute:false;
++   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories" ~absolute:false;
++   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
++  ] @
++  List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir ~absolute:true)
++    Envars.coqpath
+ 
+ (******************************************************************************)
+ (* Generate a module name given a file                                        *)
diff --git a/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch b/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch
new file mode 100644
index 00000000000..c10bf5c3142
--- /dev/null
+++ b/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch
@@ -0,0 +1,33 @@
+diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
+index a9c5074..eed92e3 100644
+--- a/serapi/serapi_paths.ml
++++ b/serapi/serapi_paths.ml
+@@ -23,10 +23,10 @@
+ let coq_loadpath_default ~implicit ~coq_path =
+   let open Loadpath in
+   let mk_path prefix = coq_path ^ "/" ^ prefix in
+-  let mk_lp ~ml ~root ~dir ~implicit =
++  let mk_lp ~ml ~root ~dir ~implicit ~absolute =
+     { recursive = true;
+       path_spec = VoPath {
+-          unix_path = mk_path dir;
++          unix_path = if absolute then dir else mk_path dir;
+           coq_path  = root;
+           has_ml    = ml;
+           implicit;
+@@ -35,11 +35,11 @@ let coq_loadpath_default ~implicit ~coq_path =
+   (* in 8.8 we can use Libnames.default_* *)
+   let coq_root     = Names.DirPath.make [Libnames.coq_root] in
+   let default_root = Libnames.default_root_prefix in
+-  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins";
+-   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories";
+-   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib";
++  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins" ~absolute:false;
++   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories" ~absolute:false;
++   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
+   ] @
+-  List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir)
++  List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir ~absolute:true)
+     Envars.coqpath
+ 
+ (******************************************************************************)
diff --git a/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch b/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch
new file mode 100644
index 00000000000..9eb70b670a1
--- /dev/null
+++ b/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch
@@ -0,0 +1,29 @@
+diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
+index b71fa60..0bec8c2 100644
+--- a/serapi/serapi_paths.ml
++++ b/serapi/serapi_paths.ml
+@@ -24,8 +24,8 @@ let coq_loadpath_default ~implicit ~coq_path =
+   let open Loadpath in
+   let mk_path prefix = coq_path ^ "/" ^ prefix in
+   (* let mk_ml = () in *)
+-  let mk_vo ~has_ml ~coq_path ~dir ~implicit =
+-    { unix_path = mk_path dir
++  let mk_vo ~has_ml ~coq_path ~dir ~implicit ~absolute =
++    { unix_path = if absolute then dir else mk_path dir
+     ; coq_path
+     ; has_ml
+     ; recursive = true
+@@ -40,10 +40,10 @@ let coq_loadpath_default ~implicit ~coq_path =
+     List.map fst plugins_dirs
+   in
+   ml_paths ,
+-  [ mk_vo ~has_ml:false ~coq_path:coq_root     ~implicit       ~dir:"theories"
+-  ; mk_vo ~has_ml:true  ~coq_path:default_root ~implicit:false ~dir:"user-contrib";
++  [ mk_vo ~has_ml:false ~coq_path:coq_root     ~implicit       ~dir:"theories" ~absolute:false
++  ; mk_vo ~has_ml:true  ~coq_path:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
+   ] @
+-  List.map (fun dir -> mk_vo ~has_ml:true ~coq_path:default_root ~implicit:false ~dir)
++  List.map (fun dir -> mk_vo ~has_ml:true ~coq_path:default_root ~implicit:false ~dir ~absolute:true)
+     Envars.coqpath
+ 
+ (******************************************************************************)
diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix
index 1f6e995703c..01954dff655 100644
--- a/pkgs/development/coq-modules/serapi/default.nix
+++ b/pkgs/development/coq-modules/serapi/default.nix
@@ -75,4 +75,19 @@ in
         }.tbz";
     sha256 = release."${version}".sha256;
   };
+
+  patches =
+    if version == "8.10.0+0.7.2"
+    then [
+      ./8.10.0+0.7.2.patch
+    ]
+    else if version == "8.11.0+0.11.1"
+    then [
+      ./8.11.0+0.11.1.patch
+    ]
+    else if version == "8.12.0+0.12.1" || version == "8.13.0+0.13.0"
+    then [
+      ./8.12.0+0.12.1.patch
+    ]
+    else [];
 })