diff options
| -rw-r--r-- | .gitlab-ci.yml | 8 | ||||
| -rw-r--r-- | API/API.mli | 21 | ||||
| -rw-r--r-- | grammar/argextend.mlp | 2 | ||||
| -rw-r--r-- | lib/envars.mli | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4366.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5578.v | 57 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 7 |
8 files changed, 100 insertions, 9 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1de9e7f7c8..e1feabd064 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -253,6 +253,14 @@ ci-color: ci-compcert: <<: *ci-template +ci-coq-dpdgraph: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_OPAM: "ocamlgraph" + EXTRA_PACKAGES: "autoconf" + allow_failure: true + ci-coquelicot: <<: *ci-template variables: diff --git a/API/API.mli b/API/API.mli index 899bafa1fd..2fd3f27927 100644 --- a/API/API.mli +++ b/API/API.mli @@ -72,6 +72,7 @@ sig val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds end type 'a puniverses = 'a * Instance.t + val out_punivs : 'a puniverses -> 'a module Constraint : module type of struct include Univ.Constraint end @@ -1038,7 +1039,16 @@ sig | Undef of inline | Def of Term.constr Mod_subst.substituted | OpaqueDef of Opaqueproof.opaque - type constant_type = Declarations.constant_type + type template_arity = Declarations.template_arity = { + template_param_levels : Univ.Level.t option list; + template_level : Univ.Universe.t; + } + + type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + + type constant_type = (Prelude.types, Context.Rel.t * template_arity) declaration_arity type constant_universes = Declarations.constant_universes type projection_body = Declarations.projection_body = { proj_ind : Names.MutInd.t; @@ -1145,6 +1155,11 @@ sig uj_val : 'constr; uj_type : 'types } + type 'types punsafe_type_judgment = 'types Environ.punsafe_type_judgment = { + utj_val : 'types; + utj_type : Sorts.t } + + type unsafe_type_judgment = Term.types punsafe_type_judgment val empty_env : env val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body val push_rel : Context.Rel.Declaration.t -> env -> env @@ -1170,6 +1185,7 @@ sig val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a val evaluable_named : Names.Id.t -> Environ.env -> bool + val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env end module UGraph : @@ -1233,6 +1249,7 @@ end module Typeops : sig + val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end @@ -2662,6 +2679,7 @@ sig type universe_opt_subst = Universes.universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types + val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr val new_univ_level : Names.DirPath.t -> Univ.Level.t @@ -3489,6 +3507,7 @@ sig type ltac_constant = Names.KerName.t + val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 36b9d612a0..8aecf0e0c8 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -178,7 +178,7 @@ let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in let pr_rules = match pr with - | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> + | None -> <:expr< fun _ _ _ _ -> Pp.str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in declare_str_items loc [ <:str_item< diff --git a/lib/envars.mli b/lib/envars.mli index edd13447fc..18b7676ce7 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -53,7 +53,7 @@ val coqroot : string the order it gets added to the search path. *) val coqpath : string list -(** [camlbin ()] is the path to the ocamlfind binary. *) +(** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string (** [camlp4bin ()] is the path to the camlp4 binary. *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2faf1e0ecb..5fbf59b815 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -649,8 +649,9 @@ module V85 = struct Goal.V82.hyps gls.Evd.sigma (sig_it gls) let make_autogoal_hints = - let cache = ref (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) + let cache = Summary.ref ~name:"make_autogoal_hints_cache" + (true, Environ.empty_named_context_val, + Hint_db.empty full_transparent_state true) in fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in @@ -979,8 +980,9 @@ module Search = struct search_hints : hint_db; } (** Local hints *) - let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, - Hint_db.empty full_transparent_state true) + let autogoal_cache = Summary.ref ~name:"autogoal_cache" + (DirPath.empty, true, Context.Named.empty, + Hint_db.empty full_transparent_state true) let make_autogoal_hints only_classes ?(st=full_transparent_state) g = let open Proofview in diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v index 6a5e9a4023..403c2d2026 100644 --- a/test-suite/bugs/closed/4366.v +++ b/test-suite/bugs/closed/4366.v @@ -10,6 +10,6 @@ end. Goal True. Proof. pose (v := stupid 24). -Timeout 2 vm_compute in v. +Timeout 4 vm_compute in v. exact I. Qed. diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v new file mode 100644 index 0000000000..5bcdaa2f18 --- /dev/null +++ b/test-suite/bugs/closed/5578.v @@ -0,0 +1,57 @@ +(* File reduced by coq-bug-finder from original input, then from 1549 lines to 298 lines, then from 277 lines to 133 lines, then from 985 lines to 138 lines, then from 206 lines to 139 lines, then from 203 lines to 142 lines, then from 262 lines to 152 lines, then from 567 lines to 151 lines, then from 3746 lines to 151 lines, then from 577 lines to 151 lines, then from 187 lines to 151 lines, thenfrom 981 lines to 940 lines, then from 938 lines to 175 lines, then from 589 lines to 205 lines, then from 3797 lines to 205 lines, then from 628 lines to 206 lines, then from 238 lines to 205 lines, then from 1346 lines to 213 lines, then from 633 lines to 214 lines, then from 243 lines to 213 lines, then from 5656 lines to 245 lines, then from 661 lines to 272 lines, then from 3856 lines to 352 lines, then from 1266 lines to 407 lines, then from 421 lines to 406 lines, then from 424 lines to 91 lines, then from 105 lines to 91 lines, then from 85 lines to 55 lines, then from 69 lines to 55 lines *) +(* coqc version trunk (May 2017) compiled on May 30 2017 13:28:59 with OCaml +4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-trunk,trunk (fd36c0451c26e44b1b7e93299d3367ad2d35fee3) *) + +Class Proper {A} (R : A -> A -> Prop) (m : A) := mkp : R m m. +Definition respectful {A B} (R : A -> A -> Prop) (R' : B -> B -> Prop) (f g : A -> B) := forall x y, R x y -> R' (f x) (g y). +Set Implicit Arguments. + +Class EqDec (A : Set) := { + eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true <-> x = y +}. + +Infix "?=" := eqb (at level 70) : eq_scope. + +Inductive Comp : Set -> Type := +| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A. + +Open Scope eq_scope. + +Goal forall (Rat : Set) (PositiveMap_t : Set -> Set) + type (t : type) (interp_type_list_message interp_type_rand interp_type_message : nat -> Set), + (forall eta : nat, PositiveMap_t (interp_type_rand eta) -> interp_type_list_message eta -> interp_type_message eta) -> + ((nat -> Rat) -> Prop) -> + forall (interp_type_sbool : nat -> Set) (interp_type0 : type -> nat -> Set), + (forall eta : nat, + (interp_type_list_message eta -> interp_type_message eta) -> PositiveMap_t (interp_type_rand eta) -> interp_type0 t eta) + -> (forall (t0 : type) (eta : nat), EqDec (interp_type0 t0 eta)) + -> (bool -> Comp bool) -> False. + clear. + intros Rat PositiveMap_t type t interp_type_list_message interp_type_rand interp_type_message adv negligible interp_type_sbool + interp_type interp_term_fixed_t_x + EqDec_interp_type ret_bool. + assert (forall f adv' k + (lem : forall (eta : nat) (evil_rands rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv eta evil_rands) rands + ?= interp_term_fixed_t_x eta (adv eta evil_rands) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + Undo. + assert (forall f adv' k + (lem : forall (eta : nat) (rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92730c14d0..74c7663ca5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -286,7 +286,12 @@ let ensure_exists f = let compile verbosely f = let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in - if not (List.is_empty pfs) then vernac_error (str "There are pending proofs") + if not (List.is_empty pfs) then + vernac_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") in match !Flags.compilation_mode with | BuildVo -> |