From 495bccc436cfe72af9955b4b9d8564a8831850b9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Feb 2017 23:23:53 +0100 Subject: Fixing #4499 (not using unnamed record field in {| |} notation). --- interp/constrextern.ml | 23 +++++++++++++---------- test-suite/output/Record.out | 6 ++++++ test-suite/output/Record.v | 5 +++++ 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dd8a48b85e..0ba056a878 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -307,16 +307,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = if !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = - match projs with - | [] -> acc - | None :: q -> ip q args acc - | Some c :: q -> - match args with - | [] -> raise No_match - | CPatAtom(_, None) :: tail -> ip q tail acc - (* we don't want to have 'x = _' in our patterns *) - | head :: tail -> ip q tail - ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, CPatAtom(_, None) -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + ((extern_reference loc Id.Set.empty (ConstRef c), pat) :: acc) + | _ -> raise No_match in + ip q tail acc + | _ -> assert false in CPatRecord(loc, List.rev (ip projs args [])) with diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index 36d643a447..37b4fb25f7 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -14,3 +14,9 @@ build 5 : test_r build_c 5 : test_c +fun '(C _ p) => p + : N -> True +fun '{| T := T |} => T + : N -> Type +fun '(C T p) => (T, p) + : N -> Type * True diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 6aa3df9830..c3d9f1e573 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -19,3 +19,8 @@ Check build 5. Check {| field := 5 |}. Check build_r 5. Check build_c 5. + +Record N := C { T : Type; _ : True }. +Check fun x:N => let 'C _ p := x in p. +Check fun x:N => let 'C T _ := x in T. +Check fun x:N => let 'C T p := x in (T,p). -- cgit v1.2.3 From f7cf2bccd813994e3cd98e97fe9c1c8b5cbde3cf Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Feb 2017 23:59:04 +0100 Subject: Better support for printing constructors with let-ins. This allows e.g. to use the record notations even when there are defined fields. A priori fixed also missing parameters when interpreting primitive tokens. --- interp/constrextern.ml | 13 ++--------- interp/constrintern.ml | 51 ++++++++++++++++++++++++++++++++++++++------ interp/notation_ops.ml | 6 ++++-- pretyping/glob_ops.ml | 33 ++++++++++++++++++++++++++++ pretyping/glob_ops.mli | 2 ++ test-suite/output/Cases.out | 14 +++++++++--- test-suite/output/Cases.v | 15 +++++++++++++ test-suite/output/Record.out | 10 +++++++++ test-suite/output/Record.v | 7 ++++++ 9 files changed, 129 insertions(+), 22 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0ba056a878..74504e36d4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -274,17 +274,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = - (* pboutill: There are letins in pat which is incompatible with notations and - not explicit application. *) - match pat with - | PatCstr(loc,cstrsp,args,na) - when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> - let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in - let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) - | _ -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in match availability_of_prim_token p sc scopes with | None -> raise No_match @@ -293,7 +284,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na with No_match -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c916fcd886..99ef21da3c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -994,6 +994,45 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr))) +open Term +open Declarations + +(* Similar to Cases.adjust_local_defs but on RCPat *) +let insert_local_defs_in_pattern (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | Context.Rel.Declaration.LocalDef _ :: decls, args -> Constrexpr.RCPatAtom (Loc.ghost,None) :: aux decls args + | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) + | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) l + +let add_local_defs_and_check_length loc env g pl args = match g with + | ConstructRef cstr -> + (* We consider that no variables corresponding to local binders + have been given in the "explicit" arguments, which come from a + "@C args" notation or from a custom user notation *) + let pl' = insert_local_defs_in_pattern cstr pl in + let maxargs = Inductiveops.constructor_nalldecls cstr in + if List.length pl' + List.length args > maxargs then + error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr); + (* Two possibilities: either the args are given with explict + variables for local definitions, then we give the explicit args + extended with local defs, so that there is nothing more to be + added later on; or the args are not enough to have all arguments, + which a priori means local defs to add in the [args] part, so we + postpone the insertion of local defs in the explicit args *) + (* Note: further checks done later by check_constructor_length *) + if List.length pl' + List.length args = maxargs then pl' else pl + | _ -> pl + let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st @@ -1221,7 +1260,7 @@ let rec subst_pat_iterator y t p = match p with | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a) | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl) -let drop_notations_pattern looked_for = +let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) let ensure_kind top loc g = @@ -1350,9 +1389,9 @@ let drop_notations_pattern looked_for = | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - RCPatCstr (loc, g, - List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ - List.map (in_pat false scopes) args, []) + let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in + let pl = add_local_defs_and_check_length loc genv g pl args in + RCPatCstr (loc, g, pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1445,7 +1484,7 @@ and check_no_patcast_subst (pl,pll) = let intern_cases_pattern genv scopes aliases pat = check_no_patcast pat; intern_pat genv aliases - (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) + (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := @@ -1455,7 +1494,7 @@ let intern_ind_pattern genv scopes pat = check_no_patcast pat; let no_not = try - drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat + drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc in match no_not with diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0c5393cf41..5648821539 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1158,6 +1158,7 @@ let match_notation_constr u c (metas,pat) = metas ([],[],[]) (* Matching cases pattern *) + let add_patterns_for_params ind l = let mib,_ = Global.lookup_inductive ind in let nparams = mib.Declarations.mind_nparams in @@ -1190,10 +1191,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - sigma,(0,add_patterns_for_params (fst r1) largs) + let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + sigma,(0,l) | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = add_patterns_for_params (fst r1) args1 in + let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818f4..0eda776519 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -559,12 +559,45 @@ let rec cases_pattern_of_glob_constr na = function PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found +open Declarations +open Term +open Context + +(* Keep only patterns which are not bound to a local definitions *) +let drop_local_defs typi args = + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | [], [] -> [] + | Rel.Declaration.LocalDef _ :: decls, pat :: args -> + begin + match pat with + | PatVar (_,Anonymous) -> aux decls args + | _ -> raise Not_found (* The pattern is used, one cannot drop it *) + end + | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) args + +let add_patterns_for_params_remove_local_defs (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + let l = + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in + drop_local_defs typi l in + Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l + (* Turn a closed cases pattern into a glob_constr *) let rec glob_constr_of_closed_cases_pattern_aux = function | PatCstr (loc,cstr,[],Anonymous) -> GRef (loc,ConstructRef cstr,None) | PatCstr (loc,cstr,l,Anonymous) -> let ref = GRef (loc,ConstructRef cstr,None) in + let l = add_patterns_for_params_remove_local_defs cstr l in GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533f..6b8f131f41 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -76,3 +76,5 @@ val map_pattern : (glob_constr -> glob_constr) -> val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr + +val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 8ce6f9795c..f064dfe763 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -2,18 +2,18 @@ t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with - | @k _ x0 => f x0 (F x0) + | k _ x0 => f x0 (F x0) end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t Argument scopes are [function_scope function_scope _] = fun d : TT => match d with - | @CTT _ _ b => b + | {| f3 := b |} => b end : TT -> 0 = 0 = fun d : TT => match d with - | @CTT _ _ b => b + | {| f3 := b |} => b end : TT -> 0 = 0 proj = @@ -72,3 +72,11 @@ e1 : texp t1 e2 : texp t2 The term "0" has type "nat" while it is expected to have type "typeDenote t0". +fun '{{n, m, _}} => n + m + : J -> nat +fun '{{n, m, p}} => n + m + p + : J -> nat +fun '(D n m p q) => n + m + p + q + : J -> nat +The command has indeed failed with message: +The constructor D (in type J) expects 3 arguments. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4074896420..6a4fd007df 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:= | TBinop t1 t2 _ b e1 e2 => O end. +(* Test notations with local definitions in constructors *) + +Inductive J := D : forall n m, let p := n+m in nat -> J. +Notation "{{ n , m , q }}" := (D n m q). + +Check fun x : J => let '{{n, m, _}} := x in n + m. +Check fun x : J => let '{{n, m, p}} := x in n + m + p. + +(* Cannot use the notation because of the dependency in p *) + +Check fun x => let '(D n m p q) := x in n+m+p+q. + +(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *) + +Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index 37b4fb25f7..d45343fe60 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -20,3 +20,13 @@ fun '{| T := T |} => T : N -> Type fun '(C T p) => (T, p) : N -> Type * True +fun '{| q := p |} => p + : M -> True +fun '{| U := T |} => T + : M -> Type +fun '{| U := T; q := p |} => (T, p) + : M -> Type * True +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index c3d9f1e573..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -24,3 +24,10 @@ Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). + +Record M := D { U : Type; a := 0; q : True }. +Check fun x:M => let 'D T _ p := x in p. +Check fun x:M => let 'D T _ p := x in T. +Check fun x:M => let 'D T p := x in (T,p). +Check fun x:M => let 'D T a p := x in (T,p,a). +Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). -- cgit v1.2.3 From 58e804f07172acc6bb01c8bdafde1217eb4ec4b8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 13 Apr 2017 20:41:40 +0200 Subject: Reinstate fixpoint refolding in [cbn], deactivated by mistake. Add a test-suite file to be sure we won't regress silently. --- pretyping/reductionops.ml | 2 +- test-suite/success/cbn.v | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 test-suite/success/cbn.v diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 297f0a1a8e..ba92f64b95 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -755,7 +755,7 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty context" in contract_fix *) let reduce_and_refold_fix recfun env refold cst_l fix sk = let raw_answer = - let env = if refold then None else Some env in + let env = if refold then Some env else None in contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in apply_subst (fun x (t,sk') -> diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v new file mode 100644 index 0000000000..6aeb05f54e --- /dev/null +++ b/test-suite/success/cbn.v @@ -0,0 +1,18 @@ +(* cbn is able to refold mutual recursive calls *) + +Fixpoint foo (n : nat) := + match n with + | 0 => true + | S n => g n + end +with g (n : nat) : bool := + match n with + | 0 => true + | S n => foo n + end. +Goal forall n, foo (S n) = g n. + intros. cbn. + match goal with + |- g _ = g _ => reflexivity + end. +Qed. \ No newline at end of file -- cgit v1.2.3 From c98ed6692d16784e531f7eb8dbb1460fa20c7766 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 May 2017 11:13:31 +0200 Subject: Fix #5255: [Context (x : T := y)] should mean [Let x := y]. --- test-suite/bugs/closed/5255.v | 24 ++++++++++++++++++++++++ toplevel/classes.ml | 18 ++++++++++++++++-- 2 files changed, 40 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/5255.v diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v new file mode 100644 index 0000000000..5daaf9edbf --- /dev/null +++ b/test-suite/bugs/closed/5255.v @@ -0,0 +1,24 @@ +Section foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End foo. + +Module Type Foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End Foo. + +Set Universe Polymorphism. + +Inductive unit := tt. +Inductive eq {A} (x y : A) : Type := eq_refl : eq x y. + +Section bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End bar. + +Module Type Bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End Bar. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8142d48d88..d3da263dde 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -383,7 +383,13 @@ let context poly l = let ctx = Univ.ContextSet.to_context !uctx in (* Declare the universe context once *) let () = uctx := Univ.ContextSet.empty in - let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in + let decl = match b with + | None -> + (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) + | Some b -> + let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + (DefinitionEntry entry, IsAssumption Logical) + in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> @@ -399,9 +405,17 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in - let nstatus = + let nstatus = match b with + | None -> pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) + | Some b -> + let ctx = Univ.ContextSet.to_context !uctx in + let decl = (Discharge, poly, Definition) in + let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let hook = Lemmas.mk_hook (fun _ gr -> gr) in + let _ = Command.declare_definition id decl entry [] [] hook in + Lib.sections_are_opened () || Lib.is_modtype_strict () in let () = uctx := Univ.ContextSet.empty in status && nstatus -- cgit v1.2.3 From 6735a7cbcaa3757e4d9ad60cb5a64fb5197b961e Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 May 2017 11:46:31 -0400 Subject: fix swapping of ids in tuples, bug 5486 --- pretyping/patternops.ml | 4 ++-- test-suite/bugs/closed/5486.v | 15 +++++++++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/5486.v diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 75d3ed30ba..79e9c727d7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -360,9 +360,9 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = + let mkGLambda na c = GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v new file mode 100644 index 0000000000..390133162f --- /dev/null +++ b/test-suite/bugs/closed/5486.v @@ -0,0 +1,15 @@ +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k : + forall _ : T, Fm), + @eq Fm + (k + match p return T with + | pair p0 swap => fst p0 + end) f. + intros. + (* next statement failed in Bug 5486 *) + match goal with + | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ] + => pose (let (a, b) := d in e a b) as t0 + end. -- cgit v1.2.3 From 8c2c92cf47536b93e8e7377e8cfd89342325dbcc Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 May 2017 12:59:08 -0400 Subject: Fixing bug #5526,allow nonlinear variables in Notation patterns --- test-suite/bugs/closed/5526.v | 3 +++ test-suite/output/Notations3.out | 4 ++++ test-suite/output/Notations3.v | 6 ++++++ toplevel/metasyntax.ml | 22 +++++++++++----------- 4 files changed, 24 insertions(+), 11 deletions(-) create mode 100644 test-suite/bugs/closed/5526.v diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v new file mode 100644 index 0000000000..88f219be30 --- /dev/null +++ b/test-suite/bugs/closed/5526.v @@ -0,0 +1,3 @@ +Fail Notation "x === x" := (eq_refl x) (at level 10). +Reserved Notation "x === x" (only printing, at level 10). +Notation "x === x" := (eq_refl x) (only printing). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 360f379676..0cb870c577 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,3 +98,7 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +fun x : ?A => x === x + : forall x : ?A, x = x +where +?A : [x : ?A |- Type] (x cannot be used) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 4b8bfe3124..5676fe8c7c 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" := (at level 85, x binder, z binder). Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(**********************************************************************) +(* Test printing of #5526 *) + +Notation "x === x" := (eq_refl x) (only printing, at level 10). +Check (fun x => eq_refl x). diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 349c05a38d..6ad5182e2d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -294,22 +294,22 @@ let is_numeral symbs = | _ -> false -let rec get_notation_vars = function +let rec get_notation_vars onlyprint = function | [] -> [] | NonTerminal id :: sl -> - let vars = get_notation_vars sl in + let vars = get_notation_vars onlyprint sl in if Id.equal id ldots_var then vars else - if Id.List.mem id vars then + (* don't check for nonlinearity if printing only, see Bug 5526 *) + if not onlyprint && Id.List.mem id vars then errorlabstrm "Metasyntax.get_notation_vars" (str "Variable " ++ pr_id id ++ str " occurs more than once.") - else - id::vars - | (Terminal _ | Break _) :: sl -> get_notation_vars sl + else id::vars + | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl | SProdList _ :: _ -> assert false -let analyze_notation_tokens l = +let analyze_notation_tokens ~onlyprint l = let l = raw_analyze_notation_tokens l in - let vars = get_notation_vars l in + let vars = get_notation_vars onlyprint l in let recvars,l = interp_list_parser [] l in recvars, List.subtract Id.equal vars (List.map snd recvars), l @@ -1016,7 +1016,7 @@ let compute_syntax_data df modifiers = if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in - let (recvars,mainvars,symbols) = analyze_notation_tokens toks in + let (recvars,mainvars,symbols) = analyze_notation_tokens onlyprint toks in let _ = check_useless_entry_types recvars mainvars etyps in let _ = check_binder_type recvars etyps in let ntn_for_interp = make_notation_key symbols in @@ -1240,7 +1240,7 @@ let add_notation_in_scope local df c mods scope = let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in - let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in + let (recvars,mainvars,symbs) = analyze_notation_tokens onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let i_typs, onlyprint = if not (is_numeral symbs) then begin let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in @@ -1317,7 +1317,7 @@ let add_notation local c ((loc,df),modifiers) sc = let add_notation_extra_printing_rule df k v = let notk = let dfs = split_notation_string df in - let _,_, symbs = analyze_notation_tokens dfs in + let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in make_notation_key symbs in Notation.add_notation_extra_printing_rule notk k v -- cgit v1.2.3 From 92e3fddf3b2b169e4853cb382f5c44d7ec9f2733 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Fri, 19 May 2017 11:41:28 -0400 Subject: add test for Show with -emacs, bug 5535 --- test-suite/Makefile | 2 +- test-suite/output/Show.out | 12 ++++++++++++ test-suite/output/Show.v | 11 +++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 test-suite/output/Show.out create mode 100644 test-suite/output/Show.v diff --git a/test-suite/Makefile b/test-suite/Makefile index c10cd4ed44..e87e133768 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -44,7 +44,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1))))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out new file mode 100644 index 0000000000..d0c963be17 --- /dev/null +++ b/test-suite/output/Show.out @@ -0,0 +1,12 @@ +3 subgoals, subgoal 1 (ID 29) + + H : 0 = 0 + ============================ + 1 = 1 + +subgoal 2 (ID 33) is: + 1 = S (S m') +subgoal 3 (ID 20) is: + S (S n') = S m +(dependent evars: (printing disabled) ) + diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v new file mode 100644 index 0000000000..60faac8dd9 --- /dev/null +++ b/test-suite/output/Show.v @@ -0,0 +1,11 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) + +(* tests of Show output with -emacs flag to coqtop; see bug 5535 *) + +Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). +Proof. + intros. + induction n as [| n']. + induction m as [| m']. + Show. +Admitted. -- cgit v1.2.3 From 321a42bf24490b08e12af5d8c2cf627e01a25aba Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Feb 2017 18:45:28 +0100 Subject: Fix bindings handling of setoid_rewrite. This fixes the discrepancy between "rewrite H with (1 := x)" and "setoid_rewrite H with (1 := x)". --- proofs/clenv.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0a90e0dbd3..beed9e36b7 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -661,7 +661,8 @@ let evar_of_binder holes = function | NamedHyp s -> evar_with_name holes s | AnonHyp n -> try - let h = List.nth holes (pred n) in + let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in + let h = List.nth nondeps (pred n) in h.hole_evar with e when CErrors.noncritical e -> errorlabstrm "" (str "No such binder.") -- cgit v1.2.3 From 004b82086b1c546e962abeac2fe91d600a304813 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 May 2017 18:30:22 -0400 Subject: Add parsers-examples target to fiat-parsers ci This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.--- dev/ci/ci-fiat-parsers.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index c62aa1d859..d8460bc70c 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} -( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples ) -- cgit v1.2.3 From ec57e7bedbd6719ad1b03800d6a8d7efd1b75ee4 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Thu, 25 May 2017 11:03:18 -0400 Subject: Bug 5546, qualify datatype constructors when needed --- test-suite/output/ShowMatch.out | 8 ++++++++ test-suite/output/ShowMatch.v | 13 +++++++++++++ toplevel/vernacentries.ml | 32 ++++++++++++++++++++++++-------- 3 files changed, 45 insertions(+), 8 deletions(-) create mode 100644 test-suite/output/ShowMatch.out create mode 100644 test-suite/output/ShowMatch.v diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out new file mode 100644 index 0000000000..e5520b8dfa --- /dev/null +++ b/test-suite/output/ShowMatch.out @@ -0,0 +1,8 @@ +match # with + | f => + end + +match # with + | A.f => + end + diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v new file mode 100644 index 0000000000..02b7eada83 --- /dev/null +++ b/test-suite/output/ShowMatch.v @@ -0,0 +1,13 @@ +(* Bug 5546 complained about unqualified constructors in Show Match output, + when qualification is needed to disambiguate them +*) + +Module A. + Inductive foo := f. + Show Match foo. (* no need to disambiguate *) +End A. + +Module B. + Inductive foo := f. + (* local foo shadows A.foo, so constructor "f" needs disambiguation *) + Show Match A.foo. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3df6d7a580..9beb3a6063 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -120,14 +120,29 @@ let show_intro all = [Not_found] is raised if the given string isn't the qualid of a known inductive type. *) +(* + + HH notes in PR #679: + + The Show Match could also be made more robust, for instance in the + presence of let in the branch of a constructor. A + decompose_prod_assum would probably suffice for that, but then, it + is a Context.Rel.Declaration.t which needs to be matched and not + just a pair (name,type). + + Otherwise, this is OK. After all, the API on inductive types is not + so canonical in general, and in this simple case, working at the + low-level of mind_nf_lc seems reasonable (compared to working at the + higher-level of Inductiveops). + +*) + let make_cases_aux glob_ref = match glob_ref with - | Globnames.IndRef i -> - let {Declarations.mind_nparams = np} - , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } - = Global.lookup_inductive i in - Util.Array.fold_right2 - (fun consname typ l -> + | Globnames.IndRef ind -> + let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in + Util.Array.fold_right_i + (fun i typ l -> let al = List.rev (fst (decompose_prod typ)) in let al = Util.List.skipn np al in let rec rename avoid = function @@ -136,8 +151,9 @@ let make_cases_aux glob_ref = let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in Id.to_string n' :: rename (n'::avoid) l in let al' = rename [] al in - (Id.to_string consname :: al') :: l) - carr tarr [] + let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in + (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) + tarr [] | _ -> raise Not_found let make_cases s = -- cgit v1.2.3 From 1a169b01458829f9420aea9c855b1ef28e5c847d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 26 May 2017 22:34:57 +0200 Subject: Fixing a subtle bug in tclWITHHOLES. This fixes Théo's bug on eset. --- tactics/tacticals.ml | 3 ++- test-suite/success/evars.v | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 66da9ee182..b3655d3735 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -487,6 +487,7 @@ module New = struct let check_evars env sigma extsigma origsigma = let rec is_undefined_up_to_restriction sigma evk = + if Evd.mem origsigma evk then None else let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) @@ -500,7 +501,7 @@ module New = struct let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with - | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc + | Some (evk',evi) -> (evk',evi)::acc | _ -> acc) extsigma [] in diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 4e2bf45118..4b2f7b53e1 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -414,4 +414,10 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2. Import EqNotations. Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a. +(* Check that pre-existing evars are not counted as newly undefined in "set" *) +(* Reported by Théo *) +Goal exists n : nat, n = n -> True. +eexists. +set (H := _ = _). +Abort. -- cgit v1.2.3 From bde0f3038bffa660b0fc15084fb99bce42c7aa43 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 27 May 2017 09:44:38 +0200 Subject: Fix a bug in checker Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug. --- checker/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 27f79e7963..9ccaaa7cbb 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -530,7 +530,7 @@ let check_positivity env_ar mind params nrecp inds = let check_inductive env kn mib = Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) - let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in + let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) -- cgit v1.2.3 From 2125c92aa9d17b27c9a19a59774e7e319e48262b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 29 May 2017 18:03:19 +0200 Subject: Omega: use "simpl" only on coefficents, not on atoms (fix #4132) Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example). --- plugins/omega/coq_omega.ml | 44 ++++++++++++++++++++++++++++++++++++------- test-suite/bugs/closed/4132.v | 31 ++++++++++++++++++++++++++++++ 2 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 test-suite/bugs/closed/4132.v diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e3076a..cefd48538a 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -666,6 +666,36 @@ let clever_rewrite p vpath t gl = let t' = applist(t, (vargs @ [abstracted])) in exact (applist(t',[mkNewMeta()])) gl +(** simpl_coeffs : + The subterm at location [path_init] in the current goal should + look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce + via "simpl" each [ci] and the final constant [k]. + The path [path_k] gives the location of constant [k]. + Earlier, the whole was a mere call to [focused_simpl], + leading to reduction inside the atoms [vi], which is bad, + for instance when the atom is an evaluable definition + (see #4132). *) + +let simpl_coeffs path_init path_k gl = + let rec loop n t = + if Int.equal n 0 then pf_nf gl t + else + (* t should be of the form ((v * c) + ...) *) + match kind_of_term t with + | App(f,[|t1;t2|]) -> + (match kind_of_term t1 with + | App (g,[|v;c|]) -> + let c' = pf_nf gl c in + let t2' = loop (pred n) t2 in + mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) + | _ -> assert false) + | _ -> assert false + in + let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let newc = context (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) + in + Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl + let rec shuffle p (t1,t2) = match t1,t2 with | Oplus(l1,r1), Oplus(l2,r2) -> @@ -728,7 +758,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -763,7 +793,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -786,7 +816,7 @@ let shuffle_mult_right p_init e1 k2 e2 = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -813,7 +843,7 @@ let shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -854,7 +884,7 @@ let rec scalar p n = function let scalar_norm p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | (_::l) -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; @@ -865,7 +895,7 @@ let scalar_norm p_init = let norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _:: l -> clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: @@ -875,7 +905,7 @@ let norm_add p_init = let scalar_norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _ :: l -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v new file mode 100644 index 0000000000..806ffb771f --- /dev/null +++ b/test-suite/bugs/closed/4132.v @@ -0,0 +1,31 @@ + +Require Import ZArith Omega. +Open Scope Z_scope. + +(** bug 4132: omega was using "simpl" either on whole equations, or on + delimited but wrong spots. This was leading to unexpected reductions + when one atom (here [b]) is an evaluable reference instead of a variable. *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +Qed. + +Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "index out of bounds" in the past, + but I never managed to reproduce that in any version, + even before my fix. *) +Qed. + +Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "Failure(occurence 2)" in the past, + but I never managed to reproduce that. *) +Qed. -- cgit v1.2.3 From e6c41b96a5ea9f8559acf176cdf997b05ccfb317 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 30 May 2017 12:10:35 +0200 Subject: Fix bug 5550: "typeclasses eauto with" does not work with section variables. --- tactics/class_tactics.ml | 1 + test-suite/bugs/closed/5550.v | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/5550.v diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d1ae85e7be..2c911addf5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -593,6 +593,7 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = + not only_classes || let open Context.Named.Declaration in try let t = Global.lookup_named (get_id hyp) |> get_type in (* Section variable, reindex only if the type changed *) diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v new file mode 100644 index 0000000000..bb1222489a --- /dev/null +++ b/test-suite/bugs/closed/5550.v @@ -0,0 +1,10 @@ +Section foo. + + Variable bar : Prop. + Variable H : bar. + + Goal bar. + typeclasses eauto with foobar. + Qed. + +End foo. -- cgit v1.2.3 From 0bba5da999dc8eeef75c7040562f687ce589ed11 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 14:04:34 -0400 Subject: Add test-suite checks for coqchk with constraints --- test-suite/coqchk/univ.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 84a4009d7e..19eea94b19 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) := (rank_injective : injective_in T natural D rank) (rank_onto : forall i, equivalent (less_than i n) (in_image T natural D rank i)). + +(* Constraints *) +Universes i j. +Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})). +Constraint i < j. +Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}). +Universes i' j'. +Constraint i' = j'. +Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})). +Inductive constraint4 : (Type -> Type) -> Type + := mk_constraint4 : let U1 := Type in + let U2 := Type in + constraint4 (fun x : U1 => (x : U2)). -- cgit v1.2.3 From 4af77d01c434ff11f0899d504628f4ff91c49142 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 12:11:28 -0400 Subject: Add opened bug 5019 --- test-suite/bugs/opened/5019.v | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 test-suite/bugs/opened/5019.v diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v new file mode 100644 index 0000000000..09622097c5 --- /dev/null +++ b/test-suite/bugs/opened/5019.v @@ -0,0 +1,4 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Fail Timeout 1 zify. -- cgit v1.2.3 From 1d6a1036a7c472e1f20c5ec586d2484203a2fe2e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 12:48:47 -0400 Subject: Fix bug #5019 (looping zify on dependent types) This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever. --- plugins/omega/PreOmega.v | 7 ++++++- test-suite/bugs/closed/5019.v | 5 +++++ test-suite/bugs/opened/5019.v | 4 ---- 3 files changed, 11 insertions(+), 5 deletions(-) create mode 100644 test-suite/bugs/closed/5019.v delete mode 100644 test-suite/bugs/opened/5019.v diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 5f5f548f84..6c0e2d776d 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -174,12 +174,18 @@ Ltac zify_nat_op := match isnat with | true => simpl (Z.of_nat (S a)) in H | _ => rewrite (Nat2Z.inj_succ a) in H + | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in this one hypothesis *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H end | |- context [ Z.of_nat (S ?a) ] => let isnat := isnatcst a in match isnat with | true => simpl (Z.of_nat (S a)) | _ => rewrite (Nat2Z.inj_succ a) + | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in the goal *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) end (* atoms of type nat : we add a positivity condition (if not already there) *) @@ -401,4 +407,3 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. (** The complete Z-ification tactic *) Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op. - diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v new file mode 100644 index 0000000000..7c973f88b5 --- /dev/null +++ b/test-suite/bugs/closed/5019.v @@ -0,0 +1,5 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Timeout 1 zify. (* used to loop forever; should take < 0.01 s *) +Admitted. diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v deleted file mode 100644 index 09622097c5..0000000000 --- a/test-suite/bugs/opened/5019.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. - clear; intros. - Fail Timeout 1 zify. -- cgit v1.2.3 From dffba98368b5b1156e1933dc7377317281c57491 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 9 Jun 2017 16:38:02 +0200 Subject: Makefile.common: remove an obsolete comment after PR#499 --- Makefile.common | 2 -- 1 file changed, 2 deletions(-) diff --git a/Makefile.common b/Makefile.common index e7887f216a..62bbbc4fd7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -145,8 +145,6 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) # vo files ########################################################################### -## we now retrieve the names of .vo file to compile in */vo.itarget files - GENVOFILES := $(GENVFILES:.v=.vo) THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \ -- cgit v1.2.3 From 79c42e22dd5106dcb85229ceec75331029ab5486 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 10 Jun 2017 16:13:54 +0200 Subject: Remove remaining vo.itarget files (obsolete since PR #499) --- plugins/btauto/vo.itarget | 3 --- plugins/derive/vo.itarget | 1 - plugins/extraction/vo.itarget | 16 ---------------- plugins/fourier/vo.itarget | 2 -- plugins/funind/vo.itarget | 1 - plugins/ltac/vo.itarget | 1 - plugins/micromega/vo.itarget | 16 ---------------- plugins/nsatz/vo.itarget | 1 - plugins/omega/vo.itarget | 5 ----- plugins/quote/vo.itarget | 1 - plugins/romega/vo.itarget | 2 -- plugins/rtauto/vo.itarget | 2 -- plugins/setoid_ring/vo.itarget | 24 ------------------------ plugins/ssr/vo.itarget | 3 --- plugins/ssrmatching/vo.itarget | 1 - theories/Logic/vo.itarget | 35 ----------------------------------- 16 files changed, 114 deletions(-) delete mode 100644 plugins/btauto/vo.itarget delete mode 100644 plugins/derive/vo.itarget delete mode 100644 plugins/extraction/vo.itarget delete mode 100644 plugins/fourier/vo.itarget delete mode 100644 plugins/funind/vo.itarget delete mode 100644 plugins/ltac/vo.itarget delete mode 100644 plugins/micromega/vo.itarget delete mode 100644 plugins/nsatz/vo.itarget delete mode 100644 plugins/omega/vo.itarget delete mode 100644 plugins/quote/vo.itarget delete mode 100644 plugins/romega/vo.itarget delete mode 100644 plugins/rtauto/vo.itarget delete mode 100644 plugins/setoid_ring/vo.itarget delete mode 100644 plugins/ssr/vo.itarget delete mode 100644 plugins/ssrmatching/vo.itarget delete mode 100644 theories/Logic/vo.itarget diff --git a/plugins/btauto/vo.itarget b/plugins/btauto/vo.itarget deleted file mode 100644 index 1f72d3ef22..0000000000 --- a/plugins/btauto/vo.itarget +++ /dev/null @@ -1,3 +0,0 @@ -Algebra.vo -Reflect.vo -Btauto.vo diff --git a/plugins/derive/vo.itarget b/plugins/derive/vo.itarget deleted file mode 100644 index b480982193..0000000000 --- a/plugins/derive/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Derive.vo \ No newline at end of file diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget deleted file mode 100644 index 9c30c5eb3e..0000000000 --- a/plugins/extraction/vo.itarget +++ /dev/null @@ -1,16 +0,0 @@ -ExtrHaskellBasic.vo -ExtrHaskellNatNum.vo -ExtrHaskellNatInt.vo -ExtrHaskellNatInteger.vo -ExtrHaskellZNum.vo -ExtrHaskellZInt.vo -ExtrHaskellZInteger.vo -ExtrHaskellString.vo -ExtrOcamlBasic.vo -ExtrOcamlIntConv.vo -ExtrOcamlBigIntConv.vo -ExtrOcamlNatInt.vo -ExtrOcamlNatBigInt.vo -ExtrOcamlZInt.vo -ExtrOcamlZBigInt.vo -ExtrOcamlString.vo diff --git a/plugins/fourier/vo.itarget b/plugins/fourier/vo.itarget deleted file mode 100644 index 87d82dacc5..0000000000 --- a/plugins/fourier/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -Fourier_util.vo -Fourier.vo diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget deleted file mode 100644 index 33c9683028..0000000000 --- a/plugins/funind/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Recdef.vo diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget deleted file mode 100644 index a28fb770be..0000000000 --- a/plugins/ltac/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Ltac.vo diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget deleted file mode 100644 index a555d5ba17..0000000000 --- a/plugins/micromega/vo.itarget +++ /dev/null @@ -1,16 +0,0 @@ -MExtraction.vo -EnvRing.vo -Env.vo -OrderedRing.vo -Psatz.vo -QMicromega.vo -Refl.vo -RingMicromega.vo -RMicromega.vo -Tauto.vo -VarMap.vo -ZCoeff.vo -ZMicromega.vo -Lia.vo -Lqa.vo -Lra.vo diff --git a/plugins/nsatz/vo.itarget b/plugins/nsatz/vo.itarget deleted file mode 100644 index 06fc883431..0000000000 --- a/plugins/nsatz/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Nsatz.vo diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget deleted file mode 100644 index 842210e216..0000000000 --- a/plugins/omega/vo.itarget +++ /dev/null @@ -1,5 +0,0 @@ -OmegaLemmas.vo -OmegaPlugin.vo -OmegaTactic.vo -Omega.vo -PreOmega.vo diff --git a/plugins/quote/vo.itarget b/plugins/quote/vo.itarget deleted file mode 100644 index 7a44fc5aa6..0000000000 --- a/plugins/quote/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Quote.vo \ No newline at end of file diff --git a/plugins/romega/vo.itarget b/plugins/romega/vo.itarget deleted file mode 100644 index f7a3c41c78..0000000000 --- a/plugins/romega/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -ReflOmegaCore.vo -ROmega.vo diff --git a/plugins/rtauto/vo.itarget b/plugins/rtauto/vo.itarget deleted file mode 100644 index 4c9364ad72..0000000000 --- a/plugins/rtauto/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -Bintree.vo -Rtauto.vo diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget deleted file mode 100644 index 595ba55ec6..0000000000 --- a/plugins/setoid_ring/vo.itarget +++ /dev/null @@ -1,24 +0,0 @@ -ArithRing.vo -BinList.vo -Field_tac.vo -Field_theory.vo -Field.vo -InitialRing.vo -NArithRing.vo -RealField.vo -Ring_base.vo -Ring_polynom.vo -Ring_tac.vo -Ring_theory.vo -Ring.vo -ZArithRing.vo -Algebra_syntax.vo -Cring.vo -Ncring.vo -Ncring_polynom.vo -Ncring_initial.vo -Ncring_tac.vo -Rings_Z.vo -Rings_R.vo -Rings_Q.vo -Integral_domain.vo \ No newline at end of file diff --git a/plugins/ssr/vo.itarget b/plugins/ssr/vo.itarget deleted file mode 100644 index 99f9f160bb..0000000000 --- a/plugins/ssr/vo.itarget +++ /dev/null @@ -1,3 +0,0 @@ -ssreflect.vo -ssrfun.vo -ssrbool.vo diff --git a/plugins/ssrmatching/vo.itarget b/plugins/ssrmatching/vo.itarget deleted file mode 100644 index b0eb388349..0000000000 --- a/plugins/ssrmatching/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -ssrmatching.vo diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget deleted file mode 100644 index 5eba0b6235..0000000000 --- a/theories/Logic/vo.itarget +++ /dev/null @@ -1,35 +0,0 @@ -Berardi.vo -PropExtensionalityFacts.vo -ChoiceFacts.vo -ClassicalChoice.vo -ClassicalDescription.vo -ClassicalEpsilon.vo -ClassicalFacts.vo -Classical_Pred_Type.vo -Classical_Prop.vo -ClassicalUniqueChoice.vo -Classical.vo -ConstructiveEpsilon.vo -Decidable.vo -Description.vo -Diaconescu.vo -Epsilon.vo -Eqdep_dec.vo -EqdepFacts.vo -Eqdep.vo -WeakFan.vo -WKL.vo -FunctionalExtensionality.vo -ExtensionalityFacts.vo -ExtensionalFunctionRepresentative.vo -Hurkens.vo -IndefiniteDescription.vo -JMeq.vo -ProofIrrelevanceFacts.vo -ProofIrrelevance.vo -PropFacts.vo -PropExtensionality.vo -RelationalChoice.vo -SetIsType.vo -SetoidChoice.vo -FinFun.vo -- cgit v1.2.3 From a2e1e2fa4f0a005e07972488b6ce6ad59404bd2c Mon Sep 17 00:00:00 2001 From: Maxime Denes Date: Fri, 9 Jun 2017 16:13:06 +0200 Subject: make test-suite/save-logs.sh usable also on old MacOS X --- test-suite/save-logs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh index fb8a1c1b0a..b613621085 100755 --- a/test-suite/save-logs.sh +++ b/test-suite/save-logs.sh @@ -9,7 +9,7 @@ mkdir "$SAVEDIR" # keep this synced with test-suite/Makefile FAILMARK="==========> FAILURE <==========" -FAILED=$(mktemp) +FAILED=$(mktemp /tmp/coq-check-XXXXX) find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" -- cgit v1.2.3 From c054dda76825435019ad1b29f7f4292d937d98f9 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Tue, 30 May 2017 10:49:41 +0200 Subject: Add support for "-bypass-API" argument of "coq_makefile" Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac --- .gitignore | 2 ++ config/coq_config.mli | 3 ++ configure.ml | 15 +++++++++ lib/coqProject_file.ml4 | 10 ++++-- lib/coqProject_file.mli | 1 + lib/envars.ml | 9 +----- lib/envars.mli | 5 +-- .../plugin-reach-outside-API-and-fail/run.sh | 37 ++++++++++++++++++++++ .../run.sh | 32 +++++++++++++++++++ test-suite/coq-makefile/template/src/test.ml4 | 1 + test-suite/coq-makefile/template/src/test_aux.ml | 2 +- test-suite/coq-makefile/template/src/test_aux.mli | 2 +- tools/coq_makefile.ml | 15 ++++----- tools/coqc.ml | 2 +- toplevel/coqinit.ml | 2 +- toplevel/coqtop.ml | 2 +- 16 files changed, 112 insertions(+), 28 deletions(-) create mode 100755 test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh create mode 100755 test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh diff --git a/.gitignore b/.gitignore index 84fe89d1eb..fa83045e75 100644 --- a/.gitignore +++ b/.gitignore @@ -72,6 +72,8 @@ test-suite/coq-makefile/*/mlihtml test-suite/coq-makefile/*/subdir/done test-suite/coq-makefile/latex1/all.pdf test-suite/coq-makefile/merlin1/.merlin +test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject +test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject # documentation diff --git a/config/coq_config.mli b/config/coq_config.mli index 2b3bc2c25b..3f7b65c395 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -53,7 +53,10 @@ val compile_date : string (* compile date *) val vo_magic_number : int val state_magic_number : int +val core_src_dirs : string list +val api_dirs : string list val plugins_dirs : string list +val all_src_dirs : string list val exec_extension : string (* "" under Unix, ".exe" under MS-windows *) val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *) diff --git a/configure.ml b/configure.ml index a5204d5b57..316cea5c93 100644 --- a/configure.ml +++ b/configure.ml @@ -1088,7 +1088,19 @@ let write_configml f = pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "no_native_compiler" (not !Prefs.nativecompiler); + + let core_src_dirs = [ "config"; "dev"; "kernel"; "library"; + "engine"; "pretyping"; "interp"; "parsing"; "proofs"; + "tactics"; "toplevel"; "printing"; "intf"; + "grammar"; "ide"; "stm"; "vernac" ] in + let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") + "" + core_src_dirs in + + pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; + pr "\nlet api_dirs = [\"API\"; \"lib\"]\n"; pr "\nlet plugins_dirs = [\n"; + let plugins = Sys.readdir "plugins" in Array.sort compare plugins; Array.iter @@ -1097,6 +1109,9 @@ let write_configml f = if Sys.is_directory f' && f.[0] <> '.' then pr " %S;\n" f') plugins; pr "]\n"; + + pr "\nlet all_src_dirs = core_src_dirs @ api_dirs @ plugins_dirs\n"; + close_out o; Unix.chmod f 0o444 diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 7a16605695..97aa90e07d 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -11,6 +11,7 @@ type project = { makefile : string option; install_kind : install option; use_ocamlopt : bool; + bypass_API : bool; v_files : string list; mli_files : string list; @@ -42,11 +43,12 @@ and install = | UserInstall (* TODO generate with PPX *) -let mk_project project_file makefile install_kind use_ocamlopt = { +let mk_project project_file makefile install_kind use_ocamlopt bypass_API = { project_file; makefile; install_kind; use_ocamlopt; + bypass_API; v_files = []; mli_files = []; @@ -166,6 +168,8 @@ let process_cmd_line orig_dir proj args = aux { proj with defs = proj.defs @ [v,def] } r | "-arg" :: a :: r -> aux { proj with extra_args = proj.extra_args @ [a] } r + | "-bypass-API" :: r -> + aux { proj with bypass_API = true } r | f :: r -> let f = CUnix.correct_path f orig_dir in let proj = @@ -185,11 +189,11 @@ let process_cmd_line orig_dir proj args = (******************************* API ************************************) let cmdline_args_to_project ~curdir args = - process_cmd_line curdir (mk_project None None None true) args + process_cmd_line curdir (mk_project None None None true false) args let read_project_file f = process_cmd_line (Filename.dirname f) - (mk_project (Some f) None (Some NoInstall) true) (parse f) + (mk_project (Some f) None (Some NoInstall) true false) (parse f) let rec find_project_file ~from ~projfile_name = let fname = Filename.concat from projfile_name in diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 8c8fc068a3..19fc9227ae 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -13,6 +13,7 @@ type project = { makefile : string option; install_kind : install option; use_ocamlopt : bool; + bypass_API : bool; v_files : string list; mli_files : string list; diff --git a/lib/envars.ml b/lib/envars.ml index 2f76183eb3..47baf66a69 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -202,14 +202,7 @@ let xdg_dirs ~warn = (* Print the configuration information *) -let coq_src_subdirs = [ - "config" ; "dev" ; "lib" ; "kernel" ; "library" ; - "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ; - "tactics" ; "toplevel" ; "printing" ; "intf" ; - "grammar" ; "ide" ; "stm"; "vernac" ; "API" ] @ - Coq_config.plugins_dirs - -let print_config ?(prefix_var_name="") f = +let print_config ?(prefix_var_name="") f coq_src_subdirs = let open Printf in fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0"); fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); diff --git a/lib/envars.mli b/lib/envars.mli index c8bbf17d96..edd13447fc 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -76,7 +76,4 @@ val xdg_data_dirs : (string -> unit) -> string list val xdg_dirs : warn : (string -> unit) -> string list (** {6 Prints the configuration information } *) -val print_config : ?prefix_var_name:string -> out_channel -> unit - -(** Directories in which coq sources are found *) -val coq_src_subdirs : string list +val print_config : ?prefix_var_name:string -> out_channel -> string list -> unit diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh new file mode 100755 index 0000000000..6301aa03c0 --- /dev/null +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash + +set -e + +git clean -dfx + +cat > _CoqProject < src/test_plugin.mllib < src/test.ml4 < _CoqProject < src/test_plugin.mllib < src/test.ml4 < ()) "test_plugin";; diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml index a01d0865a8..e134abd840 100644 --- a/test-suite/coq-makefile/template/src/test_aux.ml +++ b/test-suite/coq-makefile/template/src/test_aux.ml @@ -1 +1 @@ -let tac = Proofview.tclUNIT () +let tac = API.Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli index 10020f27de..2e7ad1529f 100644 --- a/test-suite/coq-makefile/template/src/test_aux.mli +++ b/test-suite/coq-makefile/template/src/test_aux.mli @@ -1 +1 @@ -val tac : unit Proofview.tactic +val tac : unit API.Proofview.tactic diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 8e2f75fc9c..e4f1359774 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,11 +27,6 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -(* These are the Coq library directories that are used for - * plugin development - *) -let lib_dirs = Envars.coq_src_subdirs - let usage () = output_string stderr "Usage summary:\ \n\ @@ -73,6 +68,7 @@ let usage () = \n[-f file]: take the contents of file as arguments\ \n[-o file]: output should go in file file\ \n Output file outside the current directory is forbidden.\ +\n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\n"; exit 1 @@ -197,9 +193,12 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) ;; -let generate_conf_coq_config oc args = +let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; - Envars.print_config ~prefix_var_name:"COQMF_" oc; + let src_dirs = if bypass_API + then Coq_config.all_src_dirs + else Coq_config.api_dirs @ Coq_config.plugins_dirs in + Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); ;; @@ -258,7 +257,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args; + generate_conf_coq_config oc args project.bypass_API; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; diff --git a/tools/coqc.ml b/tools/coqc.ml index 240531f123..c1f0182d9c 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -83,7 +83,7 @@ let parse_args () = | ("-config" | "--config") :: _ -> Envars.set_coqlib ~fail:(fun x -> x); - Envars.print_config stdout; + Envars.print_config stdout Coq_config.all_src_dirs; exit 0 |"--print-version" :: _ -> diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8fca302687..16fe405551 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -124,7 +124,7 @@ let init_ocaml_path () = Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl]) in Mltop.add_ml_dir (Envars.coqlib ()); - List.iter add_subdir Envars.coq_src_subdirs + List.iter add_subdir Coq_config.all_src_dirs let get_compat_version = function | "8.7" -> Flags.Current diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 26ee413fb0..31450ebd51 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -621,7 +621,7 @@ let init_toplevel arglist = Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); - if !print_config then (Envars.print_config stdout; exit (exitcode ())); + if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); init_load_path (); -- cgit v1.2.3 From 8443867a2f944c3ecaf0b0b826368c29935a21e1 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Thu, 8 Jun 2017 18:30:18 +0200 Subject: add overlays --- dev/ci/ci-user-overlay.sh | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 195ede6d00..0edaf07efc 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -30,3 +30,13 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi +echo "DEBUG: ci-user-overlay.sh 0" +if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then + echo "DEBUG: ci-user-overlay.sh 1" + bedrock_src_CI_BRANCH=trunk__API + bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git + bedrock_facade_CI_BRANCH=trunk__API + bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git + fiat_parsers_CI_BRANCH=trunk__API + fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git +fi -- cgit v1.2.3