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