Email Gateway (Feb 26 2021 at 15:56): Email Gateway (Feb 26 2021 at 15:56):From: Boris Shminke via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi, everyone,
I use Isabelle for my research, and I find Isabelle server very helpful when you need to check dozens of theory files in parallel. My primary language is Python, so I prefer to communicate with the server through TCP. Some time ago, I wrote Python code to do that directly instead of invoking the native Isabelle client. Then I decided to take this script and create a piece of software that anyone interested can use.
Here it is: https://github.com/inpefess/isabelle-client
Any comments are welcome since the client is very raw and has only one user at the moment:)
Regards,
Boris
Email Gateway (Mar 01 2021 at 13:29):From: Makarius <makarius@sketis.net>
Great. I don't know Python myself and was hoping that someone else would start
connecting it systematically to the Isabelle server.
Your implementation looks mostly clear and straightforward. Just a few
spontaneous comments on current version d28d72f2c69e:
* examples/dummy.thy: Isabelle theories should have a capitalized name;
imports for Isabelle/HOL below the checkpoint "Main" should be avoided, to
avoid exposing the complexity of the theory/ML bootstrap to applications.
* examples/example.py "isabelle server > server.info": Here you ask user to
start the server and provide its "info" to the Python function. Can this be
done by Python as well? There is a technical delicacy behind it due to the way
how the process is started and how it outputs the stdout message (this is not
a regular Unix "daemon", because of the surrounding JVM).
* For the low-level message formats (plain line, or line with length
followed by that number of bytes), see also these reference implementations in
ML, Scala, Haskell --- it could make sense to follow the signatures more closely:
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/Pure/PIDE/byte_message.ML
* isabelle_client.use_theories: here the bulk of prover messages appear in
the response, but there is no way to "tap" into incremental message output as
it occurs. This will be probably one of the first "feature requests" (or
rather "pull requests) when some other Isabelle users discover your Python
project.
Makarius
Email Gateway (Mar 02 2021 at 13:59):From: Boris Shminke via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Great. I don't know Python myself and was hoping that someone else would start
connecting it systematically to the Isabelle server.
Thank you:)
imports for Isabelle/HOL below the checkpoint "Main" should be avoided, to
avoid exposing the complexity of the theory/ML bootstrap to applications.
Do you mean one should change 'imports HOL.Nitpick' to 'imports Main'?
Can this be done by Python as well? There is a technical delicacy behind it due to the way
how the process is started and how it outputs the stdout message (this is not
a regular Unix "daemon", because of the surrounding JVM).
Do you mean one should add a function start_isabelle_server which, e.g. runs isabelle server command and returns 'info'?
- For the low-level message formats (plain line, or line with length
followed by that number of bytes), see also these reference implementations in
ML, Scala, Haskell --- it could make sense to follow the signatures more closely:
Yes, that's good idea! I already look at the code and find it a bit primitive, so consulting some Scala code might be helpful to get some insights in doing it right.
- isabelle_client.use_theories: here the bulk of prover messages appear in
the response, but there is no way to "tap" into incremental message output as
it occurs. This will be probably one of the first "feature requests" (or
rather "pull requests) when some other Isabelle users discover your Python
project.
Yes, I already thought about that. I've created several issues following this email here: https://github.com/inpefess/isabelle-client/issues.
Thank you for helpful comments!
Cheers,
Boris
Email Gateway (Mar 04 2021 at 22:30):From: Makarius <makarius@sketis.net>
On 02/03/2021 14:58, Boris Shminke wrote:
imports for Isabelle/HOL below the checkpoint "Main" should be avoided, to
avoid exposing the complexity of the theory/ML bootstrap to applications.Do you mean one should change 'imports HOL.Nitpick' to 'imports Main'?
Yes, Main is the default import for Isabelle/HOL applications.
Can this be done by Python as well? There is a technical delicacy behind it due to the way
how the process is started and how it outputs the stdout message (this is not
a regular Unix "daemon", because of the surrounding JVM).Do you mean one should add a function
start_isabelle_serverwhich, e.g. runsisabelle servercommand and returns 'info'?
Yes.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC