Merge pull request coq-community#33 from JasonGross/coq-v8.7

Coq v8.7

.gitignore

@@ -26,6 +26,7 @@ coqthmdep
 dpd2dot
 dpdusage
 Make_coq
+CoqMakefile.conf
 dpd_lex.ml
 dpd_parse.ml
 dpd_parse.mli

.travis.yml

@@ -12,14 +12,12 @@ install:
 - opam init -y
 - eval $(opam config env)
 - opam config var root
+- opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev || true
 - opam install -y ocamlfind ocamlgraph
-- travis_wait opam install -y coq
+- travis_wait opam install -y coq.8.7.dev
 - opam list
 script:
 - autoconf
 - ./configure
-- make
-- make tests # we execute `make tests` twice; first for the return code, then for the output log
-- make tests | tee tmp.log
-- if grep DIFFERENCES tmp.log ; then for i in $(grep DIFFERENCES tmp.log | grep -o 'diff .*' | sed s'/diff //g' | sed s'/ /~/g'); do i="$(echo "$i" | sed s'/~/ /g')"; echo diff $i; diff $i; done ; fi
-- if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi
+- make || exit $?
+- make test-suite

Makefile.in

@@ -152,6 +152,20 @@ DISTRIBUTED+=$(TESTS_SRC) $(TESTS_ORACLE)
 .PHONY: tests test
 tests test : $(TESTS_OK)
 
+.PHONY: test-suite
+test-suite:
+	rm -f tests.ok
+	($(MAKE) tests && touch tests.ok) | tee tmp.log
+	if grep DIFFERENCES tmp.log >/dev/null 2>&1 ; then \
+		for i in $$(grep DIFFERENCES tmp.log | grep -o 'diff .*' | sed s'/diff //g' | sed s'/ /~/g'); do \
+			i="$$(echo "$$i" | sed s'/~/ /g')"; \
+			echo diff $$i; \
+			diff $$i; \
+		done ; \
+	fi
+	if grep DIFFERENCES tmp.log >/dev/null 2>&1 ; then false ; else true ; fi
+	rm tests.ok
+
 $(TESTDIR)/%.dpdusage.log: $(TESTDIR)/%.dpd $(DPDUSAGE)
 	$(DPDUSAGE) $< > $@
 

configure.ac

@@ -30,7 +30,7 @@ if test "$OCAMLC" = no ; then
 fi
 
 AC_MSG_CHECKING(ocamlc version)
-OCAMLVERSION=$($OCAMLC --version)
+OCAMLVERSION=$($OCAMLC -version)
 AC_MSG_RESULT($OCAMLVERSION)
 case $OCAMLVERSION in
   0.*|1.*|2.*|3.*)
@@ -61,7 +61,7 @@ if test "$OCAMLOPT" = no ; then
   AC_MSG_WARN(cannot find ocamlopt; bytecode compilation only.)
 else
   AC_MSG_CHECKING(ocamlopt version)
-  TMPVERSION=$($OCAMLOPT --version)
+  TMPVERSION=$($OCAMLOPT -version)
   if test "$TMPVERSION" != "$OCAMLVERSION" ; then
     AC_MSG_RESULT($TMPVERSION)
     AC_MSG_WARN(version differs from ocamlc; ocamlopt discarded.)
@@ -75,7 +75,7 @@ fi
 AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no)
 if test "$OCAMLCDOTOPT" != no ; then
   AC_MSG_CHECKING(ocamlc.opt version)
-  TMPVERSION=$($OCAMLCDOTOPT --version)
+  TMPVERSION=$($OCAMLCDOTOPT -version)
   if test "$TMPVERSION" != "$OCAMLVERSION" ; then
     AC_MSG_RESULT($TMPVERSION)
     AC_MSG_WARN(version differs from ocamlc; ocamlc.opt discarded.)
@@ -88,7 +88,7 @@ fi
 AC_CHECK_PROG(OCAMLOPTDOTOPT,ocamlopt.opt,ocamlopt.opt,no)
 if test "$OCAMLOPTDOTOPT" != no ; then
   AC_MSG_CHECKING(ocamlc.opt version)
-  TMPVERSION=$($OCAMLOPTDOTOPT --version)
+  TMPVERSION=$($OCAMLOPTDOTOPT -version)
   if test "$TMPVERSION" != "$OCAMLVERSION" ; then
     AC_MSG_RESULT($TMPVERSION)
     AC_MSG_WARN(version differs from ocamlc; ocamlopt.opt discarded.)

