[isabelle] Performance bottleneck in Theory_Data.merge



Hi,

I try to track down a performance bottleneck in theory merge.

I enabled timing information by

ML “val _ = Context.timing := true”


Unfortunately the position information of the “slow" data slot is not available, I just get the message:

Theory_Data.merge
44.390s elapsed time, 88.221s cpu time, 0.000s GC time

Compared to other data slots where the position information is available as a link or a file reference:

Theory_Data.merge⌂
0.016s elapsed time, 0.030s cpu time, 0.000s GC time

Theory_Data.merge (file "global_theory.ML")
0.264s elapsed time, 0.523s cpu time, 0.000s GC time


Any idea how to continue?

What is the reason that the position information is lost? Could this be a hint which kind of data slot it could possibly be?

Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification





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