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

ion>
<option value='author'>author</option>
<option value='committer'>committer</option>
<option value='range'>range</option>
</select>
<input class='txt' type='search' size='10' name='q' value=''/>
<input type='submit' value='search'/>
</form>
</td></tr></table>
<div class='path'>path: <a href='/guix/log/?id=acb08304c862d65679086a9f160240bfd598289d&amp;showmsg=1'>root</a>/<a href='/guix/log/tests?id=acb08304c862d65679086a9f160240bfd598289d&amp;showmsg=1'>tests</a>/<a href='/guix/log/tests/guix-pack.sh?id=acb08304c862d65679086a9f160240bfd598289d&amp;showmsg=1'>guix-pack.sh</a></div><div class='content'><table class='list nowrap'><tr class='nohover'><th class='left'>Age</th><th class='left'>Commit message (<a href='/guix/log/tests/guix-pack.sh?id=acb08304c862d65679086a9f160240bfd598289d'>Collapse</a>)</th><th class='left'>Author</th></tr>
<tr class='logheader'><td><span title='2022-05-25 09:28:43 +0200'>2022-05-25</span></td><td class='logsubject'><a href='/guix/commit/tests/guix-pack.sh?id=d276a7dd6162d101b7790cc8ea902abfec1eafcb'>tests: Fix wrong target triplets.</a></td><td>Josselin Poiret</td></tr>
<tr class='nohover-highlight'><td/><td colspan='3' class='logmsg'>
* tests/gexp.scm (ungexp + ungexp-native,
input list + ungexp-native,
input list splicing + ungexp-native-splicing,
gexp list splicinng + ungexp-splicing,
gexp-&gt;derivation, cross-compilation,
gexp-&gt;derivation, ungexp-native,
gexp-&gt;derivation, ungexp + ungexp-native,
gexp-&gt;derivation, ungexp-native + composed gexps): Change
mips64el-linux to mips64el-linux-gnu.
* tests/guix-pack.sh: Change arm-unknown-linux-gnueabihf to
arm-linux-gnueabihf.

Signed-off-by: Mathieu Othacehe &lt;othacehe@gnu.org&gt;


</td></tr>
<tr class='logheader'><td><span title='2022-02-18 14:14:38 +0100'>2022-02-18</span></td><td class='logsubject'><a href='/guix/commit/tests/guix-pack.sh?id=5a57313918a5c1bd5cf8238c2dcae64a03523952'>profiles: 'profile-derivation' rejects unsupported packages.</a></td><td>Ludovic Courtès</td></tr>
<tr class='nohover-highlight'><td/><td colspan='3' class='logmsg'>
Previously user-facing commands would happily start building packages
even if they do not support that system.  With this change, all the
user-facing commands reject unsupported packages without going further.

* guix/profiles.scm (profile-derivation): Add #:allow-unsupported-packages?.
Define 'check-supported-packages' and honor #:allow-unsupported-packages?.
* tests/guix-pack.sh, tests/guix-package.sh, tests/guix-shell.sh: Ensure
that unsupported packages are rejected.
* tests/guix-system.sh: Pass "--system=armhf-linux" when attempting to
build gnu/system/examples/asus-c201.tmpl.


</td></tr>
<tr class='logheader'><td><span title='2020-09-28 21:06:36 -0500'>2020-09-28</span></td><td class='logsubject'><a href='/guix/commit/tests/guix-pack.sh?id=d8934360d2453a403b5433e71d09188e4ed23b57'>tests: Simplify shell exit status negation;</a></td><td>Eric Bavier</td></tr>
<tr class='nohover-highlight'><td/><td colspan='3' class='logmsg'>
* tests/guix-archive.sh, tests/guix-build-branch.sh, tests/guix-build.sh,
tests/guix-daemon.sh, tests/guix-download.sh, tests/guix-environment.sh,
tests/guix-gc.sh, tests/guix-git-authenticate.sh, tests/guix-graph.sh,
tests/guix-hash.sh, tests/guix-lint.sh, tests/guix-pack-relocatable.sh,
tests/guix-pack.sh, tests/guix-package-aliases.sh, tests/guix-package-net.sh,
tests/guix-package.sh: Use the shell '!' keyword to negate command exit status
in place of 'if ...; then false; else true; fi'


</td></tr>