aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/02-specification-language/07825-rechable-from-evars.rst9
-rw-r--r--engine/evarutil.ml21
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/evd.ml171
-rw-r--r--engine/evd.mli8
-rw-r--r--engine/proofview_monad.ml5
-rw-r--r--engine/proofview_monad.mli6
-rw-r--r--engine/termops.ml8
-rw-r--r--proofs/refine.ml2
-rw-r--r--tactics/tacticals.ml9
-rw-r--r--tactics/tactics.ml14
-rw-r--r--test-suite/bugs/closed/bug_4413.v8
-rw-r--r--test-suite/bugs/closed/bug_7825.v50
13 files changed, 212 insertions, 107 deletions
diff --git a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst
new file mode 100644
index 0000000000..e57d5a7bc5
--- /dev/null
+++ b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+ In :tacn:`refine`, new existential variables unified with existing ones are no
+ longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on
+ the orientation of evar-evar unification problems, and new existential variables
+ are always turned into (unshelved) goals. This can break compatibility in
+ some cases (`#7825 <https://github.com/coq/coq/pull/7825>`_, by Matthieu
+ Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and
+ Enrico Tassi, fixes `#4095 <https://github.com/coq/coq/issues/4095>`_ and
+ `#4413 <https://github.com/coq/coq/issues/4413>`_).
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index d719731464..771571fd3f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -516,12 +516,7 @@ let restrict_evar evd evk filter ?src candidates =
let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in
match candidates with
| Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
- | _ ->
- let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
- (* Mark new evar as future goal, removing previous one,
- circumventing Proofview.advance but making Proof.run_tactic catch these. *)
- let evd = Evd.remove_future_goal evd evk in
- (Evd.declare_future_goal evk' evd, evk')
+ | _ -> Evd.restrict evk filter ?candidates ?src evd
let rec check_and_clear_in_constr env evdref err ids global c =
(* returns a new constr where all the evars have been 'cleaned'
@@ -703,10 +698,22 @@ let rec advance sigma evk =
match evi.evar_body with
| Evar_empty -> Some evk
| Evar_defined v ->
- match is_restricted_evar sigma evk with
+ match is_aliased_evar sigma evk with
| Some evk -> advance sigma evk
| None -> None
+let reachable_from_evars sigma evars =
+ let aliased = Evd.get_aliased_evars sigma in
+ let rec search evk visited =
+ if Evar.Set.mem evk visited then visited
+ else
+ let visited = Evar.Set.add evk visited in
+ match Evar.Map.find evk aliased with
+ | evk' -> search evk' visited
+ | exception Not_found -> visited
+ in
+ Evar.Set.fold (fun evk visited -> search evk visited) evars Evar.Set.empty
+
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 9d2c29547e..6e1f67021f 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -112,6 +112,10 @@ val gather_dependent_evars : evar_map -> Evar.t list -> (Evar.Set.t option) Evar
solved. *)
val advance : evar_map -> Evar.t -> Evar.t option
+(** [reachable_from_evars sigma seeds] computes the descendents of
+ evars in [seeds] by restriction or evar-evar unifications in [sigma]. *)
+val reachable_from_evars : evar_map -> Evar.Set.t -> Evar.Set.t
+
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
@@ -234,8 +238,8 @@ exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t opti
(** Restrict an undefined evar according to a (sub)filter and candidates.
The evar will be defined if there is only one candidate left,
-@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates
- into an empty list. *)
+ @raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates
+ into an empty list. *)
val restrict_evar : evar_map -> Evar.t -> Filter.t ->
?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
diff --git a/engine/evd.ml b/engine/evd.ml
index 65df2643f2..4ae1d034d7 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -453,7 +453,7 @@ end
type evar_flags =
{ obligation_evars : Evar.Set.t;
- restricted_evars : Evar.t Evar.Map.t;
+ aliased_evars : Evar.t Evar.Map.t;
typeclass_evars : Evar.Set.t }
type side_effect_role =
@@ -631,7 +631,7 @@ let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body
associated to an evar, so we prevent registering its typeclass status. *)
let add d e i = add_with_name ~typeclass_candidate:false d e i
-(*** Evar flags: typeclasses, restricted or obligation flag *)
+(*** Evar flags: typeclasses, aliased or obligation flag *)
let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
@@ -659,29 +659,28 @@ let is_obligation_evar evd evk =
let inherit_evar_flags evar_flags evk evk' =
let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
- if not (evk_obligation || evk_typeclass) then evar_flags
- else
- let typeclass_evars =
- if evk_typeclass then
- let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
- Evar.Set.add evk' typeclass_evars
- else evar_flags.typeclass_evars
- in
- let obligation_evars =
- if evk_obligation then
- let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
- Evar.Set.add evk' obligation_evars
- else evar_flags.obligation_evars
- in
- { evar_flags with obligation_evars; typeclass_evars }
+ let aliased_evars = Evar.Map.add evk evk' evar_flags.aliased_evars in
+ let typeclass_evars =
+ if evk_typeclass then
+ let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+ Evar.Set.add evk' typeclass_evars
+ else evar_flags.typeclass_evars
+ in
+ let obligation_evars =
+ if evk_obligation then
+ let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+ Evar.Set.add evk' obligation_evars
+ else evar_flags.obligation_evars
+ in
+ { obligation_evars; aliased_evars; typeclass_evars }
(** Removal: in all other cases of definition *)
let remove_evar_flags evk evar_flags =
{ typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
- (* Restriction information is kept. *)
- restricted_evars = evar_flags.restricted_evars }
+ (* Aliasing information is kept. *)
+ aliased_evars = evar_flags.aliased_evars }
(** New evars *)
@@ -809,7 +808,7 @@ let create_evar_defs sigma = { sigma with
let empty_evar_flags =
{ obligation_evars = Evar.Set.empty;
- restricted_evars = Evar.Map.empty;
+ aliased_evars = Evar.Map.empty;
typeclass_evars = Evar.Set.empty }
let empty_side_effects = {
@@ -872,71 +871,12 @@ let evar_source evk d = (find d evk).evar_source
let evar_ident evk evd = EvNames.ident evk evd.evar_names
let evar_key id evd = EvNames.key id evd.evar_names
-let define_aux def undef evk body =
- let oldinfo =
- try EvMap.find evk undef
- with Not_found ->
- if EvMap.mem evk def then
- anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
- else
- anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
- in
- let () = assert (oldinfo.evar_body == Evar_empty) in
- let newinfo = { oldinfo with evar_body = Evar_defined body } in
- EvMap.add evk newinfo def, EvMap.remove evk undef
-
-(* define the existential of section path sp as the constr body *)
-let define_gen evk body evd evar_flags =
- let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
- let last_mods = match evd.conv_pbs with
- | [] -> evd.last_mods
- | _ -> Evar.Set.add evk evd.last_mods
- in
- let evar_names = EvNames.remove_name_defined evk evd.evar_names in
- { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+let get_aliased_evars evd = evd.evar_flags.aliased_evars
-(** By default, the obligation and evar tag of the evar is removed *)
-let define evk body evd =
- let evar_flags = remove_evar_flags evk evd.evar_flags in
- define_gen evk body evd evar_flags
-
-(** In case of an evar-evar solution, the flags are inherited *)
-let define_with_evar evk body evd =
- let evk' = fst (destEvar body) in
- let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
- define_gen evk body evd evar_flags
-
-let is_restricted_evar evd evk =
- try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+let is_aliased_evar evd evk =
+ try Some (Evar.Map.find evk evd.evar_flags.aliased_evars)
with Not_found -> None
-let declare_restricted_evar evar_flags evk evk' =
- { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
-
-(* In case of restriction, we declare the restriction and inherit the obligation
- and typeclass flags. *)
-
-let restrict evk filter ?candidates ?src evd =
- let evk' = new_untyped_evar () in
- let evar_info = EvMap.find evk evd.undf_evars in
- let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
- let evar_info' =
- { evar_info with evar_filter = filter;
- evar_candidates = candidates;
- evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
- evar_identity = Identity.make id_inst;
- } in
- let last_mods = match evd.conv_pbs with
- | [] -> evd.last_mods
- | _ -> Evar.Set.add evk evd.last_mods in
- let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
- let body = mkEvar(evk',id_inst) in
- let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
- let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
- let evar_flags = inherit_evar_flags evar_flags evk evk' in
- { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
- defn_evars; last_mods; evar_names; evar_flags }, evk'
-
let downcast evk ccl evd =
let evar_info = EvMap.find evk evd.undf_evars in
let evar_info' = { evar_info with evar_concl = ccl } in
@@ -1224,6 +1164,73 @@ let pr_shelf evd =
if List.is_empty evd.shelf then str"(empty stack)"
else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf
+let define_aux def undef evk body =
+ let oldinfo =
+ try EvMap.find evk undef
+ with Not_found ->
+ if EvMap.mem evk def then
+ anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
+ else
+ anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
+ in
+ let () = assert (oldinfo.evar_body == Evar_empty) in
+ let newinfo = { oldinfo with evar_body = Evar_defined body } in
+ EvMap.add evk newinfo def, EvMap.remove evk undef
+
+(* define the existential of section path sp as the constr body *)
+let define_gen evk body evd evar_flags =
+ let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+ let last_mods = match evd.conv_pbs with
+ | [] -> evd.last_mods
+ | _ -> Evar.Set.add evk evd.last_mods
+ in
+ let evar_names = EvNames.remove_name_defined evk evd.evar_names in
+ { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+ let evar_flags = remove_evar_flags evk evd.evar_flags in
+ define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+ let evk' = fst (destEvar body) in
+ let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+ let evd = unshelve evd [evk] in
+ let future_goals = FutureGoals.remove evk evd.future_goals in
+ let evd = { evd with future_goals } in
+ define_gen evk body evd evar_flags
+
+(* In case of restriction, we declare the aliasing and inherit the obligation
+ and typeclass flags. *)
+
+let restrict evk filter ?candidates ?src evd =
+ let evk' = new_untyped_evar () in
+ let evar_info = EvMap.find evk evd.undf_evars in
+ let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
+ let evar_info' =
+ { evar_info with evar_filter = filter;
+ evar_candidates = candidates;
+ evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
+ evar_identity = Identity.make id_inst;
+ } in
+ let last_mods = match evd.conv_pbs with
+ | [] -> evd.last_mods
+ | _ -> Evar.Set.add evk evd.last_mods in
+ let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
+ let body = mkEvar(evk',id_inst) in
+ let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+ let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+ let evd = { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
+ defn_evars; last_mods; evar_names; evar_flags }
+ in
+ (* Mark new evar as future goal, removing previous one,
+ circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+ let evd = unshelve evd [evk] in
+ let evd = remove_future_goal evd evk in
+ let evd = declare_future_goal evk' evd in
+ (evd, evk')
+
(**********************************************************)
(* Accessing metas *)
diff --git a/engine/evd.mli b/engine/evd.mli
index 9394f9a9dd..fafaad9a04 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -284,8 +284,11 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
possibly limiting the instances to a set of candidates (candidates
are filtered according to the filter) *)
-val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
-(** Tell if an evar comes from restriction of another evar, and if yes, which *)
+val get_aliased_evars : evar_map -> Evar.t Evar.Map.t
+(** The map of aliased evars *)
+
+val is_aliased_evar : evar_map -> Evar.t -> Evar.t option
+(** Tell if an evar has been aliased to another evar, and if yes, which *)
val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map
(** Mark the given set of evars as available for resolution.
@@ -388,7 +391,6 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map
val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
-
val remove_future_goal : evar_map -> Evar.t -> evar_map
val pr_future_goals_stack : evar_map -> Pp.t
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index df9fc5dab3..80263694f5 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -202,6 +202,11 @@ module type State = sig
val modify : (t->t) -> unit Logical.t
end
+module type Reader = sig
+ type t
+ val get : t Logical.t
+end
+
module type Writer = sig
type t
val put : t -> unit Logical.t
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 6cca3f5a5e..00d322858d 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -79,7 +79,7 @@ val with_empty_state : goal -> goal_with_state
val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
(** Type of proof views: current [evar_map] together with the list of
- focused goals. *)
+ focused goals, locally shelved goals and globally shelved goals. *)
type proofview = {
solution : Evd.evar_map;
comb : goal_with_state list;
@@ -115,6 +115,10 @@ module type State = sig
val set : t -> unit Logical.t
val modify : (t->t) -> unit Logical.t
end
+module type Reader = sig
+ type t
+ val get : t Logical.t
+end
module type Writer = sig
type t
diff --git a/engine/termops.ml b/engine/termops.ml
index ac6870a39e..0923ab6f4b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -310,15 +310,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
let pr_evar_list env sigma l =
let open Evd in
- let pr_restrict ev =
- match is_restricted_evar sigma ev with
+ let pr_alias ev =
+ match is_aliased_evar sigma ev with
| None -> mt ()
- | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")"
+ | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")"
in
let pr (ev, evi) =
h 0 (Evar.print ev ++
str "==" ++ pr_evar_info env sigma evi ++
- pr_restrict ev ++
+ pr_alias ev ++
(if evi.evar_body == Evar_empty
then str " {" ++ pr_existential_key sigma ev ++ str "}"
else mt ()))
diff --git a/proofs/refine.ml b/proofs/refine.ml
index dcff5e2b6c..ac410a958f 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -75,6 +75,8 @@ let generic_refine ~typecheck f gl =
let future_goals, sigma = Evd.pop_future_goals sigma in
(* Select the goals *)
let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in
+ let shelf = Evd.shelf sigma in
+ let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ List.mem ev shelf) future_goals in
(* Proceed to the refinement *)
let sigma = match Proofview.Unsafe.advance sigma self with
| None ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fc099f643d..c0fad0026f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -695,6 +695,8 @@ module New = struct
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma origsigma =
+ let reachable = lazy (Evarutil.reachable_from_evars sigma
+ (Evar.Map.domain (Evd.undefined_map origsigma))) in
let rec is_undefined_up_to_restriction sigma evk =
if Evd.mem origsigma evk then None else
let evi = Evd.find sigma evk in
@@ -710,7 +712,12 @@ module New = struct
let rest =
Evd.fold_undefined (fun evk evi acc ->
match is_undefined_up_to_restriction sigma evk with
- | Some (evk',evi) -> (evk',evi)::acc
+ | Some (evk',evi) ->
+ (* If [evk'] descends from [evk] which descends itself from
+ an originally undefined evar in [origsigma], it is a not
+ a fresh undefined hole from [sigma]. *)
+ if Evar.Set.mem evk (Lazy.force reachable) then acc
+ else (evk',evi)::acc
| _ -> acc)
extsigma []
in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5f7e35d205..1dded80d92 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5184,14 +5184,14 @@ end
(** Tacticals defined directly in term of Proofview *)
module New = struct
- open Genredexpr
- open Locus
-
let reduce_after_refine =
- reduce
- (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
- rZeta=false;rDelta=false;rConst=[]})
- {onhyps = Some []; concl_occs = AllOccurrences }
+ (* For backward compatibility reasons, we do not contract let-ins, but we unfold them. *)
+ let redfun env t =
+ let open CClosure in
+ let flags = RedFlags.red_add_transparent allnolet TransparentState.empty in
+ clos_norm_flags flags env t
+ in
+ reduct_in_concl ~check:false (redfun,DEFAULTcast)
let refine ~typecheck c =
Refine.refine ~typecheck c <*>
diff --git a/test-suite/bugs/closed/bug_4413.v b/test-suite/bugs/closed/bug_4413.v
new file mode 100644
index 0000000000..cb30aa5d1f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4413.v
@@ -0,0 +1,8 @@
+
+(* Regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems. *)
+Goal exists x, x=1 -> True.
+eexists. intro H.
+pose proof (f_equal (fun k => k) H).
+Undo.
+pose (@f_equal _ _ S _ _ H).
+Abort.
diff --git a/test-suite/bugs/closed/bug_7825.v b/test-suite/bugs/closed/bug_7825.v
new file mode 100644
index 0000000000..3f8708059a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7825.v
@@ -0,0 +1,50 @@
+Record T (x : nat) := { t : x = x }.
+
+Goal exists x, T x.
+ refine (ex_intro _ _ _).
+ Show Existentials.
+ simple refine {| t := _ |}.
+ reflexivity.
+ Unshelve. exact 0.
+Qed.
+
+(** Fine if the new evar is defined as the originally shelved evar: we do nothing.
+ In the other direction we promote the non-shelved new goal to a shelved one:
+ shelved status has priority over goal status. *)
+
+Goal forall a : nat, exists x, T x.
+ evar (x : nat). subst x. Show Existentials.
+ intros a. simple refine (ex_intro ?[x0] _ _). shelve. simpl.
+ (** Here ?x := ?x0 which is shelved, so ?x becomes shelved even if it would
+ not be by default (refine ?x and _ produce non-shelved evars by default)*)
+ simple refine (Build_T ?x _).
+ reflexivity.
+ Unshelve. exact 0.
+Qed.
+
+Goal { A : _ & { P : _ & @sigT A P } }.
+ epose _ as A;
+ epose _ as P;
+ exists A, P.
+ (* Regardless of which evars are in the goals vs the hypotheses,
+ [simple refine (existT _ _ _)] should leave over two goals. This
+ should be true even when chained with epose. *)
+ assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+ subst P;
+ assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+ subst A;
+ assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2).
+ (* fails *)
+Abort.
+
+Goal { A : _ & { P : _ & @sigT A P } }.
+ epose _ as A;
+ epose _ as P;
+ exists A, P; (* In this example we chain everything *)
+ assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+ subst P;
+ assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+ subst A;
+ assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2).
+ (* fails *)
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:28:39 +0000