cafkafk/nixpkgs
cafkafk/nixpkgs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

coqPackages.serapi: patch to fix COQPATH issue

Browse source 
SerAPI was interpreting paths as relative to the Coq root.
This commit is contained in:
Théo Zimmermann 2021-08-19 12:47:58 +02:00 committed by Vincent Laporte
parent 7c97a26073
commit 170128a5a7
4 changed files with 111 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch Normal file
View file

@ -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 *)

33
pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch Normal file
View file

@ -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
(******************************************************************************)

29
pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch Normal file
View file

@ -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
(******************************************************************************)

15
pkgs/development/coq-modules/serapi/default.nix
View file

@ -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 [];
})