Hernán Rajchert (Oct 12 2022 at 14:33): Hernán Rajchert (Oct 12 2022 at 14:33):Hi!, we have a small language formalized in Isabelle, and we wanted to add some hints in a LSP to let the user know of some possible optimizations (for example showing that ValueAdd (Constant 1) (Constant 2) == Constant 3). Is it possible to access Isabelle rewrite capabilities from outside of Isabelle?. We are already generating Haskell code from our proofs, so it would be great if we could also generate the rewrite logic.
Mathias Fleury (Oct 12 2022 at 15:31):Easily? No. But I think that the Isabelle server can be used for such cases.
Mathias Fleury (Oct 12 2022 at 15:34):(basic idea: you generate the command value "ValueAdd (Constant 1) (Constant 2)" and parse the result. For more complex things, lemma ... apply auto or along these lines)
Manuel Eberl (Oct 12 2022 at 15:48):There's also libisabelle which has been used for such things in the past, but its status is less official than that of the Isabelle server and I do not know what its current state is.
Hernán Rajchert (Oct 18 2022 at 11:56):Thanks!
Hernán Rajchert (Apr 27 2023 at 16:18):Hi @Mathias Fleury , I'm trying the Isabelle server approach, but I don't see a way to pass commands like value expr.
If I use the help command I see the following options
["cancel","echo","help","purge_theories","session_build","session_start","session_stop","shutdown","use_theories"]
I was able to start a session using my ROOT file, but I don't know how to send a particular command.
Mathias Fleury (Apr 28 2023 at 05:08):I have never used it, so I don't really know. But from the linked documentation, it seems that you need to start a session (with session_start), and then, I am not sure. You might have to write a temporary file however
Mathias Fleury (Apr 28 2023 at 05:08):best ask those questions on the mailing list
Mathias Fleury (Apr 28 2023 at 05:09):where Makarius (the developer and probably the only person who ever used it) reads and answers
Hernán Rajchert (Apr 28 2023 at 14:05):Thanks! will do
Hernán Rajchert (Apr 28 2023 at 14:06):I got the same impression, the only way available seems to be to write a custom file
Last updated: Apr 16 2024 at 20:15 UTC