Isabelle Client
Mix.install([
{:isabelle_elixir, "~> 0.1"},
])Optional: Start Isabelle locally
Optionally: If you want to start (and list) Isabelle servers programmatically via the function new_server (and list_servers) you have to make sure that the /bin directory is in the PATH. Note that this only works if running Livebook directly on the host where Isabelle is installed (if running Livebook from a container this won’t work without additional tweaking).
System.get_env("PATH")"/data/isabelle/bin:/usr/local/lib/erlang/erts-15.2.2/bin:/usr/local/lib/erlang/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin"
Uncomment (and modify) below to add Isabelle’s bin folder to PATH (if you haven’t done already).
#isabelle_dir = "/data/isabelle"
#System.put_env("PATH", isabelle_dir <> "/bin:" <> System.get_env("PATH"))nilSmoke test your setup by getting a list of currently running Isabelle servers on your machine.
#server_info = IsabelleClientMini.list_servers()[
%{
"host" => "127.0.0.1",
"name" => "my",
"password" => "e7b5c739-ac69-4588-817b-f1669629f348",
"port" => "9998"
}
]Start a server (in case of trouble double-check for port collisions)
#server_info = IsabelleClientMini.new_server("my", 9998)[
%{
"host" => "127.0.0.1",
"name" => "my",
"password" => "e7b5c739-ac69-4588-817b-f1669629f348",
"port" => "9998"
}
]Connecting to an Isabelle Server
Assume you have an Isabelle server instance running in host and listening to port (for example you ran isabelle server -n -p on host where Isabelle has been installed, or alternatively via the function new_server).
You can connect to this instance and get a socket (an instance of Port).
pw = "4d450549-5afc-43cd-8684-323ec2630fc5" # you get this from Isabelle CLI when starting server
host = "127.0.0.1"
port = 9999
socket = IsabelleClientMini.connect(pw, host, port)#Port<0.22>Using Isabelle Server
import IsabelleClientMiniIsabelleClientMiniecho(socket, %{value: 3}){:ok, %{"value" => 3}}help(socket){:ok,
["cancel", "echo", "help", "purge_theories", "session_build", "session_start", "session_stop",
"shutdown", "use_theories"]}
Interactions with Isabelle occur in the context of a session. See Isabelle System Manual for details.
Simple examples can be done in the context of Main.
start_session(socket, %{session: "Main"})
Process.sleep(5_000) # Building the session takes some time:ok
We poll the status of the previous invocation (session start). The status object has useful information for further tasks (in particuular the current session_id).
status = poll_status(socket)[
note: %{
"kind" => "writeln",
"message" => "Session Pure/Pure",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session Misc/Tools",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session HOL/HOL (main)",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session Doc/Main (doc)",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session Pure/Pure",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session Misc/Tools",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session HOL/HOL (main)",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Session Doc/Main (doc)",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "true"
},
note: %{
"kind" => "writeln",
"message" => "Starting session Main ...",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"verbose" => "false"
},
finished: %{
"session_id" => "ed1378dc-f5b4-4df9-a103-ecd04c5bdb11",
"task" => "a53ea6a2-5d29-4a74-954d-bcf3136486d7",
"tmp_dir" => "/tmp/isabelle-mx/server_session13878966386288091748"
}
]
We extract the session_id of the Main session we started before and save it for further use.
session_id = extract_session(status)"ed1378dc-f5b4-4df9-a103-ecd04c5bdb11"
Isabelle proof (and model generation) problems are given in the context of “theories”, which are read from homonymous files having extension .thy). Below we create one that declares a new type i and an (arbitrary) relation R on is. It uses Sledgehammer to mathematically prove that reflexivity and euclideanness together entail transitivity, and to disprove some other random conjecture (by finding a counterexample using Nitpick).
theory = ~S"""
theory Problem imports Main
begin
typedecl i
consts R::"i \ i \ bool"
abbreviation "reflexive \ \ x. R x x"
abbreviation "euclidean \ \ x y z. R x y \ R x z \ R y z"
abbreviation "transitive \ \ x y z. R x y \ R y z \ R x z"
theorem "reflexive \ euclidean \ transitive"
sledgehammer
oops
proposition "reflexive \ transitive \ euclidean"
nitpick[card = 4, show_all, format = 2, atoms= a b c d] oops
end
""""theory Problem imports Main\nbegin\n\ntypedecl i\nconsts R::\"i \\ i \\ bool\"\n\nabbreviation \"reflexive \\ \\ x. R x x\"\nabbreviation \"euclidean \\ \\ x y z. R x y \\ R x z \\ R y z\" \nabbreviation \"transitive \\ \\ x y z. R x y \\ R y z \\ R x z\" \n\ntheorem \"reflexive \\ euclidean \\ transitive\"\n sledgehammer\n oops\n\nproposition \"reflexive \\ transitive \\ euclidean\"\n nitpick[card = 4, show_all, format = 2, atoms= a b c d] oops\n\nend\n"Unfortunately the Isabelle server doesn’t support sending theories over the wire. So we have to save the theory in a (for Isabelle accessible) location in disk. Modify the path below according to your own Livebook setup
# The path below is the one seen by Livebook (possibly different if running inside a container)
path_wrt_livebook = "/data/problems/"
File.write!(path_wrt_livebook <> "Problem.thy", theory):ok
We send the previously saved theory to Isabelle for formal verification by invoking use_theories (and passing it the corresponding parameters as an args Map). Modify the path below according to your own setup!
# The path below is the one seen by Isabelle (possibly different than the one seen by Livebook
# if running in different hosts/containers)
path_wrt_isabelle = "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/"
args = %{
"session_id" => session_id,
"theories" => ["Problem"],
"master_dir" => path_wrt_isabelle
}
{:ok, _} = use_theories(socket, args)
# This might take some time
Process.sleep(5_000):oktheory_status = poll_status(socket) # Poll until you get the results[
note: %{
"kind" => "writeln",
"message" => "theory Draft.Problem 3%",
"percentage" => 3,
"session" => "",
"task" => "90bfbf6b-be83-493a-9efb-7b3a28712058",
"theory" => "Draft.Problem"
},
note: %{
"kind" => "writeln",
"message" => "theory Draft.Problem 99%",
"percentage" => 99,
"session" => "",
"task" => "90bfbf6b-be83-493a-9efb-7b3a28712058",
"theory" => "Draft.Problem"
},
note: %{
"kind" => "writeln",
"message" => "theory Draft.Problem 100%",
"percentage" => 100,
"session" => "",
"task" => "90bfbf6b-be83-493a-9efb-7b3a28712058",
"theory" => "Draft.Problem"
},
finished: %{
"errors" => [],
"nodes" => [
%{
"exports" => [],
"messages" => [
%{
"kind" => "writeln",
"message" => "consts\n reflexive :: \"bool\"",
"pos" => %{
"end_offset" => 85,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 7,
"offset" => 73
}
},
%{
"kind" => "writeln",
"message" => "consts\n euclidean :: \"bool\"",
"pos" => %{
"end_offset" => 123,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 8,
"offset" => 111
}
},
%{
"kind" => "writeln",
"message" => "consts\n transitive :: \"bool\"",
"pos" => %{
"end_offset" => 182,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 9,
"offset" => 170
}
},
%{
"kind" => "writeln",
"message" => "Sledgehammering...",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "verit found a proof...",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "cvc5 found a proof...",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "vampire found a proof...",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "zipperposition found a proof...",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "verit: Try this: by metis (29 ms)",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "cvc5: Try this: by meson (33 ms)",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "vampire: Duplicate proof",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "zipperposition: Duplicate proof",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "Done",
"pos" => %{
"end_offset" => 290,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 12,
"offset" => 278
}
},
%{
"kind" => "writeln",
"message" => "Nitpicking formula...",
"pos" => %{
"end_offset" => 357,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 16,
"offset" => 350
}
},
%{
"kind" => "writeln",
"message" => "Nitpick found a counterexample for card i = 4:\n Skolem constants:\n x = a\n y = b\n z = c\n Constant:\n R = (\\x. _)\n ((a, a) := True, (a, b) := True, (a, c) := True, (a, d) := True,\n (b, a) := False, (b, b) := True, (b, c) := False,\n (b, d) := False, (c, a) := False, (c, b) := True, (c, c) := True,\n (c, d) := True, (d, a) := False, (d, b) := False,\n (d, c) := False, (d, d) := True)",
"pos" => %{
"end_offset" => 357,
"file" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"line" => 16,
"offset" => 350
}
}
],
"node_name" => "/home/mx/Dropbox/AISE-Auto/livebook-local/problems/Problem.thy",
"status" => %{
"canceled" => false,
"consolidated" => true,
"failed" => 0,
"finished" => 26,
"ok" => true,
"percentage" => 100,
"running" => 0,
"total" => 26,
"unprocessed" => 0,
"warned" => 0
},
"theory_name" => "Draft.Problem"
}
],
"ok" => true,
"task" => "90bfbf6b-be83-493a-9efb-7b3a28712058"
}
]result = extract_results(theory_status)
IO.puts resultconsts
reflexive :: "bool"
consts
euclidean :: "bool"
consts
transitive :: "bool"
Sledgehammering...
verit found a proof...
cvc5 found a proof...
vampire found a proof...
zipperposition found a proof...
verit: Try this: by metis (29 ms)
cvc5: Try this: by meson (33 ms)
vampire: Duplicate proof
zipperposition: Duplicate proof
Done
Nitpicking formula...
Nitpick found a counterexample for card i = 4:
Skolem constants:
x = a
y = b
z = c
Constant:
R = (\x. _)
((a, a) := True, (a, b) := True, (a, c) := True, (a, d) := True,
(b, a) := False, (b, b) := True, (b, c) := False,
(b, d) := False, (c, a) := False, (c, b) := True, (c, c) := True,
(c, d) := True, (d, a) := False, (d, b) := False,
(d, c) := False, (d, d) := True):okWe can further parse the resulting string for downstream processing.
symbol = "R"
value =
result
|> String.split("Constant:\n", parts: 2)
|> Enum.at(1)
|> String.trim()
|> String.split("#{symbol} =", parts: 2)
|> Enum.at(1)
IO.puts(value) (\x. _)
((a, a) := True, (a, b) := True, (a, c) := True, (a, d) := True,
(b, a) := False, (b, b) := True, (b, c) := False,
(b, d) := False, (c, a) := False, (c, b) := True, (c, c) := True,
(c, d) := True, (d, a) := False, (d, b) := False,
(d, c) := False, (d, d) := True):okrel =
~r/\(\s*(\w+)\s*,\s*(\w+)\s*\)\s*:=\s*True/
|> Regex.scan(value, capture: :all_but_first)
|> Enum.map(fn [a, b] -> {String.to_atom(a), String.to_atom(b)} end)
|> MapSet.new()MapSet.new([a: :a, a: :b, a: :c, a: :d, b: :b, c: :b, c: :c, c: :d, d: :d])
The extracted MapSet (as a counterexample to our conjecture) represents a binary relation that is reflexive and transitive but not euclidean.
For example , we can convert this into a directed graph using Erlang stdlib module digraph and use corresponding library functionality.
g = :digraph.new()
# 1) Add every unique vertex first
rel
|> Enum.flat_map(fn {u, v} -> [u, v] end)
|> Enum.uniq()
|> Enum.each(&:digraph.add_vertex(g, &1))
# 2) Add directed edges for each pair
Enum.each(rel, fn {u, v} -> :digraph.add_edge(g, u, v) end)
g{:digraph, #Reference<0.3715232518.1354104836.13731>, #Reference<0.3715232518.1354104836.13732>,
#Reference<0.3715232518.1354104836.13733>, true}:digraph.edges(g)[
[:"$e" | 1],
[:"$e" | 6],
[:"$e" | 0],
[:"$e" | 2],
[:"$e" | 4],
[:"$e" | 7],
[:"$e" | 3],
[:"$e" | 8],
[:"$e" | 5]
]A topological sorting is a graph traversal in which each node v is visited only after all its dependencies are visited.
:digraph_utils.topsort(g)[:a, :c, :b, :d]
