From c6090f4b7fe238c34d4e15ceda0f1d9812a54276 Mon Sep 17 00:00:00 2001 From: stuebinm Date: Tue, 26 Oct 2021 17:47:29 +0200 Subject: slightly less hacky proof of concept --- isabelle-proto/src/main.rs | 89 +++++++---------------------- isabelle-proto/src/session.rs | 126 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 145 insertions(+), 70 deletions(-) create mode 100644 isabelle-proto/src/session.rs diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs index 1ee20a9..b16b8ac 100644 --- a/isabelle-proto/src/main.rs +++ b/isabelle-proto/src/main.rs @@ -1,9 +1,13 @@ +mod session; + use regex::Regex; use serde::{Deserialize, Serialize, de::DeserializeOwned}; use serde_json::{Result, Value}; +use session::IsabelleSession; use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}}; +use std::fmt::Debug; use isabelle_unicode::PrettyUnicode; @@ -170,6 +174,7 @@ impl Encode for ClientCommand { let blob = serde_json::to_string(self).unwrap(); let res = ty.to_owned() + &blob + "\n"; + println!("encoded: {}", res); res } } @@ -192,7 +197,7 @@ fn wait_for_client(pipe: &mut BufReader) -> Option { fn wait_for_async_task<'a,T,E,N,F> (reader: &mut BufReader, task: &str, mut prog: F) -> Option -where T: DeserializeOwned, E: DeserializeOwned, N: DeserializeOwned, +where T: DeserializeOwned, E: DeserializeOwned + Debug, N: DeserializeOwned, F: FnMut(N) { for res in reader.lines() { @@ -206,8 +211,8 @@ F: FnMut(N) match decode_async::(&line)? { AsyncAnswer::Finished(data) => return Some(data), - AsyncAnswer::Failed(_failed) - => panic!("building session failed"), + AsyncAnswer::Failed(failed) + => panic!("building session failed: {:?}", failed), AsyncAnswer::Note(val) => prog(val) } } @@ -234,79 +239,23 @@ struct Options { 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(); +fn main() { + let options = Options::from_args(); + let mut session = IsabelleSession::start_with_client(); - let task = get_async_task_id(&mut reader); + let started = session.start_session("HOL".to_owned(),vec![]).unwrap(); - let started = wait_for_async_task::(&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(); + println!("{:?}", started); - started.session_id - } - }; + let theoryresults = session.load_theory( + options.theory, + Some(options.directory) + ); + println!("loaded theory: {:?}", theoryresults); +} - // 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::(&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()) - }); -} diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs new file mode 100644 index 0000000..85081d4 --- /dev/null +++ b/isabelle-proto/src/session.rs @@ -0,0 +1,126 @@ +use std::{io::{BufRead, BufReader, Write}, process::{ChildStdin, ChildStdout, Command, Stdio}}; + +use regex::Regex; +use serde::de::DeserializeOwned; +use serde_json::Value; + +use crate::{AsyncAnswer, ClientCommand, Encode, SessionStartedFinished, UseTheoriesFinished, decode_async, get_async_task_id, wait_for_client}; + + + + +pub struct IsabelleSession { + reader : BufReader, + writer : ChildStdin, + session_id : Option +} + +impl IsabelleSession { + pub fn start_with_client() -> Self { + 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 mut reader = BufReader::new(child.stdout.take().unwrap()); + let a = wait_for_client(&mut reader); + println!("client hello: {:?}", a); + IsabelleSession { + writer: child.stdin.unwrap(), + reader, + session_id: None + } + } + + pub fn start_session(&mut self, session : String, include_sessions : Vec) + -> Result + { + + self.writer.write(ClientCommand::SessionStart { + session, include_sessions + }.encode().as_bytes()).unwrap(); + let task_id = get_async_task_id(&mut self.reader); + let started = self.await_task::(&task_id, |_n| {}) + // .await + .unwrap(); + + match started { + Ok(ref finished) => self.session_id = Some(finished.session_id.to_owned()), + Err(_) => () + }; + + started + } + + + pub fn load_theory(&mut self, theory : String, master_dir : Option) + -> Result { + let session_id = self.session_id.as_ref().unwrap(); + + self.writer.write(ClientCommand::UseTheories { + session_id: session_id.clone(), + theories: vec![ theory ], + master_dir, + }.encode().as_bytes()).unwrap(); + + let task_id = get_async_task_id(&mut self.reader); + + self.await_task::(&task_id, |_| {}) + .unwrap() + } + + + + fn await_task<'a,T,E,N,F>( + &mut self, + task_id: &str, + mut prog: F) + -> Option> + where T: DeserializeOwned, + E: DeserializeOwned, + N: DeserializeOwned, + F: FnMut(N) + { + let reader = &mut self.reader; + for res in reader.lines() { + match res { + Err(err) => { + eprintln!("error while reading from pipe: {}", err); + std::process::exit(1); + }, + Ok(line) => { + let regex = Regex::new(r"^[0-9]+$").unwrap(); + if regex.is_match(&line) { + // TODO: we don't support the long style of messages yet … + // the following just assumes that the next blob is json + // and does not contain line breaks. + } else { + // TODO: this shouldn't have to parse the json twice + let value : Value = match decode_async(&line).unwrap() { + AsyncAnswer::Finished(v) => v, + AsyncAnswer::Failed(v) => v, + AsyncAnswer::Note(v) => v + }; + match value.get("task") { + Some(id) if id == task_id => + Some(match decode_async::(&line).unwrap() { + AsyncAnswer::Finished(data) + => return Some(Ok(data)), + AsyncAnswer::Failed(failed) + => return Some(Err(failed)), + AsyncAnswer::Note(val) => prog(val) + + }), + _ => return None + }; + } + } + } + } + unreachable!{} + None + } +} -- cgit v1.2.3