tmp

ejgallego · Jul 7, 2023 · 108fe57 · 108fe57
1 parent 1a6d5d7
commit 108fe57
Showing 1 changed file with 34 additions and 14 deletions.
diff --git a/coq/workspace.ml b/coq/workspace.ml
@@ -156,11 +156,12 @@ let pp_load_path fmt
   Format.fprintf fmt "Path %s ---> %s"
     (Names.DirPath.to_string coq_path)
     unix_path
-let pp_as fmt (d, dl) = Format.fprintf fmt "(%s, %a)"
-    d Format.(pp_print_list pp_print_string) dl
 
-let pp_ap fmt (dl, d) = Format.fprintf fmt "(%a, %s)"
-    Format.(pp_print_list pp_print_string) dl d
+let pp_as fmt (d, dl) =
+  Format.fprintf fmt "(%s, %a)" d Format.(pp_print_list pp_print_string) dl
+
+let pp_ap fmt (dl, d) =
+  Format.fprintf fmt "(%a, %s)" Format.(pp_print_list pp_print_string) dl d
 
 let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } =
   let require_msg =
@@ -182,20 +183,39 @@ let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } =
       \ - Modules [%s] will be loaded by default@\n\
       \ - %d Coq path directory bindings in scope; %d Coq plugin directory \
        bindings in scope@]"
-      kind coqlib require_msg n_vo n_ml in
+      kind coqlib require_msg n_vo n_ml
+  in
   let c11 = System.all_subdirs ~unix_path:coqlib in
   let c12 = System.all_subdirs ~unix_path:(Filename.concat coqlib "..") in
-  let c13 = System.all_subdirs ~unix_path:(Filename.(concat (concat coqlib "..") "..")) in
+  let c13 =
+    System.all_subdirs ~unix_path:Filename.(concat (concat coqlib "..") "..")
+  in
+  let c11' = System.all_subdirs ~unix_path:coqlib in
+  let c12' = System.all_subdirs ~unix_path:(coqlib ^ "/..") in
+  let c13' = System.all_subdirs ~unix_path:(coqlib ^ "/../..") in
   let c2 = Sys.readdir coqlib in
   let c3 = System.all_in_path c11 "Prelude.vo" in
-  let base = Format.asprintf "l1:%a@\nl2:%a@\nl3:%a@\n%a@\n%a@\n@\n%s"
-      Format.(pp_print_list pp_as) c11
-      Format.(pp_print_list pp_as) c12
-      Format.(pp_print_list pp_as) c13
-      Format.(pp_print_list pp_print_string) (Array.to_list c2)
-      Format.(pp_print_list pp_ap) c3
-      base in
-  ( base, extra )
+  let base =
+    Format.asprintf
+      "l1:%a@\nl2:%a@\nl3:%a@\nl1':%a@\nl2':%a@\nl3':%a@\n%a@\n%a@\n@\n%s"
+      Format.(pp_print_list pp_as)
+      c11
+      Format.(pp_print_list pp_as)
+      c12
+      Format.(pp_print_list pp_as)
+      c13
+      Format.(pp_print_list pp_as)
+      c11'
+      Format.(pp_print_list pp_as)
+      c12'
+      Format.(pp_print_list pp_as)
+      c13'
+      Format.(pp_print_list pp_print_string)
+      (Array.to_list c2)
+      Format.(pp_print_list pp_ap)
+      c3 base
+  in
+  (base, extra)
 
 (* Require a set of libraries *)
 let load_objs libs =