aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/ring/ring.ml4
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/equality.ml79
-rw-r--r--tactics/equality.mli16
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1416.v7
-rw-r--r--test-suite/success/autorewrite.v (renamed from test-suite/success/autorewritein.v)6
-rw-r--r--test-suite/success/rewrite.v11
-rw-r--r--toplevel/auto_ind_decl.ml2
12 files changed, 90 insertions, 55 deletions
diff --git a/CHANGES b/CHANGES
index 10b0f09cf..90d8b604f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Tactics
- Unification in "apply" supports unification of patterns of the form
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification").
+- Tactic autorewrite does no longer instantiate pre-existing
+ existential variables (theoretical source of possible incompatibility).
Vernacular commands
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bba3f95fd..1d1e4a2a6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1416,7 +1416,7 @@ let rec rewrite_eqs_in_eqs eqs =
(fun id gl ->
observe_tac
(Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
- (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
+ (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false))
gl
)
eqs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5b689625b..9b1ccde2c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -373,7 +373,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
h_intros thin_intros;
tclMAP
- (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* deps proofs also: *) true teq eq false))
+ (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* deps proofs also: *) true teq eq false))
(List.rev eqs);
(fun g1 ->
let ty_teq = pf_type_of g1 (mkVar teq) in
@@ -534,7 +534,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
in
tclTHENS
(general_rewrite_bindings false Termops.all_occurrences
- (* dep proofs also: *) true
+ (* dep proofs also: *) true true
(mkVar eq,
ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
dummy_loc, NamedHyp def_id, mkVar def]) false)
@@ -1211,7 +1211,7 @@ let rec introduce_all_values_eq cont_tac functional termine
Nameops.out_name def_na
in
observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences
- (* dep proofs also: *) true (mkVar heq2,
+ true (* dep proofs also: *) true (mkVar heq2,
ExplicitBindings[dummy_loc,NamedHyp def_id,
f]) false) gls)
[tclTHENLIST
@@ -1266,7 +1266,7 @@ let rec introduce_all_values_eq cont_tac functional termine
f_S(mkVar pmax');
dummy_loc, NamedHyp def_id, f])
in
- observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences (* dep proofs also: *) true
+ observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences true (* dep proofs also: *) true
c_b false))
g
)
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 7588e6a2f..89309e323 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -820,9 +820,9 @@ let raw_polynom th op lc gl =
(tclTHENS
(tclORELSE
(Equality.general_rewrite true
- Termops.all_occurrences false c'i_eq_c''i)
+ Termops.all_occurrences true false c'i_eq_c''i)
(Equality.general_rewrite false
- Termops.all_occurrences false c'i_eq_c''i))
+ Termops.all_occurrences true false c'i_eq_c''i))
[tac]))
else
(tclORELSE
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 55e23d342..8ccf751c4 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -117,7 +117,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
tclTHEN tac
(one_base (fun dir c tac ->
let tac = tac, conds in
- general_rewrite dir all_occurrences false ~tac c)
+ general_rewrite dir all_occurrences true false ~tac c)
tac_main bas))
tclIDTAC lbas))
@@ -135,7 +135,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
| _ -> (* even the hypothesis id is missing *)
error ("No such hypothesis: " ^ (string_of_id !id) ^".")
in
- let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in
+ let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl in
let gls = gl'.Evd.it in
match gls with
g::_ ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3a40994f8..51265d723 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -64,6 +64,7 @@ let _ =
(* Rewriting tactics *)
type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
type orientation = bool
@@ -108,12 +109,15 @@ let freeze_initial_evars sigma flags clause =
sigma ExistentialSet.empty in
{ flags with Unification.frozen_evars = evars }
+let make_flags frzevars sigma flags clause =
+ if frzevars then freeze_initial_evars sigma flags clause else flags
+
let side_tac tac sidetac =
match sidetac with
| None -> tac
| Some sidetac -> tclTHENSFIRSTn tac [|tclIDTAC|] sidetac
-let instantiate_lemma_all env sigma gl c ty l l2r concl =
+let instantiate_lemma_all frzevars env sigma gl c ty l l2r concl =
let eqclause = Clenv.make_clenv_binding { gl with sigma = sigma } (c,ty) l in
let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
@@ -125,7 +129,7 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl =
let try_occ (evd', c') =
clenv_pose_dependent_evars true {eqclause with evd = evd'}
in
- let flags = freeze_initial_evars sigma rewrite_unif_flags eqclause in
+ let flags = make_flags frzevars sigma rewrite_unif_flags eqclause in
let occs =
Unification.w_unify_to_subterm_all ~flags env
((if l2r then c1 else c2),concl) eqclause.evd
@@ -165,33 +169,33 @@ let rewrite_conv_closed_unif_flags = {
Unification.allow_K_in_toplevel_higher_order_unification = false
}
-let rewrite_elim with_evars c e gl =
+let rewrite_elim with_evars frzevars c e gl =
let flags =
- freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
+ make_flags frzevars (project gl) rewrite_conv_closed_unif_flags c in
general_elim_clause_gen (elimination_clause_scheme with_evars ~flags) c e gl
-let rewrite_elim_in with_evars id c e gl =
+let rewrite_elim_in with_evars frzevars id c e gl =
let flags =
- freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
+ make_flags frzevars (project gl) rewrite_conv_closed_unif_flags c in
general_elim_clause_gen
(elimination_in_clause_scheme with_evars ~flags id) c e gl
(* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars cls rew elim =
+let general_elim_clause with_evars frzevars cls rew elim =
try
(match cls with
| None ->
(* was tclWEAK_PROGRESS which only fails for tactics generating one
subgoal and did not fail for useless conditional rewritings generating
an extra condition *)
- tclNOTSAMEGOAL (rewrite_elim with_evars rew elim)
- | Some id -> rewrite_elim_in with_evars id rew elim)
+ tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim)
+ | Some id -> rewrite_elim_in with_evars frzevars id rew elim)
with Pretype_errors.PretypeError (env,evd,
Pretype_errors.NoOccurrenceFound (c', _)) ->
raise (Pretype_errors.PretypeError
(env,evd,Pretype_errors.NoOccurrenceFound (c', cls)))
-let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
+let general_elim_clause with_evars frzevars tac cls sigma c t l l2r elim gl =
let all, firstonly, tac =
match tac with
| None -> false, false, None
@@ -200,12 +204,15 @@ let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
| Some (tac, AllMatches) -> true, false, Some (tclCOMPLETE tac)
in
let cs =
- (if not all then instantiate_lemma else instantiate_lemma_all)
+ (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
(pf_env gl) sigma gl c t l l2r
(match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id)
in
let try_clause c =
- side_tac (tclTHEN (Refiner.tclEVARS c.evd) (general_elim_clause with_evars cls c elim)) tac
+ side_tac
+ (tclTHEN
+ (Refiner.tclEVARS c.evd)
+ (general_elim_clause with_evars frzevars cls c elim)) tac
in
if firstonly then
tclFIRST (List.map try_clause cs) gl
@@ -279,12 +286,12 @@ let type_of_clause gl = function
| None -> pf_concl gl
| Some id -> pf_get_hyp_typ gl id
-let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars dep_proof_ok gl hdcncl =
+let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frzevars dep_proof_ok gl hdcncl =
let isatomic = isProd (whd_zeta hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in
- general_elim_clause with_evars tac cls sigma c t l
+ general_elim_clause with_evars frzevars tac cls sigma c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings)} gl
@@ -304,7 +311,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
(* Main function for dispatching which kind of rewriting it is about *)
-let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
+let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
((c,l) : constr with_bindings) with_evars gl =
if occs <> all_occurrences then (
rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
@@ -317,7 +324,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
| Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels)
- l with_evars dep_proof_ok gl hdcncl
+ l with_evars frzevars dep_proof_ok gl hdcncl
| None ->
try
rewrite_side_tac (!general_rewrite_clause cls
@@ -329,27 +336,31 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
| Some (hdcncl,args) ->
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c
- (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars dep_proof_ok gl hdcncl
+ (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok gl hdcncl
| None -> raise e
(* error "The provided term does not end with an equality or a declared rewrite relation." *)
let general_rewrite_ebindings =
general_rewrite_ebindings_clause None
-let general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,bl) =
- general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (c,bl)
+let general_rewrite_bindings l2r occs frzevars dep_proof_ok ?tac (c,bl) =
+ general_rewrite_ebindings_clause None l2r occs
+ frzevars dep_proof_ok ?tac (c,bl)
-let general_rewrite l2r occs dep_proof_ok ?tac c =
- general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,NoBindings) false
+let general_rewrite l2r occs frzevars dep_proof_ok ?tac c =
+ general_rewrite_bindings l2r occs
+ frzevars dep_proof_ok ?tac (c,NoBindings) false
-let general_rewrite_ebindings_in l2r occs dep_proof_ok ?tac id =
- general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac
+let general_rewrite_ebindings_in l2r occs frzevars dep_proof_ok ?tac id =
+ general_rewrite_ebindings_clause (Some id) l2r occs frzevars dep_proof_ok ?tac
-let general_rewrite_bindings_in l2r occs dep_proof_ok ?tac id (c,bl) =
- general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,bl)
+let general_rewrite_bindings_in l2r occs frzevars dep_proof_ok ?tac id (c,bl) =
+ general_rewrite_ebindings_clause (Some id) l2r occs
+ frzevars dep_proof_ok ?tac (c,bl)
-let general_rewrite_in l2r occs dep_proof_ok ?tac id c =
- general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,NoBindings)
+let general_rewrite_in l2r occs frzevars dep_proof_ok ?tac id c =
+ general_rewrite_ebindings_clause (Some id) l2r occs
+ frzevars dep_proof_ok ?tac (c,NoBindings)
let general_multi_rewrite l2r with_evars ?tac c cl =
let occs_of = on_snd (List.fold_left
@@ -365,12 +376,12 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
| [] -> tclIDTAC
| ((occs,id),_) :: l ->
tclTHENFIRST
- (general_rewrite_ebindings_in l2r (occs_of occs) true ?tac id c with_evars)
+ (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
(do_hyps l)
in
if cl.concl_occs = no_occurrences_expr then do_hyps l else
tclTHENFIRST
- (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
+ (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
(do_hyps l)
| None ->
(* Otherwise, if we are told to rewrite in all hypothesis via the
@@ -379,7 +390,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
| [] -> (fun gl -> error "Nothing to rewrite.")
| id :: l ->
tclIFTHENTRYELSEMUST
- (general_rewrite_ebindings_in l2r all_occurrences true ?tac id c with_evars)
+ (general_rewrite_ebindings_in l2r all_occurrences false true ?tac id c with_evars)
(do_hyps_atleastonce l)
in
let do_hyps gl =
@@ -391,7 +402,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
in
if cl.concl_occs = no_occurrences_expr then do_hyps else
tclIFTHENTRYELSEMUST
- (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
+ (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
do_hyps
type delayed_open_constr_with_bindings =
@@ -416,8 +427,8 @@ let general_multi_multi_rewrite with_evars l cl tac =
| (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
in loop l
-let rewriteLR = general_rewrite true all_occurrences true
-let rewriteRL = general_rewrite false all_occurrences true
+let rewriteLR = general_rewrite true all_occurrences true true
+let rewriteRL = general_rewrite false all_occurrences true true
(* Replacing tactics *)
@@ -1424,7 +1435,7 @@ let subst_one dep_proof_ok x gl =
tclTHENLIST
((if need_rewrite then
[generalize abshyps;
- general_rewrite dir all_occurrences dep_proof_ok (mkVar hyp);
+ general_rewrite dir all_occurrences true dep_proof_ok (mkVar hyp);
thin dephyps;
tclMAP introtac depdecls]
else
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 2cf4b3027..790594699 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -27,6 +27,7 @@ open Ind_tables
(*i*)
type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
type orientation = bool
@@ -36,10 +37,10 @@ type conditions =
| AllMatches (* Rewrite all matches whose side-conditions are solved *)
val general_rewrite_bindings :
- orientation -> occurrences -> dep_proof_flag ->
+ orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
val general_rewrite :
- orientation -> occurrences -> dep_proof_flag ->
+ orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(tactic * conditions) -> constr -> tactic
(* Equivalent to [general_rewrite l2r] *)
@@ -54,15 +55,16 @@ val register_general_rewrite_clause :
val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit
val general_rewrite_ebindings_clause : identifier option ->
- orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
- constr with_bindings -> evars_flag -> tactic
+ orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
+ ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_bindings_in :
- orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
+ orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
+ ?tac:(tactic * conditions) ->
identifier -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_in :
- orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
- identifier -> constr -> evars_flag -> tactic
+ orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
+ ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic
val general_multi_rewrite :
orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bbeb9425e..34cb5f771 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -223,7 +223,7 @@ END
let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
Refiner. tclWITHHOLES false
- (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings)) sigma true
+ (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true
let occurrences_of = function
| n::_ as nl when n < 0 -> (false,List.map abs nl)
@@ -646,7 +646,7 @@ exception Found of tactic
let rewrite_except h g =
tclMAP (fun id -> if id = h then tclIDTAC else
- tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true id (mkVar h) false))
+ tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true true id (mkVar h) false))
(Tacmach.pf_ids_of_hyps g) g
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
index da67d9b04..ee0920057 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -1,3 +1,8 @@
+(* In 8.1 autorewrite used to raised an anomaly here *)
+(* After resolution of the bug, autorewrite succeeded *)
+(* From forthcoming 8.4, autorewrite is forbidden to instantiate *)
+(* evars, so the new test just checks it is not an anomaly *)
+
Set Implicit Arguments.
Record Place (Env A: Type) : Type := {
@@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
Proof.
intros Env A e p; eapply ex_intro.
autorewrite with placeeq. (* Here is the bug *)
- auto.
-Qed.
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v
index 68f2f7ce7..5e9064f8a 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewrite.v
@@ -19,5 +19,11 @@ Proof.
apply H;reflexivity.
Qed.
+(* Check autorewrite does not solve existing evars *)
+(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
+Hint Rewrite <- plus_n_O : base1.
+Goal forall y, exists x, y+x = y.
+eexists. autorewrite with base1.
+Fail reflexivity.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe7..3d49d3cf9 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,14 @@ intros.
rewrite (H _).
reflexivity.
Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+ argument of the goal. This is sometimes used in contribs, even if
+ ad hoc. Here, we have the extra requirement that checking types
+ needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 77eeac64b..ddf5abf03 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -848,7 +848,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
Auto.default_auto
]);
Equality.general_rewrite_bindings_in true
- all_occurrences false
+ all_occurrences true false
(List.hd !avoid)
((mkVar (List.hd (List.tl !avoid))),
Glob_term.NoBindings
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:20:13 +0000