Eric Bond (Sep 15 2022 at 01:02): 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:
Pure
HOL-Eisbach.Eisbach
…
Draft.Word_Lemmas
Draft.Word_8
…
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: Apr 25 2024 at 08:20 UTC