aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.mli2
-rw-r--r--library/impargs.ml4
-rw-r--r--library/impargs.mli2
-rw-r--r--parsing/g_vernac.ml476
-rw-r--r--parsing/ppvernac.ml25
-rw-r--r--parsing/prettyp.ml40
-rw-r--r--test-suite/output/Arguments.out93
-rw-r--r--test-suite/output/Arguments.v40
-rw-r--r--toplevel/ide_slave.ml1
-rw-r--r--toplevel/vernacentries.ml54
-rw-r--r--toplevel/vernacexpr.ml8
11 files changed, 336 insertions, 9 deletions
diff --git a/interp/notation.mli b/interp/notation.mli
index 52a7c2b99c..f92ef94ed3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -48,6 +48,8 @@ val open_close_scope :
val empty_scope_stack : scopes
val push_scope : scope_name -> scopes -> scopes
+val find_scope : scope_name -> scope
+
(** Declare delimiters for printing *)
val declare_delimiters : scope_name -> delimiters -> unit
diff --git a/library/impargs.ml b/library/impargs.ml
index 2d5ffe9ab0..5d689faa0b 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -246,6 +246,10 @@ let compute_auto_implicits env flags enriching t =
if enriching then compute_implicits_flags env flags true t
else compute_implicits_gen false false false true true env t
+let compute_implicits_names env t =
+ let _, impls = compute_implicits_gen false false false false true env t in
+ List.map fst impls
+
(* Extra information about implicit arguments *)
type maximal_insertion = bool (* true = maximal contextual insertion *)
diff --git a/library/impargs.mli b/library/impargs.mli
index 6315745911..04251f332e 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -95,6 +95,8 @@ type manual_implicits = manual_explicitation list
val compute_implicits_with_manual : env -> types -> bool ->
manual_implicits -> implicit_status list
+val compute_implicits_names : env -> types -> name list
+
(** {6 Computation of implicits (done using the global environment). } *)
val declare_var_implicits : variable -> unit
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 78e01afd94..422da85447 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -581,10 +581,59 @@ GEXTEND Gram
| IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
+ (* Arguments *)
+ | IDENT "Arguments"; qid = smart_global;
+ impl = LIST1 [ l = LIST0
+ [ item = argument_spec ->
+ let id, r, s = item in [`Id (id,r,s,false,false)]
+ | "/" -> [`Slash]
+ | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
+ let f x = match sc, x with
+ | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+ | Some _, Some _ -> error "scope declared twice" in
+ List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items
+ | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
+ let f x = match sc, x with
+ | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+ | Some _, Some _ -> error "scope declared twice" in
+ List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items
+ | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
+ let f x = match sc, x with
+ | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+ | Some _, Some _ -> error "scope declared twice" in
+ List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items
+ ] -> l ] SEP ",";
+ mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
+ let mods = match mods with None -> [] | Some l -> List.flatten l in
+ let impl = List.map List.flatten impl in
+ let rec aux n (narg, impl) = function
+ | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl
+ | `Slash :: tl -> aux (n+1) (n, impl) tl
+ | [] -> narg, impl in
+ let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in
+ let nargs, rest = List.hd nargs, List.tl nargs in
+ if List.exists ((<>) nargs) rest then
+ error "All arguments lists must have the same length";
+ let err_incompat x y =
+ error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
+ if nargs > 0 && List.mem `SimplNeverUnfold mods then
+ err_incompat "simpl never" "/";
+ if List.mem `SimplNeverUnfold mods &&
+ List.mem `SimplDontExposeCase mods then
+ err_incompat "simpl never" "simpl nomatch";
+ VernacArguments (use_section_locality(), qid, impl, nargs, mods)
+
+ (* moved there so that camlp5 factors it with the previous rule *)
+ | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
+ "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
+ warning "Arguments Scope is deprecated; use Arguments instead";
+ VernacArgumentsScope (use_section_locality (),qid,scl)
+
(* Implicit *)
| IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
+ warning "Implicit Arguments is deprecated; use Arguments instead";
VernacDeclareImplicits (use_section_locality (),qid,pos)
| IDENT "Implicit"; "Type"; bl = reserv_list ->
@@ -601,12 +650,32 @@ GEXTEND Gram
idl = LIST1 identref -> Some idl ] ->
VernacGeneralizable (use_non_locality (), gen) ] ]
;
+ arguments_modifier:
+ [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase]
+ | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold]
+ | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
+ | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
+ | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
+ | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
+ [`ClearImplicits; `ClearScopes]
+ | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
+ [`ClearImplicits; `ClearScopes]
+ ] ]
+ ;
implicit_name:
[ [ "!"; id = ident -> (id, false, true)
| id = ident -> (id,false,false)
| "["; "!"; id = ident; "]" -> (id,true,true)
| "["; id = ident; "]" -> (id,true, false) ] ]
;
+ scope:
+ [ [ "%"; key = IDENT -> key ] ]
+ ;
+ argument_spec: [
+ [ b = OPT "!"; id = name ; s = OPT scope ->
+ snd id, b <> None, Option.map (fun x -> loc, x) s
+ ]
+ ];
strategy_level:
[ [ IDENT "expand" -> Conv_oracle.Expand
| IDENT "opaque" -> Conv_oracle.Opaque
@@ -901,10 +970,6 @@ GEXTEND Gram
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
- | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
- "["; scl = LIST0 opt_scope; "]" ->
- VernacArgumentsScope (use_section_locality (),qid,scl)
-
| IDENT "Infix"; local = obsolete_locality;
op = ne_lstring; ":="; p = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
@@ -970,9 +1035,6 @@ GEXTEND Gram
| IDENT "closed"; IDENT "binder" -> ETBinder false
] ]
;
- opt_scope:
- [ [ "_" -> None | sc = IDENT -> Some sc ] ]
- ;
production_item:
[ [ s = ne_string -> TacTerm s
| nt = IDENT;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6254d345f7..4e73b37939 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -835,6 +835,31 @@ let rec pr_vernac = function
prlist_with_sep spc (fun imps ->
str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
impls)
+ | VernacArguments (local, q, impl, nargs, mods) ->
+ hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+ pr_smart_global q ++
+ let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+ let pr_if b x = if b then x else str "" in
+ let pr_br imp max x = match imp, max with
+ | true, false -> str "[" ++ x ++ str "]"
+ | true, true -> str "{" ++ x ++ str "}"
+ | _ -> x in
+ let rec aux n l =
+ match n, l with
+ | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+ | _, [] -> mt()
+ | n, (id,k,s,imp,max) :: tl ->
+ spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+ aux (n-1) tl in
+ prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+ if mods <> [] then str" : " else str"" ++
+ prlist_with_sep (fun () -> str", " ++ spc()) (function
+ | `SimplDontExposeCase -> str "simpl nomatch"
+ | `SimplNeverUnfold -> str "simpl never"
+ | `DefaultImplicits -> str "default implicits"
+ | `ClearImplicits -> str "clear implicits"
+ | `ClearScopes -> str "clear scopes")
+ mods)
| VernacReserve bl ->
let n = List.length (List.flatten (List.map fst bl)) in
hov 2 (str"Implicit Type" ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 06d148ec60..741f9201e8 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -151,6 +151,45 @@ let print_argument_scopes prefix = function
str "]")]
| _ -> []
+(*****************************)
+(** Printing simpl behaviour *)
+
+let print_simpl_behaviour ref =
+ match Tacred.get_simpl_behaviour ref with
+ | None -> []
+ | Some (recargs, nargs, flags) ->
+ let never = List.mem `SimplNeverUnfold flags in
+ let nomatch = List.mem `SimplDontExposeCase flags in
+ let pp_nomatch = spc() ++ if nomatch then
+ str "avoiding to expose match constructs" else str"" in
+ let pp_recargs = spc() ++ str "when the " ++
+ let rec aux = function
+ | [] -> mt()
+ | [x] -> str (ordinal (x+1))
+ | [x;y] -> str (ordinal (x+1)) ++ str " and " ++ str (ordinal (y+1))
+ | x::tl -> str (ordinal (x+1)) ++ str ", " ++ aux tl in
+ aux recargs ++ str (plural (List.length recargs) " argument") ++
+ str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
+ str " to a constructor" in
+ let pp_nargs =
+ spc() ++ str "when applied to " ++ int nargs ++
+ str (plural nargs " argument") in
+ [hov 2 (str "The simpl tactic " ++
+ match recargs, nargs, never with
+ | _,_, true -> str "never unfolds " ++ pr_global ref
+ | [], 0, _ -> str "always unfolds " ++ pr_global ref
+ | _::_, n, _ when n < 0 ->
+ str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+ | _::_, n, _ when n > List.fold_left max 0 recargs ->
+ str "unfolds " ++ pr_global ref ++ pp_recargs ++
+ str " and" ++ pp_nargs ++ pp_nomatch
+ | _::_, _, _ ->
+ str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+ | [], n, _ when n > 0 ->
+ str "unfolds " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
+ | _ -> str "unfolds " ++ pr_global ref ++ pp_nomatch )]
+;;
+
(*********************)
(** Printing Opacity *)
@@ -625,6 +664,7 @@ let print_about_any k =
pr_infos_list
([print_ref false ref; blankline] @
print_name_infos ref @
+ print_simpl_behaviour ref @
print_opacity ref @
[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
| Syntactic kn ->
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
new file mode 100644
index 0000000000..139f9e9922
--- /dev/null
+++ b/test-suite/output/Arguments.out
@@ -0,0 +1,93 @@
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus when applied to 1 argument
+ avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+ when the 1st argument evaluates to a constructor and
+ when applied to 1 argument avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+ when the 1st and 2nd arguments evaluate to a constructor and
+ when applied to 2 arguments
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+ when the 1st and 2nd arguments evaluate to a constructor
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+pf :
+forall D1 C1 : Type,
+(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
+
+Arguments D2, C2 are implicit
+Arguments D1, C1 are implicit and maximally inserted
+Argument scopes are [foo_scope type_scope _ _ _ _ _]
+The simpl tactic never unfolds pf
+pf is transparent
+Expands to: Constant Top.pf
+fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
+
+Arguments A, B, C are implicit and maximally inserted
+Argument scopes are [type_scope type_scope type_scope _ _ _]
+The simpl tactic unfolds fcomp when applied to 6 arguments
+fcomp is transparent
+Expands to: Constant Top.fcomp
+volatile : nat -> nat
+
+Argument scope is [nat_scope]
+The simpl tactic always unfolds volatile
+volatile is transparent
+Expands to: Constant Top.volatile
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+ when the 3rd, 4th and 5th arguments evaluate to a constructor
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument T2 is implicit
+Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+ when the 4th, 5th and 6th arguments evaluate to a constructor
+f is transparent
+Expands to: Constant Top.S1.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Arguments T1, T2 are implicit
+Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+ when the 5th, 6th and 7th arguments evaluate to a constructor
+f is transparent
+Expands to: Constant Top.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+The simpl tactic unfolds f
+ when the 5th, 6th and 7th arguments evaluate to a constructor
+f is transparent
+Expands to: Constant Top.f
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
new file mode 100644
index 0000000000..c93d2505da
--- /dev/null
+++ b/test-suite/output/Arguments.v
@@ -0,0 +1,40 @@
+Arguments minus n m : simpl nomatch.
+About minus.
+Arguments minus n / m : simpl nomatch.
+About minus.
+Arguments minus !n / m : simpl nomatch.
+About minus.
+Arguments minus !n !m /.
+About minus.
+Arguments minus !n !m.
+About minus.
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) :=
+ fun x => (f (fst x), g (snd x)).
+Delimit Scope foo_scope with F.
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+About pf.
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+Arguments fcomp {A B C}%type_scope f g x /.
+About fcomp.
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+About volatile.
+Set Implicit Arguments.
+Section S1.
+Variable T1 : Type.
+Section S2.
+Variable T2 : Type.
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+ match n, m with
+ | 0,_ => 0
+ | S _, 0 => n
+ | S n', S m' => f x y n' v m' end.
+About f.
+Global Arguments f x y !n !v !m.
+About f.
+End S2.
+About f.
+End S1.
+About f.
+Arguments f : clear implicits and scopes.
+About f.
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 102c92237d..60b89c2236 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -165,6 +165,7 @@ let rec attribute_of_vernac_command = function
| VernacHints _ -> []
| VernacSyntacticDefinition _ -> []
| VernacDeclareImplicits _ -> []
+ | VernacArguments _ -> []
| VernacDeclareReduction _ -> []
| VernacReserve _ -> []
| VernacGeneralizable _ -> []
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 88b78a633f..71bd311890 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -763,6 +763,59 @@ let vernac_declare_implicits local r = function
Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
+let vernac_declare_arguments local r l nargs flags =
+ let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+ let names, rest = List.hd names, List.tl names in
+ if List.exists ((<>) names) rest then
+ error "All arguments lists must declare the same names";
+ let inf_names =
+ Impargs.compute_implicits_names (Global.env())
+ (Global.type_of_global (smart_global r)) in
+ let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in
+ let rec check ld li = match ld, li with
+ | [], [] -> ()
+ | [], l -> error ("The following arguments are not declared: " ^
+ (String.concat ", " (List.map string_of_name l)))
+ | x::_, [] -> error ("Extra argument " ^ string_of_name x)
+ | Name x::_, Name y::_ when x <> y -> error ("The declared name " ^
+ string_of_id x ^ " and the inferred one " ^ string_of_id y ^
+ " are different")
+ | _::ld, _::li -> check ld li in
+ if names <> [] then check names inf_names;
+ let implicits = List.map (Util.list_map_filter (function
+ | (Anonymous, _,_,_,_) | (_,_,_, false, _) -> None
+ | (Name id, _,_, true, max) -> Some (ExplByName id,max,false))) l in
+ (* All other infos are in the first item of l *)
+ let l = List.hd l in
+ let some_implicits_specified = implicits <> [[]] in
+ let scopes = List.map (function
+ | (_,_, None,_,_) -> None
+ | (_,_, Some (o, k), _,_) ->
+ try Some(ignore(Notation.find_scope k); k)
+ with _ -> Some (Notation.find_delimiters_scope o k)) l in
+ let some_scopes_specified = List.exists ((<>) None) scopes in
+ let rargs =
+ Util.list_map_filter (function (n, true) -> Some n | _ -> None)
+ (Util.list_map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
+ if some_scopes_specified || List.mem `ClearScopes flags then
+ vernac_arguments_scope local r scopes;
+ if not some_implicits_specified && List.mem `DefaultImplicits flags then
+ vernac_declare_implicits local r []
+ else if some_implicits_specified || List.mem `ClearImplicits flags then
+ vernac_declare_implicits local r implicits;
+ if nargs >= 0 && nargs < List.fold_left max 0 rargs then
+ error "The \"/\" option must be places after the last \"!\"";
+ let rec narrow = function
+ | #Tacred.simpl_flag as x :: tl -> x :: narrow tl
+ | [] -> [] | _ :: tl -> narrow tl in
+ let flags = narrow flags in
+ if rargs <> [] || nargs >= 0 || flags <> [] then
+ match smart_global r with
+ | ConstRef _ as c ->
+ Tacred.set_simpl_behaviour local c (rargs, nargs, flags)
+ | _ -> error "Simpl behaviour can be declared for constants only"
+;;
+
let vernac_reserve bl =
let sb_decl = (fun (idl,c) ->
let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -1377,6 +1430,7 @@ let interp c = match c with
| VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
| VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
| VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
+ | VernacArguments (local, qid, l, narg, flags) -> vernac_declare_arguments local qid l narg flags
| VernacReserve bl -> vernac_reserve bl
| VernacGeneralizable (local,gen) -> vernac_generalizable local gen
| VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index bae6cfcdd9..575735230d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -224,8 +224,6 @@ type vernac_expr =
| VernacOpenCloseScope of (locality_flag * bool * scope_name)
| VernacDelimiters of scope_name * string
| VernacBindScope of scope_name * class_rawexpr list
- | VernacArgumentsScope of locality_flag * reference or_by_notation *
- scope_name option list
| VernacInfix of locality_flag * (lstring * syntax_modifier list) *
constr_expr * scope_name option
| VernacNotation of
@@ -318,6 +316,12 @@ type vernac_expr =
locality_flag * onlyparsing_flag
| VernacDeclareImplicits of locality_flag * reference or_by_notation *
(explicitation * bool * bool) list list
+ | VernacArguments of locality_flag * reference or_by_notation *
+ ((name * bool * (loc * string) option * bool * bool) list) list *
+ int * [ `SimplDontExposeCase | `SimplNeverUnfold
+ | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
+ | VernacArgumentsScope of locality_flag * reference or_by_notation *
+ scope_name option list
| VernacReserve of simple_binder list
| VernacGeneralizable of locality_flag * (lident list) option
| VernacSetOpacity of
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 17:14:56 +0000