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.

5 files changed, 632 insertions, 21 deletions

diff --git a/Cargo.lock b/Cargo.lock
index cc3df91..add763a 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -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"
diff --git a/Cargo.toml b/Cargo.toml
index fbb6fcd..a9f9380 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -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));
-
-// }