diff options
17 files changed, 383 insertions, 250 deletions
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh index e1aed4560d..de58527cca 100755 --- a/dev/tools/make-changelog.sh +++ b/dev/tools/make-changelog.sh @@ -25,11 +25,17 @@ case "$type_first_letter" in exit 1;; esac +printf "Fixes? (space separated list of bug numbers)\n" +read -r fixes_list + +fixes_string="$(echo $fixes_list | sed 's/ /~ and /g; s,\([0-9]\+\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')" +if [ ! -z "$fixes_string" ]; then fixes_string="$(printf '\n fixes %s,' "$fixes_string")"; fi + # shellcheck disable=SC2016 # the ` are regular strings, this is intended # use %s for the leading - to avoid looking like an option (not sure # if necessary but doesn't hurt) -printf '%s **%s:**\n Bla bla\n (`#%s <https://github.com/coq/coq/pull/%s>`_,\n by %s).' - "$type_full" "$PR" "$PR" "$(git config user.name)" > "$where" +printf '%s **%s:**\n Bla bla\n (`#%s <https://github.com/coq/coq/pull/%s>`_,%s\n by %s).' - "$type_full" "$PR" "$PR" "$fixes_string" "$(git config user.name)" > "$where" printf "Name of created changelog file:\n" printf "$where\n" diff --git a/doc/changelog/04-tactics/12366-fix-exists.rst b/doc/changelog/04-tactics/12366-fix-exists.rst new file mode 100644 index 0000000000..6d976ff562 --- /dev/null +++ b/doc/changelog/04-tactics/12366-fix-exists.rst @@ -0,0 +1,7 @@ +- **Changed:** + When using :tacn:`exists` or :tacn:`eexists` with multiple arguments, + the evaluation of arguments and applications of constructors are now interleaved. + This improves unification in some cases + (`#12366 <https://github.com/coq/coq/pull/12366>`_, + fixes `#12365 <https://github.com/coq/coq/issues/12365>`_, + by Attila Gáspár). diff --git a/doc/changelog/08-tools/12410-add-fixes.rst b/doc/changelog/08-tools/12410-add-fixes.rst new file mode 100644 index 0000000000..f4c41dc3c3 --- /dev/null +++ b/doc/changelog/08-tools/12410-add-fixes.rst @@ -0,0 +1,4 @@ +- **Changed:** + ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR + (`#12410 <https://github.com/coq/coq/pull/12410>`_, fixes `#12386 + <https://github.com/coq/coq/issues/12386>`_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst new file mode 100644 index 0000000000..4e5406ad4d --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst @@ -0,0 +1,5 @@ +- **Fixed:** + ``make pretty-timed-diff`` no longer raises Python exceptions in the rare + corner case where the log of times contains no files (`#12388 + <https://github.com/coq/coq/pull/12388>`_, fixes `#12387 + <https://github.com/coq/coq/pull/12387>`_, by Jason Gross). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5954ded67f..363148e2a0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Changes in 8.11+beta1 dropped when forcing a delayed opaque proof inside a polymorphic section. Also relaxes the nesting criterion for sections, as polymorphic sections can now appear inside a monomorphic one - (`#10664, <https://github.com/coq/coq/pull/10664>`_ by Pierre-Marie Pédrot). + (`#10664 <https://github.com/coq/coq/pull/10664>`_, by Pierre-Marie Pédrot). - **Changed:** Using ``SProp`` is now allowed by default, without needing to pass ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 @@ -476,7 +476,7 @@ Changes in 8.11+beta1 by Vincent Laporte). - **Removed:** Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` - (`#9881 <https://github.com/coq/coq/pull/9811>`_, + (`#9811 <https://github.com/coq/coq/pull/9811>`_, by Vincent Laporte). .. _811Reals: @@ -690,7 +690,7 @@ Changes in 8.11.1 Bump official OCaml support and CI testing to 4.10.0 (`#11131 <https://github.com/coq/coq/pull/11131>`_, `#11123 <https://github.com/coq/coq/pull/11123>`_, - `#11102 <https://github.com/coq/coq/pull/11123>`_, + `#11102 <https://github.com/coq/coq/pull/11102>`_, by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, Guillaume Melquiond, and Guillaume Munch-Maccagnoni). @@ -1091,7 +1091,7 @@ Other changes in 8.10+beta1 e.g., a numeral notation whose parsing function outputs a proof of :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`) - (`#9874 <https://github.com/coq/coq/pull/9840>`_, + (`#9874 <https://github.com/coq/coq/pull/9874>`_, closes `#9840 <https://github.com/coq/coq/issues/9840>`_ and `#9844 <https://github.com/coq/coq/issues/9844>`_, by Jason Gross). @@ -1107,7 +1107,7 @@ Other changes in 8.10+beta1 - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` (`#10061 <https://github.com/coq/coq/pull/10061>`_, - fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + fixes `#9681 <https://github.com/coq/coq/pull/9681>`_, by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). - The `quote plugin diff --git a/engine/uState.ml b/engine/uState.ml index 7c60d8317c..25d7638686 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -25,32 +25,32 @@ module UPairSet = UnivMinim.UPairSet (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : UnivNames.universe_binders * uinfo LMap.t; - uctx_local : ContextSet.t; (** The local context of variables *) - uctx_seff_univs : LSet.t; (** Local universes used through private constants *) - uctx_univ_variables : UnivSubst.universe_opt_subst; + { names : UnivNames.universe_binders * uinfo LMap.t; + local : ContextSet.t; (** The local context of variables *) + seff_univs : LSet.t; (** Local universes used through private constants *) + univ_variables : UnivSubst.universe_opt_subst; (** The local universes that are unification variables *) - uctx_univ_algebraic : LSet.t; + univ_algebraic : LSet.t; (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) - uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) - uctx_universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *) - uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) - uctx_weak_constraints : UPairSet.t + universes : UGraph.t; (** The current graph extended with the local constraints *) + universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *) + initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) + weak_constraints : UPairSet.t } let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes let empty = - { uctx_names = UNameMap.empty, LMap.empty; - uctx_local = ContextSet.empty; - uctx_seff_univs = LSet.empty; - uctx_univ_variables = LMap.empty; - uctx_univ_algebraic = LSet.empty; - uctx_universes = initial_sprop_cumulative; - uctx_universes_lbound = UGraph.Bound.Set; - uctx_initial_universes = initial_sprop_cumulative; - uctx_weak_constraints = UPairSet.empty; } + { names = UNameMap.empty, LMap.empty; + local = ContextSet.empty; + seff_univs = LSet.empty; + univ_variables = LMap.empty; + univ_algebraic = LSet.empty; + universes = initial_sprop_cumulative; + universes_lbound = UGraph.Bound.Set; + initial_universes = initial_sprop_cumulative; + weak_constraints = UPairSet.empty; } let elaboration_sprop_cumul = Goptions.declare_bool_option_and_ref ~depr:false @@ -59,15 +59,15 @@ let elaboration_sprop_cumul = let make ~lbound u = let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in { empty with - uctx_universes = u; - uctx_universes_lbound = lbound; - uctx_initial_universes = u} + universes = u; + universes_lbound = lbound; + initial_universes = u} let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e) let is_empty ctx = - ContextSet.is_empty ctx.uctx_local && - LMap.is_empty ctx.uctx_univ_variables + ContextSet.is_empty ctx.local && + LMap.is_empty ctx.univ_variables let uname_union s t = if s == t then s @@ -81,65 +81,65 @@ let union ctx ctx' = if ctx == ctx' then ctx else if is_empty ctx' then ctx else - let local = ContextSet.union ctx.uctx_local ctx'.uctx_local in - let seff = LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in - let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in - let newus = LSet.diff (ContextSet.levels ctx'.uctx_local) - (ContextSet.levels ctx.uctx_local) in - let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in - let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in + let local = ContextSet.union ctx.local ctx'.local in + let seff = LSet.union ctx.seff_univs ctx'.seff_univs in + let names = uname_union (fst ctx.names) (fst ctx'.names) in + let newus = LSet.diff (ContextSet.levels ctx'.local) + (ContextSet.levels ctx.local) in + let newus = LSet.diff newus (LMap.domain ctx.univ_variables) in + let weak = UPairSet.union ctx.weak_constraints ctx'.weak_constraints in let declarenew g = - LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.universes_lbound ~strict:false g) newus g in - let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in - { uctx_names = (names, names_rev); - uctx_local = local; - uctx_seff_univs = seff; - uctx_univ_variables = - LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; - uctx_univ_algebraic = - LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; - uctx_initial_universes = declarenew ctx.uctx_initial_universes; - uctx_universes = - (if local == ctx.uctx_local then ctx.uctx_universes + let names_rev = LMap.lunion (snd ctx.names) (snd ctx'.names) in + { names = (names, names_rev); + local = local; + seff_univs = seff; + univ_variables = + LMap.subst_union ctx.univ_variables ctx'.univ_variables; + univ_algebraic = + LSet.union ctx.univ_algebraic ctx'.univ_algebraic; + initial_universes = declarenew ctx.initial_universes; + universes = + (if local == ctx.local then ctx.universes else - let cstrsr = ContextSet.constraints ctx'.uctx_local in - UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); - uctx_universes_lbound = ctx.uctx_universes_lbound; - uctx_weak_constraints = weak} + let cstrsr = ContextSet.constraints ctx'.local in + UGraph.merge_constraints cstrsr (declarenew ctx.universes)); + universes_lbound = ctx.universes_lbound; + weak_constraints = weak} -let context_set ctx = ctx.uctx_local +let context_set ctx = ctx.local -let constraints ctx = snd ctx.uctx_local +let constraints ctx = snd ctx.local -let context ctx = ContextSet.to_context ctx.uctx_local +let context ctx = ContextSet.to_context ctx.local let univ_entry ~poly uctx = let open Entries in if poly then - let (binders, _) = uctx.uctx_names in + let (binders, _) = uctx.names in let uctx = context uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in Polymorphic_entry (nas, uctx) else Monomorphic_entry (context_set uctx) -let of_context_set ctx = { empty with uctx_local = ctx } +let of_context_set ctx = { empty with local = ctx } -let subst ctx = ctx.uctx_univ_variables +let subst ctx = ctx.univ_variables -let ugraph ctx = ctx.uctx_universes +let ugraph ctx = ctx.universes -let initial_graph ctx = ctx.uctx_initial_universes +let initial_graph ctx = ctx.initial_universes -let algebraics ctx = ctx.uctx_univ_algebraic +let algebraics ctx = ctx.univ_algebraic -let add_uctx_names ?loc s l (names, names_rev) = +let add_names ?loc s l (names, names_rev) = if UNameMap.mem s names - then user_err ?loc ~hdr:"add_uctx_names" + then user_err ?loc ~hdr:"add_names" Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound."); (UNameMap.add s l names, LMap.add l { uname = Some s; uloc = loc } names_rev) -let add_uctx_loc l loc (names, names_rev) = +let add_loc l loc (names, names_rev) = match loc with | None -> (names, names_rev) | Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev) @@ -151,7 +151,7 @@ let of_binders b = LMap.add l { uname = Some id; uloc = None } rmap) b LMap.empty in - { ctx with uctx_names = b, rmap } + { ctx with names = b, rmap } let invent_name (named,cnt) u = let rec aux i = @@ -162,13 +162,13 @@ let invent_name (named,cnt) u = aux cnt let universe_binders ctx = - let named, rev = ctx.uctx_names in + let named, rev = ctx.names in let named, _ = LSet.fold (fun u named -> match LMap.find u rev with | exception Not_found -> (* not sure if possible *) invent_name named u | { uname = None } -> invent_name named u | { uname = Some _ } -> named) - (ContextSet.levels ctx.uctx_local) (named, 0) + (ContextSet.levels ctx.local) (named, 0) in named @@ -187,9 +187,9 @@ let drop_weak_constraints = let process_universe_constraints ctx cstrs = let open UnivSubst in let open UnivProblem in - let univs = ctx.uctx_universes in - let vars = ref ctx.uctx_univ_variables in - let weak = ref ctx.uctx_weak_constraints in + let univs = ctx.universes in + let vars = ref ctx.univ_variables in + let weak = ref ctx.weak_constraints in let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) @@ -223,7 +223,7 @@ let process_universe_constraints ctx cstrs = let equalize_universes l r local = match varinfo l, varinfo r with | Inr l', Inr r' -> equalize_variables false l l' r r' local | Inr l, Inl r | Inl r, Inr l -> - let alg = LSet.mem l ctx.uctx_univ_algebraic in + let alg = LSet.mem l ctx.univ_algebraic in let inst = univ_level_rem l r r in if alg && not (LSet.mem l (Universe.levels inst)) then (instantiate_variable l inst vars; local) @@ -284,7 +284,7 @@ let process_universe_constraints ctx cstrs = !vars, !weak, local let add_constraints ctx cstrs = - let univs, local = ctx.uctx_local in + let univs, local = ctx.local in let cstrs' = Constraint.fold (fun (l,d,r) acc -> let l = Universe.make l and r = Universe.make r in let cstr' = let open UnivProblem in @@ -298,25 +298,25 @@ let add_constraints ctx cstrs = in let vars, weak, local' = process_universe_constraints ctx cstrs' in { ctx with - uctx_local = (univs, Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; - uctx_weak_constraints = weak; } + local = (univs, Constraint.union local local'); + univ_variables = vars; + universes = UGraph.merge_constraints local' ctx.universes; + weak_constraints = weak; } (* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = - let univs, local = ctx.uctx_local in + let univs, local = ctx.local in let vars, weak, local' = process_universe_constraints ctx cstrs in { ctx with - uctx_local = (univs, Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; - uctx_weak_constraints = weak; } + local = (univs, Constraint.union local local'); + univ_variables = vars; + universes = UGraph.merge_constraints local' ctx.universes; + weak_constraints = weak; } let constrain_variables diff ctx = - let univs, local = ctx.uctx_local in + let univs, local = ctx.local in let univs, vars, local = LSet.fold (fun l (univs, vars, cstrs) -> @@ -328,12 +328,12 @@ let constrain_variables diff ctx = Constraint.add (l, Eq, Option.get (Universe.level u)) cstrs) | None -> (univs, vars, cstrs) with Not_found | Option.IsNone -> (univs, vars, cstrs)) - diff (univs, ctx.uctx_univ_variables, local) + diff (univs, ctx.univ_variables, local) in - { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + { ctx with local = (univs, local); univ_variables = vars } let qualid_of_level uctx = - let map, map_rev = uctx.uctx_names in + let map, map_rev = uctx.names in fun l -> try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> @@ -364,7 +364,7 @@ let error_unbound_universes left uctx = let loc = try let info = - LMap.find (LSet.choose left) (snd uctx.uctx_names) in + LMap.find (LSet.choose left) (snd uctx.names) in info.uloc with Not_found -> None in @@ -375,12 +375,12 @@ let error_unbound_universes left uctx = str" unbound.")) let universe_context ~names ~extensible uctx = - let levels = ContextSet.levels uctx.uctx_local in + let levels = ContextSet.levels uctx.local in let newinst, left = List.fold_right (fun { CAst.loc; v = id } (newinst, acc) -> let l = - try UNameMap.find id (fst uctx.uctx_names) + try UNameMap.find id (fst uctx.names) with Not_found -> assert false in (l :: newinst, LSet.remove l acc)) names ([], levels) @@ -391,7 +391,7 @@ let universe_context ~names ~extensible uctx = let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in let inst = Array.append (Array.of_list newinst) left in let inst = Instance.of_array inst in - let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in + let ctx = UContext.make (inst, ContextSet.constraints uctx.local) in ctx let check_universe_context_set ~names ~extensible uctx = @@ -399,10 +399,10 @@ let check_universe_context_set ~names ~extensible uctx = else let left = List.fold_left (fun left { CAst.loc; v = id } -> let l = - try UNameMap.find id (fst uctx.uctx_names) + try UNameMap.find id (fst uctx.names) with Not_found -> assert false in LSet.remove l left) - (ContextSet.levels uctx.uctx_local) names + (ContextSet.levels uctx.local) names in if not (LSet.is_empty left) then error_unbound_universes left uctx @@ -423,26 +423,26 @@ let check_mono_univ_decl uctx decl = if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints - (ContextSet.constraints uctx.uctx_local); - uctx.uctx_local + (ContextSet.constraints uctx.local); + uctx.local let check_univ_decl ~poly uctx decl = let ctx = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in if poly then - let (binders, _) = uctx.uctx_names in + let (binders, _) = uctx.names in let uctx = universe_context ~names ~extensible uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in - Entries.Monomorphic_entry uctx.uctx_local + Entries.Monomorphic_entry uctx.local in if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints - (ContextSet.constraints uctx.uctx_local); + (ContextSet.constraints uctx.local); ctx let is_bound l lbound = match lbound with @@ -465,12 +465,12 @@ let restrict_universe_context ~lbound (univs, csts) keep = (LSet.inter univs keep, csts) let restrict ctx vars = - let vars = LSet.union vars ctx.uctx_seff_univs in + let vars = LSet.union vars ctx.seff_univs in let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) - (fst ctx.uctx_names) vars + (fst ctx.names) vars in - let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in - { ctx with uctx_local = uctx' } + let uctx' = restrict_universe_context ~lbound:ctx.universes_lbound ctx.local vars in + { ctx with local = uctx' } type rigid = | UnivRigid @@ -496,20 +496,20 @@ let merge ?loc ~sideff rigid uctx ctx' = if LMap.mem u accu then accu else LMap.add u None accu in - let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in + let uvars' = LSet.fold fold levels uctx.univ_variables in if b then - { uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } - else { uctx with uctx_univ_variables = uvars' } + { uctx with univ_variables = uvars'; + univ_algebraic = LSet.union uctx.univ_algebraic levels } + else { uctx with univ_variables = uvars' } in - let uctx_local = ContextSet.append ctx' uctx.uctx_local in + let local = ContextSet.append ctx' uctx.local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g + try UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u g with UGraph.AlreadyDeclared when sideff -> g) levels g in - let uctx_names = + let names = let fold u accu = let modify _ info = match info.uloc with | None -> { info with uloc = loc } @@ -518,20 +518,20 @@ let merge ?loc ~sideff rigid uctx ctx' = try LMap.modify u modify accu with Not_found -> LMap.add u { uname = None; uloc = loc } accu in - (fst uctx.uctx_names, LSet.fold fold levels (snd uctx.uctx_names)) + (fst uctx.names, LSet.fold fold levels (snd uctx.names)) in - let initial = declare uctx.uctx_initial_universes in - let univs = declare uctx.uctx_universes in - let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_names; uctx_local; uctx_universes; - uctx_initial_universes = initial } + let initial = declare uctx.initial_universes in + let univs = declare uctx.universes in + let universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in + { uctx with names; local; universes; + initial_universes = initial } let merge_subst uctx s = - { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s } + { uctx with univ_variables = LMap.subst_union uctx.univ_variables s } let demote_seff_univs univs uctx = - let seff = LSet.union uctx.uctx_seff_univs univs in - { uctx with uctx_seff_univs = seff } + let seff = LSet.union uctx.seff_univs univs in + { uctx with seff_univs = seff } let demote_global_univs env uctx = let env_ugraph = Environ.universes env in @@ -539,21 +539,21 @@ let demote_global_univs env uctx = let global_constraints, _ = UGraph.constraints_of_universes env_ugraph in let promoted_uctx = ContextSet.(of_set global_univs |> add_constraints global_constraints) in - { uctx with uctx_local = ContextSet.diff uctx.uctx_local promoted_uctx } + { uctx with local = ContextSet.diff uctx.local promoted_uctx } let merge_seff uctx ctx' = let levels = ContextSet.levels ctx' in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g + try UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u g with UGraph.AlreadyDeclared -> g) levels g in - let initial = declare uctx.uctx_initial_universes in - let univs = declare uctx.uctx_universes in - let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_universes; - uctx_initial_universes = initial } + let initial = declare uctx.initial_universes in + let univs = declare uctx.universes in + let universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in + { uctx with universes; + initial_universes = initial } let emit_side_effects eff u = let uctx = Safe_typing.universes_of_private eff in @@ -564,13 +564,13 @@ let update_sigma_env uctx env = let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in let eunivs = { uctx with - uctx_initial_universes = univs; - uctx_universes = univs } + initial_universes = univs; + universes = univs } in - merge_seff eunivs eunivs.uctx_local + merge_seff eunivs eunivs.local let new_univ_variable ?loc rigid name - ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = + ({ local = ctx; univ_variables = uvars; univ_algebraic = avars} as uctx) = let u = UnivGen.fresh_level () in let ctx' = ContextSet.add_universe u ctx in let uctx', pred = @@ -578,23 +578,23 @@ let new_univ_variable ?loc rigid name | UnivRigid -> uctx, true | UnivFlexible b -> let uvars' = LMap.add u None uvars in - if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = LSet.add u avars}, false - else {uctx with uctx_univ_variables = uvars'}, false + if b then {uctx with univ_variables = uvars'; + univ_algebraic = LSet.add u avars}, false + else {uctx with univ_variables = uvars'}, false in let names = match name with - | Some n -> add_uctx_names ?loc n u uctx.uctx_names - | None -> add_uctx_loc u loc uctx.uctx_names + | Some n -> add_names ?loc n u uctx.names + | None -> add_loc u loc uctx.names in let initial = - UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes + UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u uctx.initial_universes in let uctx' = - {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false - u uctx.uctx_universes; - uctx_initial_universes = initial} + {uctx' with names = names; local = ctx'; + universes = UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false + u uctx.universes; + initial_universes = initial} in uctx', u let make_with_initial_binders ~lbound e us = @@ -606,23 +606,23 @@ let make_with_initial_binders ~lbound e us = let add_global_univ uctx u = let initial = - UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_initial_universes + UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.initial_universes in let univs = - UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_universes + UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.universes in - { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; - uctx_initial_universes = initial; - uctx_universes = univs } + { uctx with local = ContextSet.add_universe u uctx.local; + initial_universes = initial; + universes = univs } let make_flexible_variable ctx ~algebraic u = - let {uctx_local = cstrs; uctx_univ_variables = uvars; - uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in + let {local = cstrs; univ_variables = uvars; + univ_algebraic = avars; universes=g; } = ctx in assert (try LMap.find u uvars == None with Not_found -> true); match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with | Some v -> let uvars' = LMap.add u (Some (Universe.make v)) uvars in - { ctx with uctx_univ_variables = uvars'; } + { ctx with univ_variables = uvars'; } | None -> let uvars' = LMap.add u None uvars in let avars' = @@ -640,21 +640,21 @@ let make_flexible_variable ctx ~algebraic u = then LSet.add u avars else avars else avars in - {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'} + {ctx with univ_variables = uvars'; + univ_algebraic = avars'} let make_nonalgebraic_variable ctx u = - { ctx with uctx_univ_algebraic = LSet.remove u ctx.uctx_univ_algebraic } + { ctx with univ_algebraic = LSet.remove u ctx.univ_algebraic } let make_flexible_nonalgebraic ctx = - {ctx with uctx_univ_algebraic = LSet.empty} + {ctx with univ_algebraic = LSet.empty} let is_sort_variable uctx s = match s with | Sorts.Type u -> (match universe_level u with | Some l as x -> - if LSet.mem l (ContextSet.levels uctx.uctx_local) then x + if LSet.mem l (ContextSet.levels uctx.local) then x else None | None -> None) | _ -> None @@ -682,88 +682,88 @@ let refresh_constraints univs (ctx, cstrs) = let normalize_variables uctx = let normalized_variables, def, subst = - UnivSubst.normalize_univ_variables uctx.uctx_univ_variables + UnivSubst.normalize_univ_variables uctx.univ_variables in - let ctx_local = subst_univs_context_with_def def (make_subst subst) uctx.uctx_local in - let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in - subst, { uctx with uctx_local = ctx_local'; - uctx_univ_variables = normalized_variables; - uctx_universes = univs } + let ctx_local = subst_univs_context_with_def def (make_subst subst) uctx.local in + let ctx_local', univs = refresh_constraints uctx.initial_universes ctx_local in + subst, { uctx with local = ctx_local'; + univ_variables = normalized_variables; + universes = univs } let abstract_undefined_variables uctx = let vars' = LMap.fold (fun u v acc -> if v == None then LSet.remove u acc else acc) - uctx.uctx_univ_variables uctx.uctx_univ_algebraic - in { uctx with uctx_local = ContextSet.empty; - uctx_univ_algebraic = vars' } + uctx.univ_variables uctx.univ_algebraic + in { uctx with local = ContextSet.empty; + univ_algebraic = vars' } let fix_undefined_variables uctx = let algs', vars' = LMap.fold (fun u v (algs, vars as acc) -> if v == None then (LSet.remove u algs, LMap.remove u vars) else acc) - uctx.uctx_univ_variables - (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) + uctx.univ_variables + (uctx.univ_algebraic, uctx.univ_variables) in - { uctx with uctx_univ_variables = vars'; - uctx_univ_algebraic = algs' } + { uctx with univ_variables = vars'; + univ_algebraic = algs' } let refresh_undefined_univ_variables uctx = - let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in let subst_fn u = subst_univs_level_level subst u in let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc) - uctx.uctx_univ_algebraic LSet.empty + uctx.univ_algebraic LSet.empty in let vars = LMap.fold (fun u v acc -> LMap.add (subst_fn u) (Option.map (subst_univs_level_universe subst) v) acc) - uctx.uctx_univ_variables LMap.empty + uctx.univ_variables LMap.empty in - let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let lbound = uctx.uctx_universes_lbound in + let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in + let lbound = uctx.universes_lbound in let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) (ContextSet.levels ctx') g in - let initial = declare uctx.uctx_initial_universes in + let initial = declare uctx.initial_universes in let univs = declare UGraph.initial_universes in - let uctx' = {uctx_names = uctx.uctx_names; - uctx_local = ctx'; - uctx_seff_univs = uctx.uctx_seff_univs; - uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = univs; - uctx_universes_lbound = lbound; - uctx_initial_universes = initial; - uctx_weak_constraints = weak; } in + let uctx' = {names = uctx.names; + local = ctx'; + seff_univs = uctx.seff_univs; + univ_variables = vars; univ_algebraic = alg; + universes = univs; + universes_lbound = lbound; + initial_universes = initial; + weak_constraints = weak; } in uctx', subst let minimize uctx = let open UnivMinim in - let lbound = uctx.uctx_universes_lbound in + let lbound = uctx.universes_lbound in let ((vars',algs'), us') = - normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic uctx.uctx_weak_constraints + normalize_context_set ~lbound uctx.universes uctx.local uctx.univ_variables + uctx.univ_algebraic uctx.weak_constraints in - if ContextSet.equal us' uctx.uctx_local then uctx + if ContextSet.equal us' uctx.local then uctx else let us', universes = - refresh_constraints uctx.uctx_initial_universes us' + refresh_constraints uctx.initial_universes us' in - { uctx_names = uctx.uctx_names; - uctx_local = us'; - uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *) - uctx_univ_variables = vars'; - uctx_univ_algebraic = algs'; - uctx_universes = universes; - uctx_universes_lbound = lbound; - uctx_initial_universes = uctx.uctx_initial_universes; - uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } + { names = uctx.names; + local = us'; + seff_univs = uctx.seff_univs; (* not sure about this *) + univ_variables = vars'; + univ_algebraic = algs'; + universes = universes; + universes_lbound = lbound; + initial_universes = uctx.initial_universes; + weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } let universe_of_name uctx s = - UNameMap.find s (fst uctx.uctx_names) + UNameMap.find s (fst uctx.names) -let pr_weak prl {uctx_weak_constraints=weak} = +let pr_weak prl {weak_constraints=weak} = let open Pp in prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak) diff --git a/kernel/section.ml b/kernel/section.ml index 8c36f16799..c285b31b70 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -21,31 +21,31 @@ type section_entry = type 'a entry_map = 'a Cmap.t * 'a Mindmap.t type 'a t = { - sec_prev : 'a t option; + prev : 'a t option; (** Section surrounding the current one *) - sec_context : int; + context : int; (** Length of the named context suffix that has been introduced locally *) - sec_mono_universes : ContextSet.t; - sec_poly_universes : Name.t array * UContext.t; + mono_universes : ContextSet.t; + poly_universes : Name.t array * UContext.t; (** Universes local to the section *) all_poly_univs : Univ.Level.t array; (** All polymorphic universes, including from previous sections. *) has_poly_univs : bool; (** Are there polymorphic universes or constraints, including in previous sections. *) - sec_entries : section_entry list; + entries : section_entry list; (** Definitions introduced in the section *) - sec_data : (Instance.t * AUContext.t) entry_map; + data : (Instance.t * AUContext.t) entry_map; (** Additional data synchronized with the section *) - sec_custom : 'a; + custom : 'a; } -let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth prev +let rec depth sec = 1 + match sec.prev with None -> 0 | Some prev -> depth prev let has_poly_univs sec = sec.has_poly_univs let all_poly_univs sec = sec.all_poly_univs -let map_custom f sec = {sec with sec_custom = f sec.sec_custom} +let map_custom f sec = {sec with custom = f sec.custom} let find_emap e (cmap, imap) = match e with | SecDefinition con -> Cmap.find con cmap @@ -56,22 +56,22 @@ let add_emap e v (cmap, imap) = match e with | SecInductive ind -> (cmap, Mindmap.add ind v imap) let push_local sec = - { sec with sec_context = sec.sec_context + 1 } + { sec with context = sec.context + 1 } let push_context (nas, ctx) sec = if UContext.is_empty ctx then sec else - let (snas, sctx) = sec.sec_poly_universes in - let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in + let (snas, sctx) = sec.poly_universes in + let poly_universes = (Array.append snas nas, UContext.union sctx ctx) in let all_poly_univs = Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx) in - { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true } + { sec with poly_universes; all_poly_univs; has_poly_univs = true } let rec is_polymorphic_univ u sec = - let (_, uctx) = sec.sec_poly_universes in + let (_, uctx) = sec.poly_universes in let here = Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) in - here || Option.cata (is_polymorphic_univ u) false sec.sec_prev + here || Option.cata (is_polymorphic_univ u) false sec.prev let push_constraints uctx sec = if sec.has_poly_univs && @@ -80,25 +80,25 @@ let push_constraints uctx sec = (snd uctx) then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes."); - let uctx' = sec.sec_mono_universes in - let sec_mono_universes = (ContextSet.union uctx uctx') in - { sec with sec_mono_universes } + let uctx' = sec.mono_universes in + let mono_universes = (ContextSet.union uctx uctx') in + { sec with mono_universes } -let open_section ~custom sec_prev = +let open_section ~custom prev = { - sec_prev; - sec_context = 0; - sec_mono_universes = ContextSet.empty; - sec_poly_universes = ([||], UContext.empty); - all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev; - has_poly_univs = Option.cata has_poly_univs false sec_prev; - sec_entries = []; - sec_data = (Cmap.empty, Mindmap.empty); - sec_custom = custom; + prev; + context = 0; + mono_universes = ContextSet.empty; + poly_universes = ([||], UContext.empty); + all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] prev; + has_poly_univs = Option.cata has_poly_univs false prev; + entries = []; + data = (Cmap.empty, Mindmap.empty); + custom = custom; } let close_section sec = - sec.sec_prev, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom + sec.prev, sec.entries, sec.mono_universes, sec.custom let make_decl_univs (nas,uctx) = abstract_universes nas uctx @@ -109,8 +109,8 @@ let push_global ~poly e sec = section polymorphic universes are present.") else { sec with - sec_entries = e :: sec.sec_entries; - sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data; + entries = e :: sec.entries; + data = add_emap e (make_decl_univs sec.poly_universes) sec.data; } let push_constant ~poly con s = push_global ~poly (SecDefinition con) s @@ -131,7 +131,7 @@ let empty_segment = { let extract_hyps sec vars used = (* Keep the section-local segment of variables *) - let vars = List.firstn sec.sec_context vars in + let vars = List.firstn sec.context vars in (* Only keep the part that is used by the declaration *) List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars @@ -139,7 +139,7 @@ let section_segment_of_entry vars e hyps sec = (* [vars] are the named hypotheses, [hyps] the subset that is declared by the global *) let hyps = extract_hyps sec vars hyps in - let inst, auctx = find_emap e sec.sec_data in + let inst, auctx = find_emap e sec.data in { abstr_ctx = hyps; abstr_subst = inst; @@ -166,7 +166,7 @@ let extract_worklist info = info.abstr_subst, args let replacement_context env sec = - let cmap, imap = sec.sec_data in + let cmap, imap = sec.data in let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con sec) cmap in let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind sec) imap in (cmap, imap) @@ -175,9 +175,9 @@ let is_in_section env gr sec = let open GlobRef in match gr with | VarRef id -> - let vars = List.firstn sec.sec_context (Environ.named_context env) in + let vars = List.firstn sec.context (Environ.named_context env) in List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars | ConstRef con -> - Cmap.mem con (fst sec.sec_data) + Cmap.mem con (fst sec.data) | IndRef (ind, _) | ConstructRef ((ind, _), _) -> - Mindmap.mem ind (snd sec.sec_data) + Mindmap.mem ind (snd sec.data) diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index 48b6abf441..cb226de586 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -165,18 +165,6 @@ END (** Split *) -{ - -let rec delayed_list = function -| [] -> fun _ sigma -> (sigma, []) -| x :: l -> - fun env sigma -> - let (sigma, x) = x env sigma in - let (sigma, l) = delayed_list l env sigma in - (sigma, x :: l) - -} - TACTIC EXTEND split | [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] } END @@ -199,16 +187,12 @@ END TACTIC EXTEND exists | [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] } -| [ "exists" ne_bindings_list_sep(bll, ",") ] -> { - Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) - } +| [ "exists" ne_bindings_list_sep(bll, ",") ] -> { Tactics.split_with_delayed_bindings false bll } END TACTIC EXTEND eexists | [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] } -| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> { - Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) - } +| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> { Tactics.split_with_delayed_bindings true bll } END (** Intro *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5fe87a94c5..315c42097d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2265,6 +2265,10 @@ let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 let split_with_bindings with_evars l = Tacticals.New.tclMAP (constructor_tac with_evars (Some 1) 1) l +let split_with_delayed_bindings with_evars = + Tacticals.New.tclMAP (fun bl -> + Tacticals.New.tclDELAYEDWITHHOLES with_evars bl + (constructor_tac with_evars (Some 1) 1)) let left = left_with_bindings false let simplest_left = left NoBindings diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b6eb48a3d9..5b397b15d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -337,6 +337,7 @@ val split : constr bindings -> unit Proofview.tactic val left_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic val right_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic val split_with_bindings : evars_flag -> constr bindings list -> unit Proofview.tactic +val split_with_delayed_bindings : evars_flag -> constr bindings delayed_open list -> unit Proofview.tactic val simplest_left : unit Proofview.tactic val simplest_right : unit Proofview.tactic diff --git a/test-suite/bugs/closed/bug_12365.v b/test-suite/bugs/closed/bug_12365.v new file mode 100644 index 0000000000..a8e2bb459d --- /dev/null +++ b/test-suite/bugs/closed/bug_12365.v @@ -0,0 +1,8 @@ +Parameter a b : nat. +Parameter p : a = b. + +Goal exists (_ : True) (_ : exists x, x = b), True. +Proof. + exists I, (ex_intro _ a p). + exact I. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh new file mode 100755 index 0000000000..4a50759bdb --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log + +diff -u time-of-build-both.log.expected time-of-build-both.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in new file mode 100644 index 0000000000..1031cb85c5 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in @@ -0,0 +1,58 @@ +./src/Rewriter/PerfTesting/Specific/make.py primes.txt +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq +COQ_MAKEFILE -f _CoqProject > Makefile.coq +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +COQDEP VFILES +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +COQC src/UnsaturatedSolinasHeuristics/Tests.v +Finished transaction in 25.269 secs (24.869u,0.051s) (successful) +src/UnsaturatedSolinasHeuristics/Tests.vo (real: 26.27, user: 25.97, sys: 0.27, mem: 566428 ko) +DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256 +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions +DIFF Crypto.Fancy.Montgomery256.montred256 +DIFF Crypto.Fancy.Barrett256.Prod.MulMod +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions +DIFF Crypto.Fancy.Barrett256.barrett_red256 +DIFF Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs +cp -f AUTHORS fiat-rust/AUTHORS +cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS +cp -f LICENSE fiat-rust/LICENSE diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in new file mode 100644 index 0000000000..b78039b589 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in @@ -0,0 +1,40 @@ +./src/Rewriter/PerfTesting/Specific/make.py primes.txt +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq +COQ_MAKEFILE -f _CoqProject > Makefile.coq +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256 +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions +DIFF Crypto.Fancy.Montgomery256.montred256 +DIFF Crypto.Fancy.Barrett256.Prod.MulMod +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions +DIFF Crypto.Fancy.Barrett256.barrett_red256 +cp -f AUTHORS fiat-rust/AUTHORS +cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS +cp -f LICENSE fiat-rust/LICENSE diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected new file mode 100644 index 0000000000..6a232623bf --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected @@ -0,0 +1,5 @@ + After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) +------------------------------------------------------------------------------------------------------------------------------------------- +0m25.96s | 566428 ko | Total Time / Peak Mem | 0m00.00s | 0 ko || +0m25.96s || 566428 ko | N/A | ∞ +------------------------------------------------------------------------------------------------------------------------------------------- +0m25.97s | 566428 ko | UnsaturatedSolinasHeuristics/Tests.vo | N/A | N/A || +0m25.96s || 566428 ko | ∞ | ∞ diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index 8935759705..123b272a69 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -12,3 +12,4 @@ export COQLIB ./003-non-utf8/run.sh ./004-per-file-fuzz/run.sh ./005-correct-diff-sorting-order-mem/run.sh +./006-zero-before/run.sh diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a3078af4a1..12462726e5 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -387,8 +387,8 @@ def make_diff_table_string(left_dict, right_dict, total_string = 'Total' if not include_mem else 'Total Time / Peak Mem' middle_width = max(map(len, names + [tag, total_string])) - left_peak = max(v.get(MEM_KEY, 0) for v in left_dict.values()) - right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) + left_peak = max([0] + [v.get(MEM_KEY, 0) for v in left_dict.values()]) + right_peak = max([0] + [v.get(MEM_KEY, 0) for v in right_dict.values()]) diff_peak = left_peak - right_peak percent_diff_peak = (format_percentage((left_peak - right_peak) / float(right_peak)) if right_peak != 0 else (INFINITY if left_peak > 0 else 'N/A')) |