graphdepend.ml4

@@ -10,8 +10,8 @@
 DECLARE PLUGIN "dpdgraph"
 
 open Pp
-open Constrarg
 open Stdarg
+open EConstr
 
 let debug msg = if false then Feedback.msg_debug msg
 
@@ -35,18 +35,10 @@ let get_dirlist_grefs dirlist =
 
 let is_prop gref id =
 try
-let glob = Glob_term.GRef(Loc.ghost, gref, None) in
-   let env = Global.env() in
-   let sigma = Evd.from_env env in
-   let sigma', c = Pretyping.understand_tcc env sigma glob in
-   let sigma2 = Evarconv.consider_remaining_unif_problems env sigma' in
-   let sigma3, nf = Evarutil.nf_evars_and_universes sigma2 in
-   let pl, uctx = Evd.universe_context sigma3 in
-   let env2 = Environ.push_context uctx (Evarutil.nf_env_evar sigma3 env) in
-   let c2 = nf c in
-   let t = Environ.j_type (Typeops.infer env2 c2) in
-   let t2 = Environ.j_type (Typeops.infer env2 t) in
-       Term.is_Prop t2
+  let t, ctx = Universes.type_of_global gref in
+  let env = Environ.push_context_set ctx (Global.env ()) in
+  let s = (Typeops.infer_type env t).Environ.utj_type in
+  Sorts.is_prop s
 with _ ->
   begin
     warning (str "unable to determine the type of the type for " ++ str id);
@@ -72,9 +64,9 @@ module G = struct
       let qualid =
         Nametab.shortest_qualid_of_global Names.Idset.empty (gref n) in
       let dirpath, ident = Libnames.repr_qualid qualid in
-      let dirpath = Names.string_of_dirpath dirpath in
+      let dirpath = Names.DirPath.to_string dirpath in
       let dirpath = if dirpath = "<>" then "" else dirpath in
-      let name = Names.string_of_id ident in
+      let name = Names.Id.to_string ident in
         (dirpath, name)
         (*
       let mod_list = Names.repr_dirpath dir_path in
@@ -260,8 +252,10 @@ let locate_mp_dirpath ref =
   let (loc,qid) = Libnames.qualid_of_reference ref in
   try Nametab.dirpath_of_module (Nametab.locate_module qid)
   with Not_found ->
-    CErrors.user_err_loc
-      (loc,"",str "Unknown module" ++ spc() ++ Libnames.pr_qualid qid)
+    let msg = str "Unknown module" ++ spc() ++ Libnames.pr_qualid qid in
+    match loc with
+    | None -> CErrors.user_err msg
+    | Some loc -> CErrors.user_err ~loc msg
 
 VERNAC COMMAND EXTEND DependGraphSetFile CLASSIFIED AS QUERY
   | ["Set" "DependGraph" "File" string(str)] -> [ filename := str ]

searchdepend.ml4

@@ -8,9 +8,8 @@
 (*        (see the enclosed LICENSE file for mode details)                    *)
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 
-
 open Pp
-open Constrarg
+open Stdarg
 
 module Data = struct
   type t = int Globnames.Refmap.t
@@ -25,14 +24,14 @@ module Data = struct
   let fold f d acc = Globnames.Refmap.fold f d acc
 end
 
-let add_identifier (x:Names.identifier)(d:Data.t) =
+let add_identifier (x:Names.Id.t)(d:Data.t) =
   failwith
     ("SearchDep does not expect to find plain identifiers :" ^
-     Names.string_of_id x)
+     Names.Id.to_string x)
 
-let add_sort (s:Term.sorts)(d:Data.t) = d
+let add_sort (s:Sorts.t)(d:Data.t) = d
 
-let add_constant (cst:Names.constant)(d:Data.t) =
+let add_constant (cst:Names.Constant.t)(d:Data.t) =
   Data.add (Globnames.ConstRef cst) d
 
 let add_inductive ((k,i):Names.inductive)(d:Data.t) =

tests/graph.dot.oracle

