Email Gateway (Aug 03 2023 at 05:50): Email Gateway (Aug 03 2023 at 05:50):From: hannobecker@posteo.de
Hi,
I am working on a large development for which continuous proof checking
in Isabelle/jEdit gets increasingly slow on my local machine.
(How) Can one offload continuous proof checking to a remote server,
while continuing to run jEdit locally? (Switching to VSCode is also an
option if things are more flexible there).
Thanks,
Hanno
Email Gateway (Aug 08 2023 at 15:37):From: Makarius <makarius@sketis.net>
Note that Isabelle/VSCode is just an experimental PIDE front-end, and still
two orders of magnitude behind Isabelle/jEdit in sophistication.
Concerning remote checking: that has been vital many decades ago, and today it
re-occurs in rare situations. Can you be more specific, what your application
is like? How many CPU cores and how many GB of RAM does it usually require?
And how many CPU cores and GB RAM does your local machine have? 4-8 cores and
16-32 GB RAM should be considered normal for regular Isabelle applications,
and no reason for the extra complexity of remote computation.
In contrast, my impression is that the primary importance of remote checking
is to build huge library sessions in the background (e.g. portions of AFP),
while only a relatively small application is edited in the foreground (e.g.
the increment wrt. the background library).
Makarius
Email Gateway (Aug 10 2023 at 12:55):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
We largely develop locally on Apple M1 MacBook Pros with 32GB RAM.
Proof-checking time is now approaching an hour on these machines
despite significant effort being expended in trying to optimize our
automation setup to keep builds as efficient as possible. However, we also
have access to machines with 192 cores and terabytes of RAM—and every other
machine configuration imaginable—hence the motivation for Hanno's question.
Email Gateway (Aug 10 2023 at 21:51):From: Makarius <makarius@sketis.net>
Large numbers of cores and memory may sound important, but scaling is never
for free, and certainly not linear.
Such server class hardware is usually targeted at "cloud" services, with many
independent workloads and relative modest (virtual) hardware parameters.
It depends on CPU speed, caches, and NUMA memory architecture, how much of
performance you can get for Isabelle. For a single ML process, it is very hard
to go beyond 16 cores and 64 GB RAM: it will become slow and unresponsive (due
to excessive GC).
High-end consumer machines often work better. like the current Macbook Pro M2
or M2 max.
With the updated version of Poly/ML in Isabelle2023-RC3, ARM64 should work
fine: please test it now.
Makarius
Email Gateway (Aug 10 2023 at 23:04):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Email Gateway (Aug 11 2023 at 08:55):From: Makarius <makarius@sketis.net>
On 11/08/2023 01:04, Dominic Mulligan (via cl-isabelle-users Mailing List) wrote:
As mentioned, we have access to any sort of machine configuration one could
reasonably imagine and resource constraints imposed by co-tenancy and
virtualisation are not a concern in this context. Moreover, we can freely spin
up machines to test which ones work well and which ones do not, if needed,
empirically.
Maybe you can run some concrete test with "isabelle build" to get some
measurements, and compare the results. It is rare that some "cloud"
infrastructure is much faster than a high-end local machine.
With the updated version of Poly/ML in Isabelle2023-RC3, ARM64 should work
fine: please test it now.We tested RC2 and observed no performance boost, but rather a minor
performance decrease in batch build benchmarking compared to Isabelle2022 on
our laptops. Is there reason to expect RC3 will be substantially different?
Isabelle2023-RC3 is substantially different on ARM64: it used to crash
occasionally and people had to switch back to Intel x86_64 (which is a bit
slower).
Now is the time to test and confirm that ARM64 works without side-conditions.
(Note we will probably still update despite this, once the final release is
out, to take advantage of the maturing PolyML runtime for AArch64—as
previously discussed on this list we have been observing long GC pauses and
deadlocks in interactive editing with Isabelle2022 on AArch64.
Time for testing is now. When the final release is out, there will be no
opportunity to change things until the next release.
From your first reply to Hanno it seems that this distributed client/remote
server mode of use of Isabelle is indeed possible and is also maybe currently
in use for large developments. Is there a handy example you could point to?
I don't know of any concrete setup.
Presently, I am still busy with remote batch-builds, to run "isabelle build"
on many hosts in parallel. That introduces many technical side-conditions and
possibilities for failure, and will take some time to finish.
Proper remote execution is not for free, but requires explicit efforts to make
it robust.
Makarius
Email Gateway (Aug 11 2023 at 09:05):From: Makarius <makarius@sketis.net>
For Isabelle2023 there have been many changes in internal data structures for
core concepts, e.g. name spaces. This usually saves ML heap space, and thus
indirectly GC time. It can also cost extra runtime elsewhere, but should
normally be not that relevant.
If you can point out particular problems, in the next 2 weeks before the
release becomes final, I might still be able to address them --- like I did in
https://isabelle.sketis.net/repos/isabelle-release/rev/3fdf3c5cfa9d
Before the release things can be changed, after the release they can't.
Makarius
Email Gateway (Aug 11 2023 at 09:50):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Isabelle2023-RC3 is substantially different on ARM64: it used to crash
Ok, thanks for clarifying the status of RC2/RC3 for Arm. We will give it a
go.
Thanks,
Dominic
Last updated: Apr 29 2024 at 04:18 UTC