Email Gateway (Aug 19 2022 at 08:20): Email Gateway (Aug 19 2022 at 08:20):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all proof lovers,
After the Isar reference, I typed this in Isabelle/jEdit:
notepad
begin
fix n :: nat
have "P n"
proof (induct n)
case 0
show ?case sorry
next
case (Suc n)
from Suc.hyps show ?case sorry
qed
end
As the syntax from the PDF is not always exact (mainly characters issues),
I though there was an error there too, and felt “(Suc n)” should be
enclosed in quote, as an HOL expression. But doing so, I get this in the
Output pan:
Unknown case: "(Suc n)"
Is “(Suc n)”, and HOL or Isar expression? If that's an HOL expression as I
believe, then why do I get that error report?
Email Gateway (Aug 19 2022 at 08:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Yannick,
You can get the sources for any of the Isabelle2012 documentation.
The direct link is this:
http://isabelle.in.tum.de/repos/isabelle/archive/21c42b095c84.tar.gz
The link that would get you to the link for that file is here:
http://isabelle.in.tum.de/repos/isabelle/
You click on "files" beside "2 months ago Isabelle2012". You would then
click on "gz" at the top of the page.
You unzip the tar file, and for isar-ref.pdf, you find the folder
"isabelle-21c42b095c84\doc-src\IsarRef\Thy".
You then have to search around on those files with grep or something to
find the file that contains the desired code.
The source files keep you from having to type in the code, keep you from
copying bogus characters from the PDF, and they teach you something
about how the author produced what you see in the PDF.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:22):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Wed, 01 Aug 2012 23:30:18 +0200, Gottfried Barrow
<gottfried.barrow@gmx.com> a écrit:
You can get the sources for any of the Isabelle2012 documentation.
The direct link is this:
http://isabelle.in.tum.de/repos/isabelle/archive/21c42b095c84.tar.gz
The link that would get you to the link for that file is here:
Thanks Gottfried, those links are worth to be bookmarked :-P
You click on "files" beside "2 months ago Isabelle2012". You would then
click on "gz" at the top of the page.You unzip the tar file, and for isar-ref.pdf, you find the folder
"isabelle-21c42b095c84\doc-src\IsarRef\Thy".You then have to search around on those files with grep or something to
find the file that contains the desired code.
I got it, that's in “Synopsis.thy”, and modulo the indentation, that's the
same, there is no quote too:
notepad
begin
fix n :: nat
have "P n"
proof (induct n)
case 0
show ?case sorry
next
case (Suc n)
from Suc.hyps show ?case sorry
qed
end
So, what's the expression type of “(Suc n)” at the line whose text is
“case (Suc n)”? Isn't “(Suc n)” an HOL expression? It appears in the text
as if it was an Isar expression, but I feel sure it's not. I'm lost with
that point.
The source files keep you from having to type in the code, keep you from
copying bogus characters from the PDF, and they teach you something
about how the author produced what you see in the PDF.
They also will teach me a bit of LaTex, which I've never practiced
(red‑face)
Email Gateway (Aug 19 2022 at 08:23):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I don't know much more than you, so you should keep that in mind for the
future.
"Suc" is the successor function, and it comes from
"Isabelle2012/src/HOL/Nat.thy". This is where those "declare" commands
come in handy. I attach "I.thy". It has all the declare and print
commands I found that looked useful. Delete what you don't want, or
don't use any of it. I keep it open in jEdit all the time, that's why it
has a short name.
In particular, I used:
declare[[names_unique=true]] declare[[show_consts=true]]
In the output panel, it shows me:
constants:
prop :: (prop ⇒ prop)
Nat.Suc :: (Nat.nat ⇒ Nat.nat)
Isar as a language is independent of HOL. Isar can be used in any logic,
such as Isabelle/ZF.
HOL is one of the many logics in Isabelle2012/src, although it's the
most popular one.
"Expression" is an ambiguous word that can be used in lots of different
ways.
Isar, as I understand it, is a link between the "inner syntax" and the
"outer syntax", where HOL expressions would be "inner syntax". This is
covered in Chapter 3 of isar-ref.pdf, and on Page 5 of prog-prove.pdf. I
think "outer syntax" is related to the meta-logic which comes from
"src/Pure". Isar is tied into Pure, and Pure is the foundation for
logics such as HOL.
Putting in extraneous information here, where I use the ambiguous term
"expression", I'll go out on a limb and say, "A HOL expression is always
an Isar expression, but an Isar expression is not always a HOL expression."
I attach a screen shot to show you the useful information you get from
five of the declare commands being true.
Regards,
GB
case_Suc_n.png
I.thy
Email Gateway (Aug 19 2022 at 08:24):From: Christian Sternagel <c-sterna@jaist.ac.jp>
To answer the original question:
Here 'case (Suc n)' as well as 'case 0' (above) are part of Isar not
HOL. We could also just use 'case 0' and 'case Suc', then it is more
clear that we are just giving names of facts (those names are
automatically established when starting with 'proof (induct n)'). The
variant 'case (Suc n)' of 'case Suc' is just a nicety to allow giving
explicit names to variables (which makes proofs more robust). If you
want to see to what fact 'Suc' refers, just use 'from Suc' directly
below the 'case' line.
cheers
chris
Email Gateway (Aug 19 2022 at 08:26):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christian already gave you the answer, but I was hot on the trail
because it occurred to me to use "print_theorem" under "case (Suc n)",
which Christian had given as a tip some days ago. This all ties into
differentiating between Isar and HOL.
"case" is an Isar command that's described on page 129 of isar-ref.pdf.
If you try to put quotes like this:
case ("Suc n")
then you get the error:
Outer syntax error: name declaration expected, but keyword ) was found
The outer syntax error substantiates that "case" is not HOL syntax,
because HOL syntax is inner syntax.
Put "print_theorems" under "case (Suc n)", and you get this:
facts:
<unnamed>: ((P∷(Nat.nat ⇒ HOL.bool)) (n∷Nat.nat))
local.Suc: ((P∷(Nat.nat ⇒ HOL.bool)) (n∷Nat.nat))
Somebody like me might not know what it means, but it definitely tells
me that "Suc" isn't the the HOL function "Nat.Suc::(nat => nat)", like I
had told you. You can't always know what something means, but you can
know what it isn't sometimes.
Page 45 of prog-prove.pdf explains "case".
Regards,
GB
Email Gateway (Aug 19 2022 at 08:27):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Chris,
Is this right? There's Isar syntax, which is defined in Pure. There's
HOL syntax, which is defined using Isar keywords. And there is the HOL
logic which is a combination of Isar syntax and HOL syntax.
What I'm thinking about in particular is that the proof of a HOL theorem
is a HOL proof, but it may contain Isar commands.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:27):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Gottfried,
I would really prefer to hand this question over to a wizard ;)
But let me give it a try. What I think (but that does not necessarily
mean that it's true) is the following:
Isar syntax is not part of Pure, but the "Isar-language" is
well-integrated on top of Pure.
HOL syntax is defined via commands (not sure whether those are really
part of Isar or rather independent; my guess would be that they are just
convenience tools built on top of the Isabelle/ML layer... but then,
what is not?)
HOL as a logic is independent from Isar.
Proofs are irrelevant, thus they can't be part of the logic, i.e.,
they are not part of HOL.
In the end, a proof is just a step-wise manipulation of the abstract
data type 'thm' through a well-defined interface (sometimes called the
trusted Kernel).
cheers
chris
Email Gateway (Aug 19 2022 at 08:27):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Chris, thanks for the explanation. There's lots of interesting
information there, but I reduced everything down to this statement, "I
just want to know what word to use for Isabelle's programming language".
I was in doubt for a while, and then it occurred to me, "Oh yea, it is
called the Isar reference manual".
In Chapter 5, page 76, it says, "Isabelle/Isar theories are defined via
theory files..." It then says that "theory" and "end" are Isar commands.
As far as I'm concerned, everything between "theory" and "end" is the
Isar programming language. There is the ML in the "ML{ ... }", but other
than that, it's all Isar to me now.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:27):From: Lars Noschinski <noschinl@in.tum.de>
The Isar command "case" (in its long form) takes a case name and a list
of inner syntax expressions (probably what you mean with HOL
expressions). The case name "Suc" happens to be the same as the name of
the constructor "Suc"; but this is just coincidence:
notepad
begin
fix n :: nat and P
proof (induct n rule: nat.induct[case_names Foo Bar])
case Foo show ?case sorry
next
case (Bar n) show ...
Email Gateway (Aug 19 2022 at 08:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 8/1/2012 9:18 PM, Christian Sternagel wrote:
- Pure is a kind of minimal logic independent from Isar.
- Isar syntax is not part of Pure, but the "Isar-language" is
well-integrated on top of Pure.- HOL syntax is defined via commands (not sure whether those are
really part of Isar or rather independent; my guess would be that they
are just convenience tools built on top of the Isabelle/ML layer...
but then, what is not?)
My questions about syntax end up being the easy (easier, but not
completely answered) questions. Your reply below as to what HOL is as a
logic becomes the "not so easily understood" reply.
Here's what I found: Isar outer syntax is defined in
~/src/Pure/isar_syn.ML.
(* Title: Pure/Isar/isar_syn.ML
Author: Markus Wenzel, TU Muenchen
Isar/Pure outer syntax.
*)
So Isar/Pure outer syntax is used to define inner syntax (I guess), such
as HOL's inner syntax, because in that file there are the usual Isar
commands that are documented in isar-ref.pdf:
line 154: Outer_Syntax.command ("judgement
line 158: Outer_Syntax.command ("consts
line 207: Outer_Syntax.command ("axioms
line 219: Outer_Syntax.command ("defs
line 228: Outer_Syntax.command ("definition
line 249: Outer_Syntax.local_theory ("notation
etc.
Well, life is not so simple. "datatype" is not specific to Isar. It's
defined in ~/src/HOL/Datatype.thy, and is somehow defined with
~/src/HOL/Tools/Datatype/datatype.ML.
I type "datatype" without typing anything else, and I get the error
"Outer syntax error".
That's enough of that stuff for now.
- HOL as a logic is independent from Isar.
- Proofs are irrelevant, thus they can't be part of the logic, i.e.,
they are not part of HOL.- In the end, a proof is just a step-wise manipulation of the abstract
data type 'thm' through a well-defined interface (sometimes called the
trusted Kernel).
Yea, so I guess we could do it all in ML, where ML is the language of
the foundation.
Your second two statements are the "something to think about".
Regards,
GB
Email Gateway (Aug 19 2022 at 08:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
This calls for a "dude expression" using "dude syntax" interpreted with
standard "dude semantics", as in, "Man, dude, if you (meaning me) would
only open the source files and do some brainless scrolling around, you
wouldn't clutter up the list with as many emails for a single subject."
At the bottom of ~/src/HOL/Tools/Datatype/datatype.ML, we get this:
val _ =
Outer_Syntax.command @{command_spec "datatype"} "define inductive
datatypes"
(Parse.and_list1 spec_cmd
(Toplevel.theory o (snd oo add_datatype_cmd
Datatype_Aux.default_config)));
So some HOL syntax is defined with Isar commands, and some HOL syntax is
defined with ML, where some HOL syntax is added as outer syntax.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:28):From: Lars Noschinski <noschinl@in.tum.de>
"HOL syntax" is not a very useful term here. In Isabelle/Isar, we
distinguish between outer and inner syntax. The inner syntax is the
syntax used to input terms (and types). Apart from trivial cases, inner
syntax needs to be quoted.
The outer syntax is everything else. Most of it is already part of Pure
(i.e. independent of any logic), mainly everything which makes up proof
and document structure; but logics often add additional commands for
logic-specific operations (e.g. "fun" and "inductive" for HOL).
Both syntaxes can be extended, but after bootstrapping, the outer syntax
usually stays pretty static; where as the inner syntax is changed with
any definition or syntax annotation you issue. I think, by default there
is no tool on the Isar level which would modify the outer syntax (just
as there is no construct on the term level, which would modify the inner
syntax).
-- Lars.
Email Gateway (Aug 19 2022 at 08:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
One last comment, hopefully.
Outer_syntax is defined in src/Pure/Isar/outer_syntax.ML:
(* Title: Pure/Isar/outer_syntax.ML
Author: Markus Wenzel, TU Muenchen
The global Isabelle/Isar outer syntax.
I was wanting to start using the phrase "the Pure programming language",
but "Outer_syntax.command" is an Isar command, so the HOL outer syntax
"datatype" is defined as HOL syntax using an Isar command.
My use of "the Pure programming language" will have to wait until I
understand whether there's any HOL syntax which can be defined using ML,
but which cannot be defined using Isar.
I like to have the vocabulary locked down. I go with these ideas until
someone tells me different.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 8/2/2012 10:42 AM, Lars Noschinski wrote:
On 02.08.2012 15:58, Gottfried Barrow wrote:
So some HOL syntax is defined with Isar commands, and some HOL syntax is
defined with ML, where some HOL syntax is added as outer syntax."HOL syntax" is not a very useful term here. In Isabelle/Isar, we
distinguish between outer and inner syntax. The inner syntax is the
syntax used to input terms (and types). Apart from trivial cases,
inner syntax needs to be quoted.
Lars, I sent the last email before I got this one. But in prog-prove,
Tobias says,
"When Isabelle prints a syntax error message, it refers to the HOL
syntax as the inner syntax
and the enclosing theory language as the outer syntax."
I'm trying to pin down "what is the Isar programming language". I want
to speak of one programming language, "Isar", but if it's not that
simple, then I want to be more sophisticated about it.
I understand that between "theory MyTheory" and "end" in "MyTheory.thy"
there are things like Latex and ML. But I can consider any of that as
part of an argument to an Isar command like "ML{ .... }" or "text{ ...
}". I'm trying to figure out if there's anything between "theory" and
"end" that someone would have to say, "Most of what's between 'theory'
and 'end' is Isar, but there are exceptions."
The outer syntax is everything else. Most of it is already part of
Pure (i.e. independent of any logic), mainly everything which makes up
proof and document structure; but logics often add additional commands
for logic-specific operations (e.g. "fun" and "inductive" for HOL).
But if you can't combine "HOL syntax" with "inner syntax" and "outer
syntax", then it makes it hard to talk about what's specific to HOL.
There's the HOL specific outer syntax "datatype". I want to call that
"HOL syntax", or at least "HOL outer syntax".
Both syntaxes can be extended, but after bootstrapping, the outer
syntax usually stays pretty static; where as the inner syntax is
changed with any definition or syntax annotation you issue. I think,
by default there is no tool on the Isar level which would modify the
outer syntax (just as there is no construct on the term level, which
would modify the inner syntax).
This brings up "Outer_syntax.command", which I mentioned in the email I
sent out before this one.
I'm going to call "Outer_syntax.command" an Isar command, and it's used
in Datatype.thy to define "datatype" as outer syntax. If I don't call it
an Isar command, then what am I going to call it? If I call it an ML
command or a Pure command, then I can't say that Isar is the programming
language that's being used to define "datatype". If that's the case,
then there's a lower level programming language that I'm using. If there
is, I want to know what to call it.
Thanks,
GB
Email Gateway (Aug 19 2022 at 08:28):From: Lawrence Paulson <lp15@cam.ac.uk>
ML is a programming language. You write programs in ML.
Pure is not a programming language. It is a logical formalism, specifically, the logical framework that is the basis of Isabelle.
HOL is also a programming language, namely higher-order logic.
Isar is a formal language for proof developments. These are not programs and it is not a programming language.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 8/2/2012 11:17 AM, Lawrence Paulson wrote:
ML is a programming language. You write programs in ML.
Pure is not a programming language. It is a logical formalism, specifically, the logical framework that is the basis of Isabelle.
HOL is also a programming language, namely higher-order logic.
Isar is a formal language for proof developments. These are not programs and it is not a programming language.
Larry, thanks. I'm making some progress here. I've acquired some
resolution for the word "language". A language that's used on a computer
is not necessarily a "programming language". Sounds reasonable. I guess.
It's hard for me not to think of a sequence of instructions as a program.
Now all I have to do is figure out exactly what the "Isar proof
language" is, and what between "theory" and "end" isn't Isar.
It gets a little difficult to sort it all out. ML is a programming
language which is used to implement Isar, which is a formal language,
but not a programming language, and Isar is used to implement HOL, which
is a programming language, and the syntax for Isar and "HOL syntax" is
all intertwined, where you occasionally drop down into the ML
programming language to use an "Isar command", like
"Outer_syntax.command", to define syntax for the HOL programming language.
I'll check out on this thread, and store away any other comments that
come in for future reference.
Regards,
GB
Larry Paulson
On 2 Aug 2012, at 16:46, Gottfried Barrow wrote:
One last comment, hopefully.
Outer_syntax is defined in src/Pure/Isar/outer_syntax.ML:
(* Title: Pure/Isar/outer_syntax.ML
Author: Markus Wenzel, TU MuenchenThe global Isabelle/Isar outer syntax.
I was wanting to start using the phrase "the Pure programming language", but "Outer_syntax.command" is an Isar command, so the HOL outer syntax "datatype" is defined as HOL syntax using an Isar command.
My use of "the Pure programming language" will have to wait until I understand whether there's any HOL syntax which can be defined using ML, but which cannot be defined using Isar.
I like to have the vocabulary locked down. I go with these ideas until someone tells me different.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:28):From: Makarius <makarius@sketis.net>
The content of a theory file between 'theory' and the final 'end' is by
definition the Isar source language.
Isar is a general framework to define "domain-specific formal
languages". It allows to nest various sub-languages easily, most
notably the Isar proof language. Other more exotic language embeddings
are here:
notepad
begin
(* Isar proof language here *)
fix a b :: nat
fix n :: nat
assume a: "⋀m. n + m > 0"
ML_val {*
(* ML inside Isar proof context here *)
(* antiquotation of logical entities here:*)
fun foo th = th RS @{thm a}
(* further nesting: term language inside fact language: *)
fun bar th = th RS @{thm a [of "a + b"]}
*}
end
end
* Note that above the Prover IDE markup will tell you about the formal
entities occurring in the nested sublanguages. E.g. CTRL-hover over
"a + b" parts will do the same as if they would occur directly as
terms within the main Isar source language (statements, proofs).
* ML has a special role in the game: it is the platform for first
bootstrapping the Isar language framework, and later gets re-embedded
into the Isar source language, with the above antiquotation
mechanisms to get some parts of Isar back into ML. E.g. like this:
ML {*
val my_thm = @{lemma "⋀x. x = x" by (rule refl)}
*}
* Formal latex is another special sub-language. For example, it allows
to embed ML with embedded formal entities like this:
text {*
blah blah; this is mainly {\LaTeX}, but with some antiquotations
@{ML "
(* this is again ML inside the Isar context *)
let val my_thm = @{lemma \"⋀x. x = x\" by (rule refl)}
in Thm.prop_of my_thm end"}
*}
Here the incremental parser of Isabelle/jEdit sometimes gets problems
with the nested quotes, but in the end you should get proper formal
markup of everything to hover over, and understand this formal
gibberish.
* Outer_syntax.command that was left somewhat myterious above is not
very special. It is just an Isabelle/ML function that defines new
Isar commands. Similar to the ML function Method.setup to define
proof methods, but the latter also has an Isar source language
counterpart called method_setup; both Method.setup and
method_setup take an ML expression for the method implementation as
argument: ML that is embedded into Isar in the usual way.
It is just a historical accident, that Outer_syntax.command is still
not fully-integrated into the self-defining self-embedding game of
formal languages. (Just today I've made further stepts towards that,
and found out that only 'theory' needs to be given from outside; all
other Isar commands can be defined inside the Isar framework.)
On now to make sophisticated specifications and serious proofs in
Isabelle/HOL ...
Makarius
Email Gateway (Aug 19 2022 at 08:30):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I think I have it.
HOL imports pure, therefore it inherits the Isar language and a default
set of Isar outer syntax commands, where new outer syntax can be defined
with "Outer_syntax.command". Everything in a .thy file is Isar syntax
and everything is HOL syntax, so there's no need to talk about HOL
syntax, since, again, everything is HOL syntax. We could, however,
compare Isabelle/HOL syntax with Isabelle/FOL syntax, where they would
both share the default Isar outer syntax commands.
The word "term" doesn't have a lot of significance to me. I assume you
mean "lambda calculus term", but I see very little lambda calculus in
expressions between double quotes, so it doesn't completely help me to
know what to put in double quotes.
However, it is useful to know that if I see something in double quotes,
I know it must be either a type or a lambda calculus term, even if the
lambda calculus doesn't look like lambda calculus.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:31):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Except for the technical details about which I didn't investigate, I feel
to understand about the same as I read documents explaining Isabelle
(actually, Markus Wenzel's thesis you pointed to, a captivating document):
the distinction between inner and outer syntax, does not map the
distinction between Isabelle‑Pure and the rest. If all is defined by
extension in terms derived and derived‑derived from the Isabelle‑Pure
core, and if extension can apply to both the outer and inner syntax, then
the distinction is not that meaningful. Finally, may inner syntax is for
some kind of expressions, and expressions which are not lexically atomic.
Perhaps that's a layout choice inspired by simplifying parsing. Can we say
what is a value (ex. contains variables of all kinds) and is not lexically
atomic (or is lexically atomic, but whose name is not a simple name), have
to be written in quotes? Just that?
Email Gateway (Aug 19 2022 at 08:33):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I've been totally focused on the frontend languages, ML, Isar, and HOL,
while knowing nothing about what the backend prover does with them.
I now have a way to make sense of it all being Isar syntax, the HOL
syntax being a part of the Isar syntax, and HOL not being dependent on Isar.
It could be that Isar is a framework that HOL uses to state lambda
calculus terms, and the backend strips away all the outer syntax, where
all that's left is the HOL lambda calculus terms. That idea lines up
with Christian saying that proofs are irrelevant.
Now I sit on the two ideas and wait to see if I read something that
supports one of the two ideas, that HOL inherits Isar and makes it its
own, or Isar is a framework that gets stripped away by the backend.
Today, right now, I'm leaning towards the idea that much of the Isar
gets stripped away.
(I do see "framework" in "Chapter 2 The Isabelle/Isar Framework", which
is where I must have gotten "framework". I don't see "stripped away"
anywhere yet. There's a lot I haven't read yet.)
I don't really care to know the details of what the backend does, it
would take years to learn about it, but it's nice to make sense of
important high-level concepts.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:35):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I believe HOL inherits/use Isar, but I can't prove it (cheese).
Along with this, for others interested in the original question too, here
is an evidence that what you write in quotes, is not specifically HOL: you
write lemma's conclusion to prove in quotes, and that's obviously not HOL,
which I believe is object logic only. Ex. the “==>” is meta‑level logic.
So here comes an updated definitions perhaps, of what you have to put in
quotes: you write in quotes, every expressions which involves mix‑fix
notations (I don't know any of these outside of quotes), to which is to be
added previously mentioned type expressions when not syntactically atomic
and names when not simples (ex. containing dash, math symbols and the
like).
P.S. I've not read all replies to that thread in deep details so far, so I
apologies for any contradictions with what others may have said if ever
there are some.
Last updated: Apr 25 2024 at 16:19 UTC