@@ -401,7 +401,9 @@ Test_exists_last [label="exists_last", URL=<Test.html#exists_last>, peripheries=
   Test_split_nth -> Test_split [] ;
   Test_split_nth -> Test_nth [] ;
   Test_split_nth -> Test_list_ind [] ;
-  Test_list_ind -> Test_list_rect [] ;
+  Test_list_ind -> Test_cons [] ;
+  Test_list_ind -> Test_nil [] ;
+  Test_list_ind -> Test_list [] ;
   Test_list_rect -> Test_cons [] ;
   Test_list_rect -> Test_nil [] ;
   Test_list_rect -> Test_list [] ;

tests/graph.dpd.oracle

@@ -456,8 +456,8 @@ E: 52 178 [weight=2, ];
 E: 52 179 [weight=2, ];
 E: 52 180 [weight=26, ];
 E: 53 180 [weight=6, ];
-E: 54 55 [weight=50, ];
-E: 54 168 [weight=108, ];
+E: 54 55 [weight=49, ];
+E: 54 168 [weight=107, ];
 E: 54 176 [weight=1, ];
 E: 54 178 [weight=5, ];
 E: 54 179 [weight=2, ];
@@ -1076,10 +1076,9 @@ E: 175 177 [weight=1, ];
 E: 175 178 [weight=1, ];
 E: 175 179 [weight=1, ];
 E: 175 180 [weight=4, ];
-E: 176 177 [weight=1, ];
-E: 176 178 [weight=1, ];
-E: 176 179 [weight=1, ];
-E: 176 180 [weight=4, ];
+E: 176 178 [weight=2, ];
+E: 176 179 [weight=2, ];
+E: 176 180 [weight=10, ];
 E: 177 178 [weight=2, ];
 E: 177 179 [weight=2, ];
 E: 177 180 [weight=10, ];

tests/graph2.dot.oracle

@@ -21,8 +21,6 @@ Test_perm_trans [label="perm_trans", URL=<Test.html#perm_trans>, fillcolor="#7FA
 _eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ;
 _eq [label="eq", URL=<.html#eq>, fillcolor="#E2CDFA"] ;
 _eq_refl [label="eq_refl", URL=<.html#eq_refl>, fillcolor="#7FAAFF"] ;
-_eq_rect [label="eq_rect", URL=<.html#eq_rect>, fillcolor="#F070D1"] ;
-Test_list_rect [label="list_rect", URL=<Test.html#list_rect>, fillcolor="#F070D1"] ;
 Test_perm_nil [label="perm_nil", URL=<Test.html#perm_nil>, fillcolor="#7FAAFF"] ;
 Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>, fillcolor="#7FFFD4"] ;
   Test_Permutation_app_swap -> Test_Permutation_sym [] ;
@@ -47,8 +45,10 @@ Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>,
   Test_Permutation_refl -> Test_Permutation [] ;
   Test_Permutation_refl -> Test_perm_skip [] ;
   Test_Permutation_refl -> Test_perm_nil [] ;
-  Test_list_ind -> Test_list_rect [] ;
-  _eq_ind -> _eq_rect [] ;
+  Test_list_ind -> Test_list [] ;
+  Test_list_ind -> Test_nil [] ;
+  Test_list_ind -> Test_cons [] ;
+  _eq_ind -> _eq [] ;
   _eq_ind_r -> _eq_ind [] ;
   _eq_ind_r -> _eq_sym [] ;
   Test_Permutation_trans -> Test_Permutation [] ;
@@ -69,14 +69,10 @@ Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>,
   Test_perm_trans -> Test_cons [] ;
   _eq_sym -> _eq [] ;
   _eq_sym -> _eq_refl [] ;
-  _eq_rect -> _eq [] ;
-  Test_list_rect -> Test_list [] ;
-  Test_list_rect -> Test_nil [] ;
-  Test_list_rect -> Test_cons [] ;
   Test_perm_nil -> Test_list [] ;
   Test_perm_nil -> Test_nil [] ;
   Test_perm_nil -> Test_cons [] ;
   Test_Permutation_ind -> Test_Permutation [] ;
 subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled 
-Test_Permutation_ind; Test_perm_nil; Test_list_rect; Test_perm_trans; Test_cons; Test_nil; Test_perm_swap; Test_perm_skip; Test_list; Test_Permutation; Test_app; Test_Permutation_trans; Test_list_ind; Test_Permutation_refl; Test_app_comm_cons; Test_app_nil_end; Test_Permutation_sym; Test_Permutation_app_swap; };
+Test_Permutation_ind; Test_perm_nil; Test_perm_trans; Test_cons; Test_nil; Test_perm_swap; Test_perm_skip; Test_list; Test_Permutation; Test_app; Test_Permutation_trans; Test_list_ind; Test_Permutation_refl; Test_app_comm_cons; Test_app_nil_end; Test_Permutation_sym; Test_Permutation_app_swap; };
 } /* END */

tests/graph2.dpd.oracle

@@ -11,16 +11,14 @@ N: 192 "list" [kind=inductive, prop=no, path="Test", ];
 N: 188 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ];
 N: 185 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ];
 N: 197 "perm_trans" [kind=construct, prop=yes, path="Test", ];
-N: 202 "list_rect" [body=yes, kind=cnst, prop=no, path="Test", ];
 N: 193 "perm_skip" [kind=construct, prop=yes, path="Test", ];
 N: 200 "eq_refl" [kind=construct, prop=yes, ];
 N: 187 "eq_ind" [body=yes, kind=cnst, prop=yes, ];
-N: 204 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ];
+N: 202 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ];
 N: 191 "Permutation" [kind=inductive, prop=no, path="Test", ];
 N: 190 "app" [body=yes, kind=cnst, prop=no, path="Test", ];
 N: 184 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ];
