Re: [isabelle] Large datatype definition: measuring elapsed time
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:
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?
"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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and