* gnu/packages/coq.scm (coq): Update to 8.15.0. (coq-equations): Update to 1.3-8.15. * gnu/packages/patches/coq-fix-envvars.patch: Adapt to new version.
		
			
				
	
	
		
			53 lines
		
	
	
	
		
			1.8 KiB
		
	
	
	
		
			Diff
		
	
	
	
	
	
			
		
		
	
	
			53 lines
		
	
	
	
		
			1.8 KiB
		
	
	
	
		
			Diff
		
	
	
	
	
	
From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001
 | 
						|
From: Julien Lepiller <julien@lepiller.eu>
 | 
						|
Date: Thu, 10 Feb 2022 16:44:10 +0100
 | 
						|
Subject: [PATCH] Fix environment variable usage.
 | 
						|
 | 
						|
---
 | 
						|
 boot/env.ml | 26 +++++++++++++++++++-------
 | 
						|
 1 file changed, 19 insertions(+), 7 deletions(-)
 | 
						|
 | 
						|
diff --git a/boot/env.ml b/boot/env.ml
 | 
						|
index e8521e7..d834a3a 100644
 | 
						|
--- a/boot/env.ml
 | 
						|
+++ b/boot/env.ml
 | 
						|
@@ -32,17 +32,29 @@ let fail_msg =
 | 
						|
 
 | 
						|
 let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1
 | 
						|
 
 | 
						|
+let path_to_list p =
 | 
						|
+  let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
 | 
						|
+    String.split_on_char sep p
 | 
						|
+
 | 
						|
 (* This code needs to be refactored, for now it is just what used to be in envvars  *)
 | 
						|
 let guess_coqlib () =
 | 
						|
   Util.getenv_else "COQLIB" (fun () ->
 | 
						|
   let prelude = "theories/Init/Prelude.vo" in
 | 
						|
-  Util.check_file_else
 | 
						|
-    ~dir:Coq_config.coqlibsuffix
 | 
						|
-    ~file:prelude
 | 
						|
-    (fun () ->
 | 
						|
-      if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
 | 
						|
-      then Coq_config.coqlib
 | 
						|
-      else fail ()))
 | 
						|
+  let coqlibpath = Util.getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in
 | 
						|
+  let paths = path_to_list coqlibpath in
 | 
						|
+  let valid_paths =
 | 
						|
+    List.filter
 | 
						|
+      (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "")
 | 
						|
+      paths in
 | 
						|
+  match valid_paths with
 | 
						|
+  | [] ->
 | 
						|
+    if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
 | 
						|
+    then Coq_config.coqlib
 | 
						|
+    else
 | 
						|
+      fail "cannot guess a path for Coq libraries; please use -coqlib option \
 | 
						|
+            or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \
 | 
						|
+            If you intend to use Coq without a standard library, the -boot -noinit options must be used."
 | 
						|
+  | p::_ -> p)
 | 
						|
 
 | 
						|
 (* Build layout uses coqlib = coqcorelib *)
 | 
						|
 let guess_coqcorelib lib =
 | 
						|
-- 
 | 
						|
2.34.0
 | 
						|
 |