Email Gateway (Oct 30 2023 at 16:25): Email Gateway (Oct 30 2023 at 16:25):From: Andrea Vezzosi <vezzosi.ndr@gmail.com>
Hi,
I am using isabelle server to programmatically check isabelle theories
from a separate process.
I have noticed that it takes around ~20s to check a fairly small and simple
theory (3/4 lemmas, each proven by auto).
According to the Timings panel in Isabelle/jEdit checking the same theory
takes instead around 3.5s.
Is there a way to get the isabelle server time down to the one of jEdit
? As far as I understand they are both built upon the PIDE functionality,
so I was hoping they would be fairly close in performance.
Should I rather be using some other interface to programmatically interact
with isabelle? I had been using isabelle build but I noticed I get more
complete feedback on the theory from isabelle server in case of errors.
Here's a truncated log of my interaction with isabelle server:
00:00:00 session_start {"dirs":[...],"session":"Backgrounds"}
00:00:00 OK {"task":"c2647269-8493-46df-9d17-bed67dd44169"}
00:00:03 FINISHED
{"session_id":"2728ab87-e1f2-48db-b5c7-a83f06dd5b24","tmp_dir":"...","task":"c2647269-8493-46df-9d17-bed67dd44169"}
<NOTE several times>
00:00:00 use_theories
{"check_limit":50,"session_id":"2728ab87-e1f2-48db-b5c7-a83f06dd5b24","theories":["/path/to/thys/TheoryName"]}
00:00:00 OK {"task":"b669c563-4568-471b-b6d8-6f83e90e82d7"}
<NOTE several times>
00:00:15 FINISHED {"ok":false,"errors":[...], "nodes":[...]}
00:00:00 session_stop {"session_id":"2728ab87-e1f2-48db-b5c7-a83f06dd5b24"}
00:00:00 OK {"task":"431c096f-d8c8-44dd-8da3-6984d7713bfa"}
The 3 and 15 seconds are the time elapsed since the "OK" message.
On the other hand I start jEdit with isabelle jedit -R Backgrounds. The
Backgrounds session uses HOL as base session and is previously built.
Best Regards,
Andrea Vezzosi
Email Gateway (Nov 10 2023 at 09:33):From: Andrea Vezzosi <vezzosi.ndr@gmail.com>
The solution seems to be to set headless_consolidate_delay to 1s, as
opposed to the 15s default, to bring it in line with
editor_consolidate_delay.
What is the downside of a shorter consolidate delay? Is it only wasted
computation if the theory is changed soon after?
Best Regards,
Andrea
Email Gateway (Nov 26 2023 at 13:17):From: Makarius <makarius@sketis.net>
These defaults go back to a time, when "isabelle dump" was important to export
content from AFP (approx. 2018/2019). I had struggled quite a bit to make it
work most of the time, with 64 GB RAM and 24-48h runtime. Later that huge PIDE
session was replaced by regular "isabelle build" with a few special options,
e.g. "isabelle build -o export_theory".
What is the downside of a shorter consolidate delay? Is it only wasted
computation if the theory is changed soon after?
The consolidation of theory processing does require notable time. It depends
on your application what is best: e.g. short delays for small theories with
lots of updates, or long delays for big theories with few updates.
I have now changed the defaults for the next Isabelle release here:
https://isabelle-dev.sketis.net/rISABELLE212c94edae2b -- including a small
example in the "system" manual, to make more clear that there are options that
can be adjusted.
Makarius
Last updated: Apr 29 2024 at 04:18 UTC