Stream: Isabelle/ML

Topic: Isabelle Console seL4

view this post on Zulip Eric Bond (Sep 15 2022 at 01:02):

We’re able to run isabelle process on theories in the AFP via the command:

isabelle process -T ../afp/thys/Word_Lib/Word_8 -e "Thy_Info.get_names () |> map writeln"

This gives us the following output:



However, when we run a similar command on l4v:

isabelle process -T ../l4v/proof/bisim/Separation -e "Thy_Info.get_names () |> map writeln"

We get errors like this:

*** exception Fail raised (line 57 of "System/isabelle_system.ML"): Bad bash_process server address
*** At command "apply" (line 2964 of "~~/src/HOL/Library/Word.thy")

We saw mention of a server here, so we started an isabelle server like so:

isabelle server

Then, when we re-run the command, we get a different error:

*** Malformed message header: "OK {"isabelle_id":"c2a2be496f35","isabelle_name":"Isabelle2021-1"}"
*** At command "by" (line 139 of "~/workspace/l4v/lib/More_Numeral_Type.thy")
*** Malformed message header: "OK

When we start the server and then use a client and run

session_start {"session":"HOL", "dirs":["/workspace/l4v"]}
use_theories {"session_id":"263e7eca-9b8a-43ed-b94a-ae835d60555f", "theories":["/workspace/l4v//proof/bisim/Separation"]}

We are able to load theories
I've had a hard time deciphering this error message and no luck reading the manual. Any thoughts :)?
Our goal is to drop into an ML process/console with L4V theories loaded so that we can perform data extraction using ML code.

Last updated: Dec 07 2023 at 12:30 UTC