summaryrefslogtreecommitdiff
path: root/isabelle-proto/src
diff options
context:
space:
mode:
authorstuebinm2021-09-21 22:25:59 +0200
committerstuebinm2021-09-21 22:50:24 +0200
commit5a021caf3ff516c110571bfb4485e833ba8b1d06 (patch)
treebfaff792077a25c0754f6e7beed10e3f4864dd86 /isabelle-proto/src
parent2eebd7b354432ae564757a93c7b8c44150b58010 (diff)
proof of concept: talking to `isabelle server`
for now this just checks a file given on the command line, and panics if anything at all goes wrong.
Diffstat (limited to '')
-rw-r--r--isabelle-proto/src/main.rs312
1 files changed, 312 insertions, 0 deletions
diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs
new file mode 100644
index 0000000..1ee20a9
--- /dev/null
+++ b/isabelle-proto/src/main.rs
@@ -0,0 +1,312 @@
+
+use regex::Regex;
+use serde::{Deserialize, Serialize, de::DeserializeOwned};
+use serde_json::{Result, Value};
+
+use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}};
+
+use isabelle_unicode::PrettyUnicode;
+
+use structopt::StructOpt;
+
+type SessionID = String;
+type TaskID = String;
+
+#[derive(Serialize, Deserialize)]
+#[serde(untagged)]
+enum ClientCommand {
+ UseTheories {
+ session_id : SessionID,
+ theories : Vec<String>,
+ master_dir : Option<String>
+ },
+ SessionStart {
+ session : String,
+ include_sessions : Vec<String>
+ },
+ Echo (String),
+ ShutDown
+}
+
+#[derive(Debug)]
+enum SyncAnswer<T,E> {
+ Ok (T),
+ Error (E),
+}
+
+enum AsyncAnswer<T, E, N> {
+ Finished (T),
+ Failed (E),
+ Note (N)
+}
+
+#[derive(Deserialize, Debug)]
+struct ClientHello {
+ isabelle_id : String,
+ isabelle_version : String
+}
+
+#[derive(Deserialize)]
+struct SessionStartedOk {
+ session_id : String,
+ tmp_dir : String,
+ task : String
+}
+
+#[derive(Deserialize)]
+struct SessionStartedNote {
+ percentage : u8,
+ task : TaskID,
+ message : String,
+ kind : String,
+ session : String,
+ theory : String
+}
+
+#[derive(Deserialize, Clone, Debug)]
+struct SessionStartedFinished {
+ session_id : SessionID,
+ tmp_dir : String,
+ task : TaskID
+}
+
+
+
+#[derive(Deserialize, Clone, Debug)]
+struct UseTheoriesFinished {
+ ok : bool,
+ errors : Vec<IsabelleError>,
+ nodes : Vec<IsabelleNode>,
+ task : TaskID,
+}
+
+#[derive(Deserialize, Clone, Debug)]
+struct IsabelleError {
+ kind : String,
+ message : String,
+ pos : Span
+}
+
+#[derive(Deserialize, Clone, Debug)]
+struct IsabelleNode {
+ messages : Vec<IsabelleError>,
+ exports : Vec<()>,
+ status : Status,
+ theory_name : String,
+ node_name : String
+}
+
+#[derive(Deserialize, Clone, Debug)]
+struct Status {
+ percentage : u8,
+ unprocessed : u64,
+ running : u64,
+ finished : u64,
+ failed : u64,
+ total : u64,
+ consolidated : bool,
+ canceled : bool,
+ ok : bool,
+ warned : u64
+}
+
+#[derive(Deserialize,Clone, Debug)]
+struct Span {
+ line : u64,
+ offset : u64,
+ end_offset : u64,
+ file : String
+}
+
+#[derive(Deserialize)]
+struct AsyncStartOk {
+ task : TaskID
+}
+
+fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
+where T: Deserialize<'a> {
+ let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
+ let mat = regex.find(msg)?;
+ let ty = &msg[..mat.end()];
+ let rest = &msg[mat.end()..];
+
+ match ty {
+ "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
+ "ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
+ _ => None
+ }
+}
+
+fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
+where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
+ let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
+ let mat = regex.find(msg)?;
+ let ty = &msg[..mat.end()];
+ let rest = &msg[mat.end()..];
+
+ match ty {
+ "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
+ "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
+ "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
+ _ => None
+ }
+}
+
+
+
+trait Encode {
+ fn encode (&self) -> String;
+}
+
+impl Encode for ClientCommand {
+ fn encode (&self) -> String {
+ let ty = match self {
+ ClientCommand::UseTheories {..} => "use_theories",
+ ClientCommand::SessionStart {..} => "session_start",
+ ClientCommand::Echo (..) => "echo",
+ ClientCommand::ShutDown => "shutdown"
+ };
+
+ let blob = serde_json::to_string(self).unwrap();
+
+ let res = ty.to_owned() + &blob + "\n";
+ res
+ }
+}
+
+fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
+ for res in pipe.lines() {
+ match res {
+ Err(_) => (),
+ Ok(line) => {
+ let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
+ if let Some(SyncAnswer::Ok(data)) = hello {
+ return Some(data);
+ }
+ }
+ }
+ }
+ None
+}
+
+
+fn wait_for_async_task<'a,T,E,N,F>
+ (reader: &mut BufReader<ChildStdout>, task: &str, mut prog: F) -> Option<T>
+where T: DeserializeOwned, E: DeserializeOwned, N: DeserializeOwned,
+F: FnMut(N)
+{
+ for res in reader.lines() {
+ match res {
+ Err(_) => (),
+ Ok(line) => {
+ let regex = Regex::new(r"^[0-9]+$").unwrap();
+ if regex.is_match(&line) {
+
+ } else {
+ match decode_async::<T,E,N>(&line)? {
+ AsyncAnswer::Finished(data)
+ => return Some(data),
+ AsyncAnswer::Failed(_failed)
+ => panic!("building session failed"),
+ AsyncAnswer::Note(val) => prog(val)
+ }
+ }
+ }
+ }
+ };
+ None
+}
+
+fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
+ let mut res = String::new();
+ reader.read_line(&mut res).unwrap();
+ match decode_sync(&res).unwrap() {
+ SyncAnswer::Ok(AsyncStartOk { task }) => task,
+ SyncAnswer::Error(_) => panic!("failed to start async task!")
+ }
+}
+
+#[derive(StructOpt)]
+#[structopt(name = "isabelle-proto-POC", about="proof of concept for communicating with an Isabelle server")]
+struct Options {
+ theory : String,
+ #[structopt(name="directory", default_value=Box::leak(Box::new(std::env::current_dir().unwrap().into_os_string().into_string().unwrap())))]
+ directory : String
+}
+
+fn main() {
+ let options = Options::from_args();
+ println!("will check: {} in {}", options.theory, options.directory);
+
+ let mut child = Command::new("isabelle")
+ .arg("client")
+ .stdin(Stdio::piped())
+ .stdout(Stdio::piped())
+ .stderr(Stdio::piped())
+ .spawn()
+ .expect("failed to run isabelle client!");
+
+ let stdin = child.stdin.as_mut().unwrap();
+ let stdout = child.stdout.take().unwrap();
+
+ let mut reader = BufReader::new(stdout);
+
+ let _ = wait_for_client(&mut reader);
+ // TODO: display version information?
+
+ let mut len : usize = 0;
+
+ let session_id = match std::env::var("ISABAT_SESSION_ID") {
+ Ok(id) => id,
+ Err(_) => {
+
+ // client should be ready, start a session
+ stdin.write(ClientCommand::SessionStart{
+ session: "HOL".to_string(),
+ include_sessions: vec![],
+ }.encode().as_bytes()).unwrap();
+
+ let task = get_async_task_id(&mut reader);
+
+ let started = wait_for_async_task::<SessionStartedFinished, Value, Value,_>(&mut reader, &task, |note| {
+ if let Some(Value::String(msg)) = note.get("message") {
+ len = msg.len();
+ print!("{}\r", msg);
+ std::io::stdout().flush().unwrap();
+ }
+ }).unwrap();
+
+ started.session_id
+ }
+ };
+
+
+ // HOL should be loaded now, include a theory file
+
+ stdin.write(ClientCommand::UseTheories {
+ session_id,
+ theories: vec![ options.theory ],
+ master_dir: Some(options.directory),
+ }.encode().as_bytes()).unwrap();
+
+ let task = get_async_task_id(&mut reader);
+ let result = wait_for_async_task::<UseTheoriesFinished, Value, Value, _>(&mut reader, &task, |note| {
+ if let Some(Value::String(msg)) = note.get("message") {
+ let white = len.checked_sub(msg.len()).unwrap_or(0);
+ len = msg.len();
+ print!("{}{}\r", msg, str::repeat(" ", white));
+ std::io::stdout().flush().unwrap();
+ }
+ }).unwrap();
+ println!("{}", str::repeat(" ", len));
+
+ // built a theory! Let's display errors
+
+ result
+ .errors
+ .iter()
+ .for_each(|err| {
+ println!("Isabelle Error:");
+ println!("{}", err.message.to_pretty_unicode().unwrap())
+ });
+}