Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Performance of AFP/Padic_Fields

Email Gateway (Aug 07 2025 at 10:11):

From: Makarius <makarius@sketis.net>
On 30/06/2025 20:52, Manuel Eberl wrote:

The entry in question is "Padic_Field", and the theory that is affected most
severely is "Padic_Field_Powers". We talked about this entry quite a bit when
it was first submitted three years ago. Back then the performance problems
were so severe I was wondering whether we could even accept it.

The entire entry is still pretty slow for what it is. But it's not as
excessive as it once was. I asked the author to try to reduce the context
switches as much as possible and that already helped a lot. But I also think
some of the other performance tuning you did to Isabelle since then also helped.

As it stands now, there are still two "context" commands in there that take
about 5 s (elapsed) on my machine, namely in line 41 and line 10404. The
"lemma" command on line 2837 and the subsequent "blast" call also take about 2
seconds each, presumably due to the context switch induced by "(in
padic_fields)". As I recall, this used to be almost an order of magnitude worse.

Of course, 2 or 5 seconds is not dramatic. But in a development that uses
locales quite a bit, these numbers accumulate to an extent that makes working
with such a development interactively (especially during refactoring) very
annoying.

Thanks for the detailed report. I have looked around a bit in that session: it
requires more work to understand its uses of locales and potential problems of
that infrastructure (or the application).

I am also including measurements from the past two years, always on the same
hardware: it shows that nothing has really changed so far.

Makarius

Padic_Field.csv

Email Gateway (Aug 07 2025 at 15:36):

From: Lawrence Paulson <lp15@cam.ac.uk>
Sorting in the order of the build date, I get the following. It is a bit jagged, and the maximum value of timing_cpu is 777000.

Larry
[PastedGraphic-2.png]
On 7 Aug 2025, at 11:10, Makarius <makarius@sketis.net> wrote:

Thanks for the detailed report. I have looked around a bit in that session: it requires more work to understand its uses of locales and potential problems of that infrastructure (or the application).

I am also including measurements from the past two years, always on the same hardware: it shows that nothing has really changed so far.

Makarius
<Padic_Field.csv>

PastedGraphic-2.png

Email Gateway (Aug 07 2025 at 17:23):

From: Makarius <makarius@sketis.net>
On 07/08/2025 17:35, Lawrence Paulson wrote:

Sorting in the order of the build date, I get the following. It is a bit
jagged, and the maximum value of timing_cpu is 777000.

The build_date is somewhat accidental. Relevant is the pull_date, i.e. the
date when a the nightly-build daemon has first seen a certain changeset (via
"hg pull").

Makarius

Last updated: Aug 20 2025 at 20:23 UTC