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:
 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?

"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 MHonArc.