[isabelle-dev] datatype takes minutes, but timing panel shows 10s
makarius at sketis.net
Sat Apr 18 21:28:47 CEST 2015
On Thu, 9 Apr 2015, Andreas Lochbihler wrote:
> Dear BNF and Isabelle/jEdit developers,
> Today, I noticed that the datatype command in Isabelle/e936c2828bec is
> sometimes extremely slow. At the end of this mail, there is a large
> enumeration type where this shows up. Processing this definition on my laptop
> takes about 4 minutes, but the timing panel from the Plugins/Isabelle menu
> just shows 11.398 seconds for the datatype command.
> In Isabelle2014, processing this datatype declaration takes about one minute.
> So what has happened in between? (The Isabelle2014 timing panel is also way
> off with 8 seconds.)
The Timing panel merely visualizes certain protocol information from Isar
command transactions. So far, i.e. in Isabelle2014,
Isabelle/e936c2828bec, the forthcoming Isabelle2015, this covers only the
synchronous transaction time, i.e. the elpased time span until the next
transaction can start, while the previous transaction might still have
internal forks to be finished.
This should eventually become a bit more advanced. It is particularly
important to include contious timings, without awaiting termination.
Thus there would be a chance to visualize long-running and potentially
non-terminating tasks in the IDE.
More information about the isabelle-dev