[isabelle] Large datatype definition: measuring elapsed time



Hi,

I'm formalizing the syntax of IPv6 Addresses.

I made a quite large datatype.

https://github.com/diekmann/Iptables_Semantics/blob/ccc5d5f9f0e09834c676cb36380409c095e6580d/thy/Bitmagic/IPv6Addr.thy#L98

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.