Merge PR #12289: test-suite: fix bug causing unit tests to be skipped

Reviewed-by: herbelin

4 files changed, 18 insertions, 68 deletions

diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index e76614a0cf..305c6a627e 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -56,6 +56,7 @@ jobs:
     MACOSX_DEPLOYMENT_TARGET: '10.11'
 
   steps:
+
   - checkout: self
     fetchDepth: 10
 
@@ -97,6 +98,7 @@ jobs:
 
   - script: |
       eval $(opam env)
+      export OCAMLPATH=$(pwd):"$OCAMLPATH"
       make -j "$NJOBS" test-suite PRINT_LOGS=1
     displayName: 'Run Coq Test Suite'
 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index bbd31486fe..f0f838680e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -281,8 +281,8 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 
 # ML files from unit-test framework, not containing tests
-UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml)
-UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml)
+UNIT_SRCFILES:=$(shell find ./unit-tests/src -name '*.ml')
+UNIT_ALLMLFILES:=$(shell find ./unit-tests -name '*.ml')
 UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES))
 UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES))
 
@@ -312,11 +312,6 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \
 	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
-unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK)
-	$(SHOW) 'TEST      $<'
-	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \
-	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
-	$(HIDE)./$<.test
 
 #######################################################################
 # Other generic tests
diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml
deleted file mode 100644
index 3082acdf1f..0000000000
--- a/test-suite/unit-tests/ide/lex_tests.ml
+++ /dev/null
@@ -1,50 +0,0 @@
-open Utest
-
-let log_out_ch = open_log_out_ch __FILE__
-
-let lex s =
-  let n =
-    let last = String.length s - 1 in
-    if s.[last] = '.' then Some last else None in
-  let stop = ref None in
-  let f i _ = assert(!stop = None); stop := Some i in
-  begin try Coq_lex.delimit_sentences f s
-  with Coq_lex.Unterminated -> () end;
-  if n <> !stop then begin
-    let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in
-    Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop)
-  end;
-  n = !stop
-
-let i2s i = "test at line: " ^ string_of_int i
-
-let tests = [
-
-  mk_bool_test (i2s __LINE__) "no quotation" @@ lex
-  "foo.+1 bar."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation" @@ lex
-  "foo constr:(xxx)."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex
-  "foo constr:(xxx. yyy)."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex
-  "foo constr:((xxx. (foo.+1 ) \")\" yyy))."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex
-  "foo constr:[xxx. (foo.+1 ) \")\" yyy]."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex
-  "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex
-  "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex
-  "bar:{{ foo {{ hello. }} }}."
-  ;
-
-]
-
-let _ = run_tests __FILE__ log_out_ch tests
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index d0b8d21b69..60267cd859 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -76,11 +76,14 @@ let _ = add_test "tokenize_string/diff_mode in lexer" t
 
 open Pp
 
+let write_diffs_option s =
+  Goptions.set_string_option_value Proof_diffs.opt_name s
+
 (* example that was failing from #8922 *)
 let t () =
-  Proof_diffs.write_diffs_option "removed";
+  write_diffs_option "removed";
   ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1");
-  Proof_diffs.write_diffs_option "on"
+  write_diffs_option "on"
 let _ = add_test "shorten_diff_span failure from #8922" t
 
 (* note pp_to_string concatenates adjacent strings, could become one token,
@@ -181,7 +184,7 @@ let _ = if false then add_test "diff_pp/add_diff_tags token containing white spa
 
 let add_entries map idents rhs_pp =
   let make_entry() = { idents; rhs_pp; done_ = false } in
-  List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;;
+  List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents;;
 
 let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps
 let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps
@@ -194,11 +197,11 @@ let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (fl
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["a"]; ["b"]] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["a"] (str " : foo");
   add_entries o_hyp_map ["b"] (str " : bar car");
   let n_line_idents = [ ["b"]; ["a"]] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["b"] (str " : car");
   add_entries n_hyp_map ["a"] (str " : foo bar");
   let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ]));
@@ -224,11 +227,11 @@ let _ = add_test "diff_hyps simple diffs" t
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["a"]; ["c"; "d"]] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["a"] (str " : nat");
   add_entries o_hyp_map ["c"; "d"] (str " : int");
   let n_line_idents = [ ["a"; "b"]; ["d"]] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["a"; "b"] (str " : nat");
   add_entries n_hyp_map ["d"] (str " : int");
   let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ]));
@@ -264,12 +267,12 @@ DIFFS
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["a"]; ["b"]; ["c"]] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["a"] (str " : foo");
   add_entries o_hyp_map ["b"] (str " : bar");
   add_entries o_hyp_map ["c"] (str " : nat");
   let n_line_idents = [ ["b"; "a"; "c"] ] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat");
   let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))]));
                   flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))]));
@@ -302,10 +305,10 @@ DIFFS
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["b"; "a"; "c"] ] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat");
   let n_line_idents = [ ["a"]; ["b"]; ["c"]] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["a"] (str " : foo");
   add_entries n_hyp_map ["b"] (str " : bar");
   add_entries n_hyp_map ["c"] (str " : nat");