Email Gateway (Aug 22 2022 at 20:13): Email Gateway (Aug 22 2022 at 20:13):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear users(ccing other interested users),
I am trying to use Isabelle client to talk to Isabelle server. I want to
send a JSON request to Isabelle server saying that a given top-level
command in my theory was edited.
What is the corresponding JSON request? I imagine, to do such a request, I
need the Isabelle server command that somehow takes as argument the ID of
the top-level command !
In the sequel is a successfully tested example from
https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessions
Best wishes,
Yakoub
EXAMPLE**
isabelle client
server "isabelle" = 127.0.0.1:34329 (password
"e64b1abe-1b8a-4c61-b4c5-fbe7eb04b350")
OK {"isabelle_id":"91162dd89571","isabelle_version":"Isabelle2018: August
2018"}
session_start {"session": "HOL"}
OK {"task":"8b1d25b4-dc1e-420d-b377-72d419fdded0"}
NOTE {"kind":"writeln","message":"Starting HOL
...","task":"8b1d25b4-dc1e-420d-b377-72d419fdded0"}
177
FINISHED
{"session_id":"b11041f2-ac33-43c0-94ac-715d6f26fd41","tmp_dir":"/tmp/isabelle-yakoubn/server_session1411428207973312821","task":"8b1d25b4-dc1e-420d-b377-72d419fdded0"}
use_theories {"session_id": "b11041f2-ac33-43c0-94ac-715d6f26fd41",
"theories":["~~/src/HOL/ex/Seq"]}
OK {"task":"70b9abee-bfa2-428c-b8b2-b5b08119be0c"}
133
NOTE
{"task":"70b9abee-bfa2-428c-b8b2-b5b08119be0c","session":"","theory":"Draft.Seq","message":"theory
Draft.Seq","kind":"writeln"}
838
FINISHED
{"ok":true,"errors":[],"nodes":[{"messages":[{"kind":"writeln","message":"Found
termination order: \"(\\<lambda>p. size (fst p)) <mlex>
{}\"","pos":{"line":13,"offset":163,"end_offset":166,"file":"/home/yakoubn/Desktop/Work/Practice/Isabelle2018_app/Isabelle2018/src/HOL/ex/Seq.thy"}},{"kind":"writeln","message":"Found
termination order: \"size <mlex>
{}\"","pos":{"line":18,"offset":276,"end_offset":279,"file":"/home/yakoubn/Desktop/Work/Practice/Isabelle2018_app/Isabelle2018/src/HOL/ex/Seq.thy"}}],"theory_name":"Draft.Seq","node_name":"/home/yakoubn/Desktop/Work/Practice/Isabelle2018_app/Isabelle2018/src/HOL/ex/Seq.thy","exports":[],"status":{"unprocessed":0,"initialized":true,"running":0,"finished":29,"failed":0,"total":29,"consolidated":true,"ok":true,"warned":0}}],"task":"70b9abee-bfa2-428c-b8b2-b5b08119be0c"}
session_stop {"session_id":"70b9abee-bfa2-428c-b8b2-b5b08119be0c"}
OK {"task":"4f792742-0f98-4b94-bc63-c048bc9e3d82"}
132
FAILED {"kind":"error","message":"No session
'70b9abee-bfa2-428c-b8b2-b5b08119be0c'","task":"4f792742-0f98-4b94-bc63-c048bc9e3d82"}
session_stop {"session_id":"b11041f2-ac33-43c0-94ac-715d6f26fd41"}
OK {"task":"3330a613-28cd-4d17-aa70-d42a15ee0575"}
FINISHED
{"ok":true,"return_code":0,"task":"3330a613-28cd-4d17-aa70-d42a15ee0575"}
shutdown
OK
Email Gateway (Aug 22 2022 at 20:15):From: Makarius <makarius@sketis.net>
As explained in the documentation ("system" manual chapter 4), the
Isabelle server takes document content from the file-system, e.g. a
temporary directory provided by the session context. PIDE edits are
derived from that for each use_theories protocol command (section 4.4.8).
Fine-grained PIDE command IDs are not directly involved here. The server
protocol imitates old-style REPL interaction in some sense.
Makarius
Email Gateway (Aug 22 2022 at 20:16):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
I thought that Isabelle server is the future for developing Isabelle apps
in a very clean way.
But, if it does not support all the features of PIDE protocol, it does not
make sens to me to use it now!
Maybe it is too early to start using it.
Any further development in the future for Isabelle server or it is meant
for something else?
I have one more question, will the usage of the non fine grained command
"use_theories" affect the the performance of the application?
How scalable it is with regard the fine grained PIDE commands?
The amazing feature of Isabelle is its parallel infrastructure and fine
grained PIDE protocol commands allows to take full advantage of that.
What is the best way to use "use_theories" to take advantage of the
parallel infrastructure of Isabelle?
It is very important to me to have some numbers on "use_theories", and know
its limitations, in order I take the right decision to develop my next
application.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:16):From: Makarius <makarius@sketis.net>
On 15/07/2019 11:52, Yakoub Nemouchi wrote:
I thought that Isabelle server is the future for developing Isabelle
apps in a very clean way.
But, if it does not support all the features of PIDE protocol, it does
not make sens to me to use it now!
Maybe it is too early to start using it.
Any further development in the future for Isabelle server or it is meant
for something else?
Have you studied the documentation ("system" manual chapter 4)?
The server does support full PIDE, but presents it in a more
conventional way, with a directory of your choice as local scratchpad.
The main PIDE application (Isabelle/jEdit) does that on its own account,
using the builtin file-system view of the jEdit text editor (which is by
itself not an IDE).
I have one more question, will the usage of the non fine grained command
"use_theories" affect the the performance of the application?
It depends how you do it. You can present the server updated files and
repeated use_theories protocol commands. The headless PIDE session
should do the right thing about it, i.e. derive edits from the implicit
change of files and re-check what needs to be re-checked, in the same
manner.
Makarius
Last updated: Apr 26 2024 at 16:20 UTC