Email Gateway (Oct 10 2022 at 10:14): Email Gateway (Oct 10 2022 at 10:14):From: pdevant <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I am experimenting with the isabelle server and came across a problem with the
purge_theories command.
Given: A basic theory with a trivial lemma in it like this:
lemma test: "true = true"
sledgehammer
sorry
The Goal is to make isabelle server run sledgehammer and then insert the found
solution.
By using isabelle server together with start_session and use_theories i am
already able to get the proof and insert it using my own script.
Then i want to run sledgehammer again by executing use_theories in the same
way on the same theory file that now looks like this:
lemma test: "true = true"
by simp
sledgehammer
sorry
I would expect isabelle server to say something like "bad context" or "no
subgoals to solve". But what actually happens is that it prints the exact same
sledgehammer output again. After carefully reading the documentation i found
out that in order to actually update the theory, that isabelle server
processes, you need to run "purge_theories" before executing "use_theories" a
second time. However this does not affect the outcome, although the server
confirms that it did the purge.
{'purged': [{'node_name': '<REMOVED>/tests/ressources/prove/testfile3.thy',
'theory_name': 'Draft.testfile3'}], 'retained': []}
Is there anything i am missing? Did I missinterpret the documentation? Or is
this a bug?
Best regards,
Pascal
Email Gateway (Oct 17 2022 at 14:26):From: Makarius <makarius@sketis.net>
I have spent a few days investigating the situation, and producing a few
last-minute changes for the headless PIDE session, which is behind e.g.
"isabelle server" and "isabelle dump".
The result is now
https://isabelle.sketis.net/repos/isabelle-release/rev/14cf5a50c1e9 which has
the following update on Isabelle2022/NEWS:
The headless PIDE session now supports adhoc editing of theories via
repeated "use_theories" on changed files. This functionality was
originally intended (e.g. see Isabelle2018), but it got lost due to
later improvements of "isabelle dump". Now it should work again, e.g. as
follows for "isabelle server &" and "isabelle client":
session_start {"session": "HOL", "options":
["headless_consolidate_delay=0.5", "headless_prune_delay=5"]}
use_theories {"session_id": "...", "theories": ["/home/makarius/tmp/Test"]}
use_theories {"session_id": "...", "theories": ["/home/makarius/tmp/Test"]}
purge_theories {"session_id":"...", "all": true}
session_stop {"session_id": "..."}
shutdown
The next release candidate Isabelle2022-RC4 will appear within 1-2 days. You
can either wait and hope for the best, or try out the above repository version
in the meantime: it is relatively simple to build as explained in
https://isabelle.sketis.net/repos/isabelle-release/file/tip/README_REPOSITORY
-- but you need to clone https://isabelle.sketis.net/repos/isabelle-release
The final release of Isabelle2022 will appear 1 week later. It will remain
unchanged until the next release after it (approx. Sep-2023).
Makarius
Email Gateway (Oct 18 2022 at 13:54):From: Makarius <makarius@sketis.net>
That was only 1 day, and only 1 week left for last-minute final testing.
See https://isabelle.sketis.net/website-Isabelle2022-RC4 and
https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/
Makarius
Last updated: Apr 24 2024 at 01:07 UTC