[isabelle] Performance bottleneck in Theory_Data.merge


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:

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:

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?



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

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