guix/gnu/packages/patches/coq-fix-envvars.patch
Julien Lepiller 5179f4525d
gnu: coq: Update to 8.15.0.
* 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.
2022-02-11 10:32:56 +01:00

54 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