diff options
| -rw-r--r-- | Cargo.lock | 307 | ||||
| -rw-r--r-- | Cargo.toml | 3 | ||||
| -rw-r--r-- | isabelle-proto/Cargo.toml | 14 | ||||
| -rw-r--r-- | isabelle-proto/src/main.rs | 312 | ||||
| -rw-r--r-- | isabelle-unicode/src/lib.rs | 17 |
5 files changed, 632 insertions, 21 deletions
@@ -1,6 +1,85 @@ # This file is automatically @generated by Cargo. # It is not intended for manual editing. [[package]] +name = "aho-corasick" +version = "0.7.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f" +dependencies = [ + "memchr", +] + +[[package]] +name = "ansi_term" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ee49baf6cb617b853aa8d93bf420db2383fab46d314482ca2803b40d5fde979b" +dependencies = [ + "winapi", +] + +[[package]] +name = "atty" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +dependencies = [ + "hermit-abi", + "libc", + "winapi", +] + +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + +[[package]] +name = "clap" +version = "2.33.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "37e58ac78573c40708d45522f0d80fa2f01cc4f9b4e2bf749807255454312002" +dependencies = [ + "ansi_term", + "atty", + "bitflags", + "strsim", + "textwrap", + "unicode-width", + "vec_map", +] + +[[package]] +name = "heck" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d621efb26863f0e9924c6ac577e8275e5e6b77455db64ffa6c65c904e9e132c" +dependencies = [ + "unicode-segmentation", +] + +[[package]] +name = "hermit-abi" +version = "0.1.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" +dependencies = [ + "libc", +] + +[[package]] +name = "isabelle-proto" +version = "0.1.0" +dependencies = [ + "isabelle-unicode", + "regex", + "serde", + "serde_json", + "structopt", +] + +[[package]] name = "isabelle-unicode" version = "0.1.0" dependencies = [ @@ -8,12 +87,234 @@ dependencies = [ ] [[package]] -name = "symbolmacro" +name = "isabelle2unicode" version = "0.1.0" +dependencies = [ + "isabelle-unicode", +] + +[[package]] +name = "itoa" +version = "0.4.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b71991ff56294aa922b450139ee08b3bfc70982c6b2c7562771375cf73542dd4" + +[[package]] +name = "lazy_static" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" + +[[package]] +name = "libc" +version = "0.2.102" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2a5ac8f984bfcf3a823267e5fde638acc3325f6496633a5da6bb6eb2171e103" + +[[package]] +name = "memchr" +version = "2.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a" + +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9f5105d4fdaab20335ca9565e106a5d9b82b6219b5ba735731124ac6711d23d" +dependencies = [ + "unicode-xid", +] + +[[package]] +name = "quote" +version = "1.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "regex" +version = "1.5.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.6.25" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b" + +[[package]] +name = "ryu" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "71d301d4193d031abdd79ff7e3dd721168a9572ef3fe51a1517aba235bd8f86e" + +[[package]] +name = "serde" +version = "1.0.130" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f12d06de37cf59146fbdecab66aa99f9fe4f78722e3607577a5375d66bd0c913" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.130" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7bc1a1ab1961464eae040d96713baa5a724a8152c1222492465b54322ec508b" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.68" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0f690853975602e1bfe1ccbf50504d67174e3bcf340f23b5ea9992e0587a52d8" +dependencies = [ + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "strsim" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" + +[[package]] +name = "structopt" +version = "0.3.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf9d950ef167e25e0bdb073cf1d68e9ad2795ac826f2f3f59647817cf23c0bfa" +dependencies = [ + "clap", + "lazy_static", + "structopt-derive", +] + +[[package]] +name = "structopt-derive" +version = "0.4.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "134d838a2c9943ac3125cf6df165eda53493451b719f3255b2a26b85f772d0ba" +dependencies = [ + "heck", + "proc-macro-error", + "proc-macro2", + "quote", + "syn", +] [[package]] -name = "util" +name = "symbolmacro" version = "0.1.0" + +[[package]] +name = "syn" +version = "1.0.76" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c6f107db402c2c2055242dbf4d2af0e69197202e9faacbef9571bbe47f5a1b84" dependencies = [ - "isabelle-unicode", + "proc-macro2", + "quote", + "unicode-xid", ] + +[[package]] +name = "textwrap" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" +dependencies = [ + "unicode-width", +] + +[[package]] +name = "unicode-segmentation" +version = "1.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8895849a949e7845e06bd6dc1aa51731a103c42707010a5b591c0038fb73385b" + +[[package]] +name = "unicode-width" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973" + +[[package]] +name = "unicode-xid" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3" + +[[package]] +name = "vec_map" +version = "0.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" + +[[package]] +name = "version_check" +version = "0.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5fecdca9a5291cc2b8dcf7dc02453fee791a280f3743cb0905f8822ae463b3fe" + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" @@ -2,5 +2,6 @@ members = [ "symbolmacro", "isabelle-unicode", - "isabelle2unicode" + "isabelle2unicode", + "isabelle-proto" ] diff --git a/isabelle-proto/Cargo.toml b/isabelle-proto/Cargo.toml new file mode 100644 index 0000000..351532f --- /dev/null +++ b/isabelle-proto/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "isabelle-proto" +version = "0.1.0" +authors = ["stuebinm <stuebinm@disroot.org>"] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +regex = "1" +serde = { version = "1.0.130", features = [ "derive" ] } +serde_json = "1.0.68" +isabelle-unicode = { path = "../isabelle-unicode" } +structopt = "0.3.23" 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()) + }); +} diff --git a/isabelle-unicode/src/lib.rs b/isabelle-unicode/src/lib.rs index 30a7cec..b9fcc37 100644 --- a/isabelle-unicode/src/lib.rs +++ b/isabelle-unicode/src/lib.rs @@ -53,20 +53,3 @@ impl PrettyUnicode for str { } } -// fn main() { - -// let stdin = io::stdin(); - -// stdin.lock() -// .lines() -// .filter_map(|line| match line { -// Ok(line) if line.trim().is_empty() -// => Some("\n".to_string()), -// Ok(line) -// => line.to_pretty_unicode(), -// Err(_) -// => None -// }) -// .for_each(|line| print!("{}", line)); - -// } |