[isabelle-dev] datatype takes minutes, but timing panel shows 10s

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Thu Apr 9 15:28:09 CEST 2015


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.)

Best,
Andreas

datatype family
   = AF_UNSPEC
   | AF_UNIX
   | AF_INET
   | AF_INET6
   | AF_IMPLINK
   | AF_PUP
   | AF_CHAOS
   | AF_NS
   | AF_NBS
   | AF_ECMA
   | AF_DATAKIT
   | AF_CCITT
   | AF_SNA
   | AF_DECnet
   | AF_DLI
   | AF_LAT
   | AF_HYLINK
   | AF_APPLETALK
   | AF_ROUTE
   | AF_NETBIOS
   | AF_NIT
   | AF_802
   | AF_ISO
   | AF_OSI
   | AF_NETMAN
   | AF_X25
   | AF_AX25
   | AF_OSINET
   | AF_GOSSIP
   | AF_IPX
   | Pseudo_AF_XTP
   | AF_CTF
   | AF_WAN
   | AF_SDL
   | AF_NETWARE
   | AF_NDD
   | AF_INTF
   | AF_COIP
   | AF_CNT
   | Pseudo_AF_RTIP
   | Pseudo_AF_PIP
   | AF_SIP
   | AF_ISDN
   | Pseudo_AF_KEY
   | AF_NATM
   | AF_ARP
   | Pseudo_AF_HDRCMPLT
   | AF_ENCAP
   | AF_LINK
   | AF_RAW
   | AF_RIF
   | AF_NETROM
   | AF_BRIDGE
   | AF_ATMPVC
   | AF_ROSE
   | AF_NETBEUI
   | AF_SECURITY
   | AF_PACKET
   | AF_ASH
   | AF_ECONET
   | AF_ATMSVC
   | AF_IRDA
   | AF_PPPOX
   | AF_WANPIPE
   | AF_BLUETOOTH


More information about the isabelle-dev mailing list