Email Gateway (Aug 22 2022 at 12:59): Email Gateway (Aug 22 2022 at 12:59):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I'm formalizing the syntax of IPv6 Addresses.
I made a quite large datatype.
The datatype definition is loading on my laptop within some minutes.
However, when I ctrl+hover the datatype command, it tells me:
command "datatype"
32.453s elapsed time, 42.494s cpu time, 11.460s GC time
Sitting there with a stop watch, it took more than 3 minutes. Is this
a bug in the time measurement of datatype?
In general, is there a way to speed up the datatype definition?
Best,
Cornelius
Email Gateway (Aug 22 2022 at 12:59):From: Makarius <makarius@sketis.net>
On Wed, 16 Mar 2016, C. Diekmann wrote:
I'm formalizing the syntax of IPv6 Addresses.
I made a quite large datatype.
It should be possible to formalize this more conveniently with small
datatypes and fewer cases.
The datatype definition is loading on my laptop within some minutes.
However, when I ctrl+hover the datatype command, it tells me:
command "datatype"
32.453s elapsed time, 42.494s cpu time, 11.460s GC timeSitting there with a stop watch, it took more than 3 minutes. Is this
a bug in the time measurement of datatype?
"Bug" is already meaningless in most software-engineering contexts. Here
we have a mix of computing, mathematics and physics. So it is hard to tell
what the outcome is precisely.
What is measured here is the toplevel transaction time. Thus forks due to
internal proofs are omitted, and arbitrary environmental effects on CPU
time are added.
Makarius
Email Gateway (Aug 22 2022 at 13:00):From: Mario Carneiro <di.gama@gmail.com>
A suggestion on how to simplify the definition (I am not an Isabelle expert
so I will have to guess some notation). A "list with optional omission" can
be represented as a type List A | (List A, List A) (that is, a tuple of two
lists or one), and there is a function from this type and given a default
value a : A, to Option(FixedList n A) (lists of length n) which takes l :
List A to Some(l) if Len(l) = n and None otherwise, and takes (k,l) to
Some(k ++ [a; n - Len(k) - Len(l)] ++ l) (where ++ is list concat and [a;
n] is a list containing n a's) if n - Len(k) - Len(l) is nonnegative and
None otherwise.
Your IPv6 type is the above with n = 8 and A = "16 word", a = 0, and the
valid members of the type are those elements of List A | (List A, List A)
that don't map to None.
Mario
Last updated: Nov 21 2024 at 12:39 UTC