Email Gateway (Aug 13 2025 at 11:31): Email Gateway (Aug 13 2025 at 11:31):From: Makarius <makarius@sketis.net>
On 13/08/2025 09:35, Tobias Nipkow wrote:
I tuned another slow proof in HOL-Analysis.
Using the timimg panel, I was surprised that this showed up:
- HOL-Analysis.Infinite_Sum
- 91.8 command "text"Does that have anything to do with the cite command in that text block?
I cannot reproduce this problem, neither in your version Isabelle/304519f22c2c
nor in official Isabelle2025.
* What happens when you use Isabelle2025, the official download?
* What happens when you delete the cite antiquotation?
Makarius
Email Gateway (Aug 13 2025 at 12:15):From: Manuel Eberl <manuel@pruvisto.org>
Might be obvious, but just in case: did you try running this command a
few more times? If I recall correctly, timings are sometimes spuriously
very high on innocuous commands. Perhaps due to garbage collection.
Manuel
On 13/08/2025 13:30, Makarius wrote:
On 13/08/2025 09:35, Tobias Nipkow wrote:
I tuned another slow proof in HOL-Analysis.
Using the timimg panel, I was surprised that this showed up:
- HOL-Analysis.Infinite_Sum
- 91.8 command "text"Does that have anything to do with the cite command in that text block?
I cannot reproduce this problem, neither in your version
Isabelle/304519f22c2c nor in official Isabelle2025.* What happens when you use Isabelle2025, the official download?
* What happens when you delete the cite antiquotation?
Makarius
Email Gateway (Aug 13 2025 at 13:02):From: Tobias Nipkow <nipkow@in.tum.de>
Isabelle 2025 behaves the same for me. The way I tested it was to load
Analysis.thy a number of times, without significant other system load. The
actual time for the text block differs but is always in the 20-90 secs range.
However, when I remove the cite, the timing issue disappears.
Tobias
On 13/08/2025 13:30, Makarius wrote:
On 13/08/2025 09:35, Tobias Nipkow wrote:
I tuned another slow proof in HOL-Analysis.
Using the timimg panel, I was surprised that this showed up:
- HOL-Analysis.Infinite_Sum
- 91.8 command "text"Does that have anything to do with the cite command in that text block?
I cannot reproduce this problem, neither in your version Isabelle/304519f22c2c
nor in official Isabelle2025.* What happens when you use Isabelle2025, the official download?
* What happens when you delete the cite antiquotation?
Makarius
Email Gateway (Aug 16 2025 at 15:53):From: Makarius <makarius@sketis.net>
On 13/08/2025 15:02, Tobias Nipkow wrote:
The way I tested it was to load
Analysis.thy a number of times, without significant other system load. The
actual time for the text block differs but is always in the 20-90 secs range.
However, when I remove the cite, the timing issue disappears.
That way, I managed to see a reported timing of approx. 60s for the 'text'
command with "cite" antiquotation, but not every time.
Behind the "cite" antiquotation is quite some complexity: Isabelle/ML needs to
ask Isabelle/Scala to parse bibtex files --- but results are made persistent
for the underlying session, and the bibtex parsing is quite fast in the first
place.
After further experimentation with the implementation, it looks like the high
number is caused by lots of proof tasks running in parallel to an asynchronous
request from ML to Scala and back to ML. There is no long-running task behind
it, just delays in elapsed time.
Conclusion: nothing to be seen here; can be ignored.
Makarius
Email Gateway (Aug 16 2025 at 17:49):From: Makarius <makarius@sketis.net>
On 16 Aug 2025, at 16:53, Makarius <makarius@sketis.net> wrote:
After further experimentation with the implementation, it looks like the
high number is caused by lots of proof tasks running in parallel to an
asynchronous request from ML to Scala and back to ML. There is no long-running
task behind it, just delays in elapsed time.
On 16/08/2025 18:09, Lawrence Paulson wrote:
The timing panel is subject to extreme variations depending on what else is going on. I guess this is part of poly/ML and cannot be fixed.
We have many things stacked on top of each other: Poly/ML, Isabelle/ML,
Isabelle/Scala.
Timings are expected to occasionally inaccurate, especially in a parallel and
asynchronous system like Isabelle.
Makarius
Last updated: Aug 20 2025 at 20:23 UTC