From 4a0bc9e3de7a19439f45ba59405015033607ed68 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 16 Jun 2020 02:09:36 +0900
Subject: Fix bugs in hierarchy.ml

- pass `Unix.environment ()` to `coqtop` to preserve the parent process
  environment,
- check the exit status of `coqtop` and report an error if it is wrong,
- do not rely on `ssrfun.id` in the `check_join` tactic, and
- improve the error message for missing unification hints.
---
 etc/utils/hierarchy.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/etc/utils/hierarchy.ml b/etc/utils/hierarchy.ml
index 1d25993..f764e9a 100644
--- a/etc/utils/hierarchy.ml
+++ b/etc/utils/hierarchy.ml
@@ -161,8 +161,8 @@ Tactic Notation "check_join"
   let T1 := open_constr:(_ : t1) in
   let T2 := open_constr:(_ : t2) in
   match tt with
-    | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
-    | _ => fail "There is no join of" t1 "and" t2
+    | _ => unify ((fun x : t1 => x : Type) T1) ((fun x : t2 => x : Type) T2)
+    | _ => fail "There is no join of" t1 "and" t2 "but is expected to be" tjoin
   end;
   let Tjoin :=
     lazymatch T1 with
@@ -239,7 +239,7 @@ let () =
          String.concat " "
            (List.map (fun (path, log) -> Printf.sprintf "-R %S %S" path log)
               !opt_libmaps))
-        [||]
+        (Unix.environment ())
     in
     Printf.fprintf coqtop_in {|
 Set Printing Width 4611686018427387903.
@@ -251,8 +251,11 @@ Redirect %S Print Graph.
       (List.hd (String.split_on_char '.' tmp_canonicals))
       (List.hd (String.split_on_char '.' tmp_coercions));
     close_out coqtop_in;
-    try while true do ignore (input_line coqtop_out) done
-      with End_of_file -> ignore (Unix.close_process_full coqtop_ch)
+    try
+      while true do ignore (input_line coqtop_out) done
+    with End_of_file ->
+      if Unix.close_process_full coqtop_ch <> WEXITED 0 then
+        failwith "Failed to invoke coqtop."
   end;
   (* Parsing *)
   let canonicals = parse_canonicals tmp_canonicals in
-- 
cgit v1.2.3


From 36613c83d65aa821b01a9fac38c479af65ef3589 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 16 Jun 2020 02:11:03 +0900
Subject: Fix some Makefile issues and rename `hierarchy_test.v` to
 `test_hierarchy_all.v`

---
 mathcomp/Make.test-suite |  2 +-
 mathcomp/Makefile.common | 10 ++++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
index 2be741b..0b51909 100644
--- a/mathcomp/Make.test-suite
+++ b/mathcomp/Make.test-suite
@@ -1,4 +1,4 @@
-test_suite/hierarchy_test.v
+test_suite/test_hierarchy_all.v
 test_suite/test_ssrAC.v
 test_suite/test_guard.v
 
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index 857ddef..b6b71ea 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -56,11 +56,10 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile
 
 # Test suite ---------------------------------------------------------
 
-test_suite/hierarchy_test.v: build
-	mkdir -p test_suite
-	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/hierarchy_test.v
+test_suite/test_hierarchy_all.v: build
+	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v
 
-Makefile.test-suite.coq: test_suite/hierarchy_test.v
+Makefile.test-suite.coq: test_suite/test_hierarchy_all.v
 	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq
 
 # Global config, build, clean and distclean --------------------------
@@ -128,6 +127,9 @@ endif
 %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
 
+test_suite/%.vo: __always__ Makefile.test-suite.coq
+	+$(COQMAKE_TESTSUITE) $@
+
 doc: __always__ Makefile.coq
 	mkdir -p _build_doc/
 	cp -r $(COQFILES) -t _build_doc/ --parents
-- 
cgit v1.2.3