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