Jonathan Julian Huerta y Munive (May 23 2024 at 12:20): Jonathan Julian Huerta y Munive (May 23 2024 at 12:20):Hi, I want to find the Isabelle/ML and Isabelle/Scala functions in charge of communicating both worlds. The way I currently understand Isabelle's inner workings is that there is a "thread" managing the messages from both systems. I am interested in the functions (from both sides) that send and receive the messages to/from this "thread". If this is not the correct model, an explanation with pointers to the code would be desirable. Written in another way, I am interested in the functions corresponding to the "internal protocol" part in slide 5 of these slides. Thanks!
Fabian Huch (May 23 2024 at 15:47):What are you trying to achieve, exactly? There are many moving parts here, and your question is too broad to answer well.
Fabian Huch (May 23 2024 at 15:57):Certainly there is no 'single thread that manages all communication and lives outside the system' if that is what you mean
Fabian Huch (May 23 2024 at 15:58):On a technical level, there are System channels and Databases for IPC.
Jonathan Julian Huerta y Munive (May 23 2024 at 16:35):I am trying to understand Isabelle better to decide the best approach to interface the proving process with Python. Suppose I want to use this Python library. I would like to build a heap, postulate a theorem from Python from that point, receive a filtered list of possible methods and proven theorems from this heap, choose the proof method and its arguments from Python, ask Isabelle/ML to send back the new Proof.state after using that method, and repeat. After looking at Isabelle's scala files, it seems to me that doing it via Isabelle/scala would alleviate the need of building my own YXML parsers, document model, thread management, and all the engineering already there.
Fabian Huch (May 23 2024 at 18:10):Yes, I would highly recommend simply using Isabelle/Scala instead of trying to interact with the raw Poly/ML process.
Jonathan Julian Huerta y Munive (May 24 2024 at 12:26):Fabian Huch said:
On a technical level, there are System channels and Databases for IPC.
Based on this, I guess I would like to pinpoint how the proof state is updated from the Isabelle/scala part. Reading the libraries takes a lot of time. Is the process described precisely somewhere with pointers to the code?
Fabian Huch (May 24 2024 at 15:16):No, the precise document is the code itself. Maybe you are better off using the Isabelle server to send theory snippets/receive results? Of course it doesn't scale as well, but it's easy to use from the outside, and there are even python bindings for the API.
Fabian Huch (May 24 2024 at 15:19):Anyway, the state is updated via Document.Edits (see Pure/PIDE/document.scala), which are progressed from within the ML process.
Jonathan Julian Huerta y Munive (May 24 2024 at 17:37):Thanks @Fabian Huch. I'll take my time to understand Isabelle/Scala. I think I am making good progress on that front.
Jonathan Julian Huerta y Munive (Jun 18 2024 at 08:00):For future reference to whoever is interested: the most useful file to answer my question was session.scala. The file has its own model of the prover and it declares various Consumer_Threads to interact with it and the PIDE. Interesting threads in that file are manager, dispatcher and change_parser. Among the messages that they handle are Prover.Outputs and Prover.Inputs. Accordingly, the file prover.scala provides the Prover class extending the referred Protocol in the slides linked above. The protocol is implemented in both the scala side (protocol.scala) and the ML side (protocol.ML). Then, as Fabian stated, Document.Edits are sent to the ML side which contain the code snippets that Isabelle/ML processes.
Chengsong Tan (Sep 23 2024 at 14:29):Jonathan Julian Huerta y Munive said:
For future reference to whoever is interested: the most useful file to answer my question was
session.scala. The file has its own model of theproverand it declares variousConsumer_Threads to interact with it and the PIDE. Interesting threads in that file aremanager,dispatcherandchange_parser. Among the messages that they handle areProver.Outputs andProver.Inputs. Accordingly, the fileprover.scalaprovides theProverclass extending the referredProtocolin the slides linked above. The protocol is implemented in both the scala side (protocol.scala) and the ML side (protocol.ML). Then, as Fabian stated,Document.Editsare sent to the ML side which contain the code snippets that Isabelle/ML processes.
Hi Julian,
Thanks very much for this very useful information! I am now also trying to come up with some automated tools utilizing Isabelle/Scala.
I was wondering if you have any "hello world" snippets you can share? For instance what code in Isabelle/Scala did you write to cause an edit to happen without actually editing in jedit? Or how do you intercept the messages returned by the prover IDE and print them to stdout instead?
Thanks a lot for any help in advance!
Best wishes,
Chengsong
Jonathan Julian Huerta y Munive (Sep 25 2024 at 09:44):@Chengsong Tan I am sorry to write that I do not have anything quick to follow/share with you. Basically, I used the develop version of Isabelle with its Mercurial version control and modified the code in a personal "branch" in session.scala so that the manager and the dispatcher printed to the standard output some messages that they send and receive. However, after reading them and the protocol.scala I felt that the messages that they send are very specific for the PIDE. Right now I am using Dominique Unruh's scala-isabelle which seems to work for my purposes. If you wish, we can discuss more privately about each other's objectives and maybe we can align them.
Jonathan Julian Huerta y Munive (Sep 25 2024 at 10:06):If you want to go the "official" way, code that might be useful to read appears in PIDE/headless.scala (e.g. resources.start_session) and its interaction with Tools/server_commands.scala
Last updated: Dec 21 2024 at 12:33 UTC