-N: 203 "perm_nil" [kind=construct, prop=yes, path="Test", ];
-N: 201 "eq_rect" [body=yes, kind=cnst, prop=no, ];
+N: 201 "perm_nil" [kind=construct, prop=yes, path="Test", ];
 N: 196 "cons" [kind=construct, prop=no, path="Test", ];
 E: 181 182 [weight=3, ];
 E: 181 183 [weight=2, ];
@@ -42,8 +40,8 @@ E: 182 192 [weight=12, ];
 E: 182 193 [weight=1, ];
 E: 182 194 [weight=1, ];
 E: 182 197 [weight=1, ];
-E: 182 203 [weight=1, ];
-E: 182 204 [weight=1, ];
+E: 182 201 [weight=1, ];
+E: 182 202 [weight=1, ];
 E: 183 186 [weight=1, ];
 E: 183 187 [weight=1, ];
 E: 183 190 [weight=6, ];
@@ -61,13 +59,11 @@ E: 185 186 [weight=1, ];
 E: 185 191 [weight=3, ];
 E: 185 192 [weight=4, ];
 E: 185 193 [weight=1, ];
-E: 185 203 [weight=1, ];
-E: 186 192 [weight=4, ];
-E: 186 195 [weight=1, ];
-E: 186 196 [weight=1, ];
-E: 186 202 [weight=1, ];
-E: 187 199 [weight=1, ];
-E: 187 201 [weight=1, ];
+E: 185 201 [weight=1, ];
+E: 186 192 [weight=10, ];
+E: 186 195 [weight=2, ];
+E: 186 196 [weight=2, ];
+E: 187 199 [weight=4, ];
 E: 188 187 [weight=1, ];
 E: 188 198 [weight=1, ];
 E: 188 199 [weight=2, ];
@@ -90,14 +86,10 @@ E: 197 195 [weight=2, ];
 E: 197 196 [weight=6, ];
 E: 198 199 [weight=6, ];
 E: 198 200 [weight=1, ];
-E: 201 199 [weight=4, ];
-E: 202 192 [weight=10, ];
-E: 202 195 [weight=2, ];
-E: 202 196 [weight=2, ];
-E: 203 192 [weight=6, ];
-E: 203 195 [weight=2, ];
-E: 203 196 [weight=6, ];
-E: 204 191 [weight=14, ];
-E: 204 192 [weight=30, ];
-E: 204 195 [weight=4, ];
-E: 204 196 [weight=12, ];
+E: 201 192 [weight=6, ];
+E: 201 195 [weight=2, ];
+E: 201 196 [weight=6, ];
+E: 202 191 [weight=14, ];
+E: 202 192 [weight=30, ];
+E: 202 195 [weight=4, ];
+E: 202 196 [weight=12, ];

tests/search.oracle

@@ -3,5 +3,4 @@ Welcome to Coq
 Fetching opaque proofs from disk for dpdgraph.tests.Test
 [cons(42) nil(6) perm_swap(1) perm_skip(3) list(18) Permutation(11) app(43)
 Permutation_trans(3) eq_ind_r(1) eq_ind(2) list_ind(2) Permutation_refl(2)
-app_comm_cons(1) app_nil_end(2) Permutation_sym(3)
-]
+app_comm_cons(1) app_nil_end(2) Permutation_sym(3) ]