Explore introducing Quiver and GRN-Lean for automated design and verification

apps/desktop/src-tauri/src/grn_validation/commands.rs

@@ -0,0 +1,65 @@
+use serde::Serialize;
+use serde_json::Value;
+use tauri::State;
+use tokio::io::AsyncWriteExt;
+use tokio::process::Command;
+
+use super::GrnLeanState;
+
+#[derive(Serialize)]
+#[serde(rename_all = "camelCase")]
+pub struct GrnAnalyzerStatus {
+    available: bool,
+    source: Option<String>,
+}
+
+#[tauri::command]
+pub fn grn_analyzer_status(state: State<'_, GrnLeanState>) -> GrnAnalyzerStatus {
+    GrnAnalyzerStatus {
+        available: state.analyzer().is_some(),
+        source: state.source().map(str::to_owned),
+    }
+}
+
+#[tauri::command]
+pub async fn grn_analyze(state: State<'_, GrnLeanState>, design: String) -> Result<Value, String> {
+    // Parse once before crossing the process boundary. The Lean executable
+    // remains authoritative for schema interpretation and certificate logic.
+    serde_json::from_str::<Value>(&design)
+        .map_err(|error| format!("Invalid design JSON: {error}"))?;
+    let analyzer = state
+        .analyzer()
+        .ok_or_else(|| "The grn-lean analyzer is not installed.".to_string())?;
+
+    let mut child = Command::new(analyzer)
+        .kill_on_drop(true)
+        .stdin(std::process::Stdio::piped())
+        .stdout(std::process::Stdio::piped())
+        .stderr(std::process::Stdio::piped())
+        .spawn()
+        .map_err(|error| format!("Could not start grn-lean: {error}"))?;
+    let mut stdin = child
+        .stdin
+        .take()
+        .ok_or_else(|| "Could not open grn-lean input.".to_string())?;
+    stdin
+        .write_all(design.as_bytes())
+        .await
+        .map_err(|error| format!("Could not send the design to grn-lean: {error}"))?;
+    drop(stdin);
+
+    let output = child
+        .wait_with_output()
+        .await
+        .map_err(|error| format!("Could not read grn-lean output: {error}"))?;
+    if !output.status.success() {
+        let stderr = String::from_utf8_lossy(&output.stderr);
+        return Err(if stderr.trim().is_empty() {
+            "grn-lean rejected the design.".to_string()
+        } else {
+            format!("grn-lean rejected the design: {}", stderr.trim())
+        });
+    }
+    serde_json::from_slice(&output.stdout)
+        .map_err(|error| format!("grn-lean returned invalid JSON: {error}"))
+}

apps/desktop/src-tauri/src/grn_validation/mod.rs

@@ -0,0 +1,63 @@
+pub mod commands;
+
+use std::path::{Path, PathBuf};
+
+/// The formal analyzer is a separate, immutable executable. Packaged builds
+/// place it under `runtime/grn-lean/analyze`; development also discovers the
+/// sibling checkout used by this workspace. `GG_GRN_LEAN_BIN` is an explicit
+/// override for contributors with another layout.
+pub struct GrnLeanState {
+    analyzer: Option<PathBuf>,
+    source: Option<&'static str>,
+}
+
+impl GrnLeanState {
+    pub fn new(resource_dir: Option<PathBuf>) -> Self {
+        let environment = std::env::var_os("GG_GRN_LEAN_BIN").map(PathBuf::from);
+        if let Some(path) = environment.filter(|path| executable_file(path)) {
+            return Self {
+                analyzer: Some(path),
+                source: Some("environment"),
+            };
+        }
+
+        let bundled = resource_dir.map(|root| root.join("runtime/grn-lean/analyze"));
+        if let Some(path) = bundled.filter(|path| executable_file(path)) {
+            return Self {
+                analyzer: Some(path),
+                source: Some("bundled"),
+            };
+        }
+
+        if cfg!(debug_assertions) {
+            let manifest = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+            let candidates = [
+                manifest.join("../../../../../marpaia/grn-lean/.lake/build/bin/analyze"),
+                manifest.join("../../../../../grn-lean/.lake/build/bin/analyze"),
+            ];
+            if let Some(path) = candidates.into_iter().find(|path| executable_file(path)) {
+                return Self {
+                    analyzer: Some(path),
+                    source: Some("development"),
+                };
+            }
+        }
+
+        Self {
+            analyzer: None,
+            source: None,
+        }
+    }
+
+    pub fn analyzer(&self) -> Option<&Path> {
+        self.analyzer.as_deref()
+    }
+
+    pub fn source(&self) -> Option<&str> {
+        self.source
+    }
+}
+
+fn executable_file(path: &Path) -> bool {
+    path.is_file()
+}

