diff options
33 files changed, 322 insertions, 159 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index c7437c4a4a..a9230042a5 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -13,4 +13,4 @@ Fixes / closes #???? <!-- If this is a feature pull request / breaks compatibility: --> <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated. -- [ ] Entry added in [CHANGES](/CHANGES). +- [ ] Entry added in CHANGES. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 37b556c553..1a769333cc 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -28,6 +28,8 @@ Please make pull requests against the `master` branch. It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests. +If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so. + Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes. Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. diff --git a/Makefile.checker b/Makefile.checker index 5b5855782f..8334b6a2a6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -33,7 +33,7 @@ CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE)) -include $(CHECKERDEPS) ifeq ($(BEST),opt) -$(CHICKEN): checker/check.cmxa checker/main.ml +$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ $(STRIP) $@ @@ -43,7 +43,7 @@ $(CHICKEN): $(CHICKENBYTE) cp $< $@ endif -$(CHICKENBYTE): checker/check.cma checker/main.ml +$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ diff --git a/Makefile.ide b/Makefile.ide index 08829b5544..09eef1f6bb 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -45,8 +45,8 @@ IDEDEPS:=clib/clib.cma lib/lib.cma IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map diff --git a/checker/checker.mli b/checker/checker.mli new file mode 100644 index 0000000000..ceab137747 --- /dev/null +++ b/checker/checker.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val start : unit -> unit diff --git a/checker/main.mli b/checker/main.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/checker/main.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/checker/print.mli b/checker/print.mli new file mode 100644 index 0000000000..3b2715de92 --- /dev/null +++ b/checker/print.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Cic + +val print_pure_constr : constr -> unit diff --git a/checker/validate.ml b/checker/validate.ml index 8200405878..2624e6d495 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -49,8 +49,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx exception ValidObjError of string * error_context * Obj.t let fail ctx o s = raise (ValidObjError(s,ctx,o)) -type func = error_context -> Obj.t -> unit - (* Check that object o is a block with tag t *) let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () diff --git a/checker/validate.mli b/checker/validate.mli new file mode 100644 index 0000000000..7eed692a0b --- /dev/null +++ b/checker/validate.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val validate : bool -> Values.value -> 'a -> unit diff --git a/checker/values.ml b/checker/values.ml index 5a371164c6..4698227ff0 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -372,22 +372,3 @@ let v_lib = let v_opaques = Array (v_computation v_constr) let v_univopaques = Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|])) - -(** Registering dynamic values *) - -module IntOrd = -struct - type t = int - let compare (x : t) (y : t) = compare x y -end - -module IntMap = Map.Make(IntOrd) - -let dyn_table : value IntMap.t ref = ref IntMap.empty - -let register_dyn name t = - dyn_table := IntMap.add name t !dyn_table - -let find_dyn name = - try IntMap.find name !dyn_table - with Not_found -> Any diff --git a/checker/values.mli b/checker/values.mli new file mode 100644 index 0000000000..aad8fd5f45 --- /dev/null +++ b/checker/values.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type value = + | Any + | Fail of string + | Tuple of string * value array + | Sum of string * int * value array array + | Array of value + | List of value + | Opt of value + | Int + | String + | Annot of string * value + | Dyn + +val v_univopaques : value +val v_libsum : value +val v_lib : value +val v_opaques : value +val v_stm_seg : value diff --git a/checker/votour.ml b/checker/votour.ml index 77c9999c42..8cb97a2b1b 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -210,7 +210,6 @@ let access_list v o pos = let access_block o = match Repr.repr o with | BLOCK (tag, os) -> (tag, os) | _ -> raise Exit -let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit (** raises Exit if the object has not the expected structure *) exception Forbidden @@ -249,8 +248,7 @@ let rec get_children v o pos = match v with |Dyn -> begin match Repr.repr o with | BLOCK (0, [|id; o|]) -> - let n = access_int id in - let tpe = find_dyn n in + let tpe = Any in [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] | _ -> raise Exit end @@ -395,7 +393,7 @@ let visit_vo f = | None -> () done -let main = +let () = if not !Sys.interactive then Arg.parse [] visit_vo ("votour: guided tour of a Coq .vo or .vi file\n"^ diff --git a/checker/votour.mli b/checker/votour.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/checker/votour.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/dev/ci/README.md b/dev/ci/README.md index f4423558cc..bb13587e94 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 0000000000..78789a6fc5 --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli new file mode 100644 index 0000000000..0c0c5d1e74 --- /dev/null +++ b/ide/config_lexer.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val print_file : string -> string list Util.String.Map.t -> unit +val load_file : string -> string list Util.String.Map.t diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli new file mode 100644 index 0000000000..53026be38b --- /dev/null +++ b/ide/coq_commands.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val tactics : string list list +val commands : string list list +val state_preserving : string list diff --git a/ide/coq_lex.mli b/ide/coq_lex.mli new file mode 100644 index 0000000000..417e0a76fa --- /dev/null +++ b/ide/coq_lex.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val delimit_sentences : (int -> GText.tag -> unit) -> string -> unit + +exception Unterminated diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 8d99cc3e66..6e330c62b5 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -55,6 +55,8 @@ let os_specific_init () = () (** Win32 *) +IFDEF WIN32 THEN + (* On win32, we add the directory of coqide to the PATH at launch-time (this used to be done in a .bat script). *) @@ -86,7 +88,6 @@ let reroute_stdout_stderr () = (* We also provide specific kill and interrupt functions. *) -IFDEF WIN32 THEN external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = diff --git a/ide/coqide_main.mli b/ide/coqide_main.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/ide/coqide_main.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/ide/coqide_ui.mli b/ide/coqide_ui.mli new file mode 100644 index 0000000000..9f6fa5635a --- /dev/null +++ b/ide/coqide_ui.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val init : unit -> unit +val ui_m : GAction.ui_manager diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index f0575e325a..7c0a7495a0 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -7,11 +7,7 @@ (************************************************************************) let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) -let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0) let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0) -let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0) -let space = Glib.Utf8.to_unichar " " ~pos:(ref 0) -let tab = Glib.Utf8.to_unichar "\t" ~pos:(ref 0) (* TODO: avoid num and prime at the head of a word *) @@ -30,17 +26,6 @@ let ends_word (it:GText.iter) = not (is_word_char c) ) - -let inside_word (it:GText.iter) = - let c = it#char in - not (starts_word it) && - not (ends_word it) && - is_word_char c - - -let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it - - let find_word_start (it:GText.iter) = let rec step_to_start it = Minilib.log "Find word start"; @@ -72,100 +57,6 @@ let get_word_around (it:GText.iter) = let stop = find_word_end it in start,stop - -let rec complete_backward w (it:GText.iter) = - Minilib.log "Complete backward..."; - match it#backward_search w with - | None -> (Minilib.log "backward_search failed";None) - | Some (start,stop) -> - Minilib.log ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset)); - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 - then complete_backward w start - else Some (start,stop,ne) - else complete_backward w start - - -let rec complete_forward w (it:GText.iter) = - Minilib.log "Complete forward..."; - match it#forward_search w with - | None -> None - | Some (start,stop) -> - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 then - complete_forward w stop - else Some (stop,stop,ne) - else complete_forward w stop - - -let find_comment_end (start:GText.iter) = - let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) = - match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with - | None,_ -> comment_end - | Some _, None -> raise Not_found - | Some (_,next_search_start),Some (next_search_end,next_comment_end) -> - find_nested_comment next_search_start next_search_end next_comment_end - in - match start#forward_search "*)" with - | None -> raise Not_found - | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end - - -let rec find_string_end (start:GText.iter) = - let dblquote = int_of_char '"' in - let rec escaped_dblquote c = - (c#char = dblquote) && not (escaped_dblquote c#backward_char) - in - match start#forward_search "\"" with - | None -> raise Not_found - | Some (stop,next_start) -> - if escaped_dblquote stop#backward_char - then find_string_end next_start - else next_start - - -let rec find_next_sentence (from:GText.iter) = - match (from#forward_search ".") with - | None -> raise Not_found - | Some (non_vernac_search_end,next_sentence) -> - match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with - | None,None -> - if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0 - then next_sentence else find_next_sentence next_sentence - | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start) - | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start) - | Some (_,comment_search_start),Some (_,string_search_start) -> - find_next_sentence ( - if comment_search_start#compare string_search_start < 0 - then find_comment_end comment_search_start - else find_string_end string_search_start) - - -let find_nearest_forward (cursor:GText.iter) targets = - let fold_targets acc target = - match cursor#forward_search target,acc with - | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start - | Some (t_start,_),None -> Some t_start - | _ -> acc - in - match List.fold_left fold_targets None targets with - | None -> raise Not_found - | Some nearest -> nearest - - -let find_nearest_backward (cursor:GText.iter) targets = - let fold_targets acc target = - match cursor#backward_search target,acc with - | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start - | Some (t_start,_),None -> Some t_start - | _ -> acc - in - match List.fold_left fold_targets None targets with - | None -> raise Not_found - | Some nearest -> nearest - (** On double-click on a view, select the whole word. This is a workaround for a deficient word handling in TextView. *) let fix_double_click self = diff --git a/ide/gtk_parsing.mli b/ide/gtk_parsing.mli new file mode 100644 index 0000000000..b54f731b33 --- /dev/null +++ b/ide/gtk_parsing.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val fix_double_click : + < buffer : < get_iter : [> `INSERT ] -> GText.iter; + move_mark : [> `INSERT | `SEL_BOUND ] -> + where:GText.iter -> unit; + .. >; + event : < connect : + < button_press : + callback:([> `TWO_BUTTON_PRESS ] Gdk.event -> + bool) -> + 'a; + .. >; + .. >; + .. > -> + unit +val starts_word : GText.iter -> bool +val ends_word : GText.iter -> bool +val find_word_start : GText.iter -> GText.iter +val find_word_end : GText.iter -> GText.iter diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/ide/ide_slave.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/ide/macos_prehook.mli b/ide/macos_prehook.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/ide/macos_prehook.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/ide/nanoPG.mli b/ide/nanoPG.mli new file mode 100644 index 0000000000..3ad8435b5c --- /dev/null +++ b/ide/nanoPG.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val get_documentation : unit -> string +val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook -> + GAction.action_group list -> unit diff --git a/ide/utf8_convert.mli b/ide/utf8_convert.mli new file mode 100644 index 0000000000..06a131a68e --- /dev/null +++ b/ide/utf8_convert.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val f : string -> string diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cbc4ee2ec4..5f501bff10 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -301,21 +301,29 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let poly, univsctx = match c.const_entry_universes with - | Monomorphic_const_entry univs -> false, univs - | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs - in - let ctx = Univ.ContextSet.union univsctx ctx in let body, ctx, _ = match trust with | Pure -> body, ctx, [] | SideEffects _ -> inline_side_effects env body ctx side_eff in - let env = push_context_set ~strict:(not poly) ctx env in - let ctx = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) - else Monomorphic_const_entry ctx + let env, usubst, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> + let ctx = Univ.ContextSet.union univs ctx in + let env = push_context_set ~strict:true ctx env in + env, Univ.empty_level_subst, Monomorphic_const ctx + | Polymorphic_const_entry uctx -> + (** Ensure not to generate internal constraints in polymorphic mode. + The only way for this to happen would be that either the body + contained deferred universes, or that it contains monomorphic + side-effects. The first property is ruled out by upper layers, + and the second one is ensured by the fact we currently + unconditionally export side-effects from polymorphic definitions, + i.e. [trust] is always [Pure]. *) + let () = assert (Univ.ContextSet.is_empty ctx) in + let env = push_context ~strict:false uctx env in + let sbst, auctx = Univ.abstract_universes uctx in + let sbst = Univ.make_instance_subst sbst in + env, sbst, Polymorphic_const auctx in - let usubst, univs = abstract_constant_universes ctx in let j = infer env body in let typ = match typ with | None -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 167d6bda0d..d04bdb6521 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -343,16 +343,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now if poly || now then let make_body t (c, eff) = let body = c in - let typ = - if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then - nf t - else t + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff)) in + let typ = if allow_deferred then t else nf t in let env = Global.env () in let used_univs_body = Univops.universes_of_constr env body in let used_univs_typ = Univops.universes_of_constr env typ in - if keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff) then + if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to diff --git a/test-suite/Makefile b/test-suite/Makefile index de669218ce..16a56f4408 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,6 +40,7 @@ coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) +VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) @@ -174,10 +175,20 @@ summary.log: # if not on travis we can get the log files (they're just there for a # local build, and downloadable on GitLab) +PRINT_LOGS?= +TRAVIS?= # special because we want to print travis_fold directives +ifdef APPVEYOR +PRINT_LOGS:=APPVEYOR +else +ifdef CIRCLECI +PRINT_LOGS:=CIRCLECI +endif #CIRCLECI +endif #APPVEYOR + report: summary.log $(HIDE)bash save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi + $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### diff --git a/test-suite/README.md b/test-suite/README.md new file mode 100644 index 0000000000..1d1195646e --- /dev/null +++ b/test-suite/README.md @@ -0,0 +1,75 @@ +# Coq Test Suite + +The test suite can be run from the Coq root directory by `make test-suite`. +This does a clean step first, so if you've already run it, then change something, +you'll have to do a lot of work again. + +If you run `make` from the `test-suite` directory, there is no clean step. +You can also run `make aaa/bbb/ccc.v.log` to build the log for one test, +or `make ddd` where `ddd` is on of the sub-directories of `test-suite` +to just build the logs for that directory. +In these cases, a summary is not printed, but can be generated by `make summary`. + +`make -B` can be used to rerun tests ( -B meaning always remake). + +From the `test-suite` directory, `make report` (included in `make +all`) prints a summary of which tests failed using the produced log +files (this still works when only some tests are built as described +above). Setting the `PRINT_LOGS` variable will make it print the logs +of the failing tests. + +For instance, running the following in the `test-suite` directory: + +```bash +$ echo Fail. > success/fail.v # make some failing test + +$ make +TEST prerequisite/make_local.v +... +TEST success/fail.v +... +BUILDING SUMMARY FILE +FAILURES + success/fail.v...Error! (should be accepted) +Makefile:189: recipe for target 'all failed +make: *** [report] Error 1 + +$ make report PRINT_LOGS=1 +BUILDING SUMMARY FILE +logs/success/fail.v.log +==========> TESTING success/fail.v <========== +Welcome to Coq (version information) +Skipping rcfile loading. +File "/path/to/success/fail.v", line 1, characters 4-5: +Error: +Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]). + +0m0.000000s 0m0.000000s +0m0.040000s 0m0.000000s +==========> FAILURE <========== + success/fail.v...Error! (should be accepted) + +FAILURES + success/fail.v...Error! (should be accepted) +Makefile:189: recipe for target 'report' failed +make: *** [report] Error 1 + +$ echo 'Comments "foo".' > success/fail.v + +$ make +TEST success/fail.v +BUILDING SUMMARY FILE +NO FAILURES +``` + +See [`test-suite/Makefile`](/test-suite/Makefile) for more information. + +## Adding a test + +Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number. +Files in this directory are tested for successful compilation. +When you fix a bug, you should usually add a regression test here as well. + +The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile. + +There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output. diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v index b736b734fd..aa8da53361 100644 --- a/test-suite/success/abstract_poly.v +++ b/test-suite/success/abstract_poly.v @@ -17,4 +17,4 @@ intros m n P e p. abstract (rewrite e in p; exact p). Defined. -Check bar_subproof@{Set Set Set}. +Check bar_subproof@{Set Set}. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index fd4be08b12..2433cb1d0f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -455,7 +455,7 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; - eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed"; + eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) |