apps/desktop/src-tauri/src/lib.rs

@@ -4,6 +4,7 @@ mod backup;
 mod data;
 mod flapjack;
 mod flapjack_server;
+mod grn_validation;
 mod inspector;
 mod mcp;
 mod python;
@@ -65,6 +66,7 @@ pub fn run() {
             app.manage(flapjack_store);
 
             let resource_dir = app.path().resource_dir().ok();
+            app.manage(grn_validation::GrnLeanState::new(resource_dir.clone()));
             app.manage(python::PythonState::new(resource_dir));
             backup::start_backup_scheduler(app.handle().clone());
             mcp::spawn_initial_connect(app.handle().clone());
@@ -140,6 +142,8 @@ pub fn run() {
             sbol_server::commands::sbol_server_info,
             flapjack_server::commands::flapjack_server_ensure,
             flapjack_server::commands::flapjack_server_info,
+            grn_validation::commands::grn_analyzer_status,
+            grn_validation::commands::grn_analyze,
             flapjack::commands::flapjack_overview,
             flapjack::commands::flapjack_studies_list,
             flapjack::commands::flapjack_study_get,

apps/desktop/src-tauri/src/python/mod.rs

@@ -18,10 +18,23 @@ pub struct PythonState {
 
 impl PythonState {
     /// Resolve the interpreter and `uv` paths from the (optional) bundled
-    /// resource dir, falling back to the dev layout.
+    /// resource dir, falling back to the dev layout. Development builds prefer
+    /// the source runtime: Tauri copies resources into `target/debug`, and
+    /// macOS can reject the copied interpreter before the app is signed.
     pub fn new(resource_dir: Option<PathBuf>) -> Self {
-        let interpreter = gg_pyenv::python_executable(resource_dir.as_deref());
-        let uv = gg_pyenv::uv_executable(resource_dir.as_deref());
+        let (interpreter, uv) = if cfg!(debug_assertions) {
+            (
+                gg_pyenv::python_executable(None)
+                    .or_else(|| gg_pyenv::python_executable(resource_dir.as_deref())),
+                gg_pyenv::uv_executable(None)
+                    .or_else(|| gg_pyenv::uv_executable(resource_dir.as_deref())),
+            )
+        } else {
+            (
+                gg_pyenv::python_executable(resource_dir.as_deref()),
+                gg_pyenv::uv_executable(resource_dir.as_deref()),
+            )
+        };
         Self {
             interpreter,
             uv,
@@ -86,3 +99,37 @@ fn spawn_diagnostics_forwarder(app: AppHandle, client: Arc<PythonLspClient>) {
         }
     });
 }
+
+#[cfg(all(test, debug_assertions))]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn debug_runtime_prefers_source_tree_over_copied_resources() {
+        let (Some(expected_python), Some(expected_uv)) = (
+            gg_pyenv::python_executable(None),
+            gg_pyenv::uv_executable(None),
+        ) else {
+            eprintln!("skipping: source Python or uv runtime not found");
+            return;
+        };
+
+        let resource_dir = tempfile::tempdir().unwrap();
+        let runtime = resource_dir.path().join("runtime");
+        #[cfg(not(windows))]
+        let (copied_python, copied_uv) =
+            (runtime.join("python/bin/python3"), runtime.join("uv/uv"));
+        #[cfg(windows)]
+        let (copied_python, copied_uv) =
+            (runtime.join("python/python.exe"), runtime.join("uv/uv.exe"));
+        std::fs::create_dir_all(copied_python.parent().unwrap()).unwrap();
+        std::fs::create_dir_all(copied_uv.parent().unwrap()).unwrap();
+        std::fs::write(&copied_python, []).unwrap();
+        std::fs::write(&copied_uv, []).unwrap();
+
+        let state = PythonState::new(Some(resource_dir.path().to_path_buf()));
+
+        assert_eq!(state.interpreter(), Some(&expected_python));
+        assert_eq!(state.uv(), Some(&expected_uv));
+    }
+}