async server + rust client

.gitignore

@@ -163,3 +163,15 @@ cython_debug/
 
 # ignore all .out files generated by jsi runs
 **/*.out
+
+# Generated by Cargo
+# will have compiled files and executables
+**/debug/
+**/target/
+
+# Remove Cargo.lock from gitignore if creating an executable, leave it for libraries
+# More information here https://doc.rust-lang.org/cargo/guide/cargo-toml-vs-cargo-lock.html
+Cargo.lock
+
+# These are backup files generated by rustfmt
+**/*.rs.bk

jsi-client-rs/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "jsif"
+version = "0.1.0"
+edition = "2021"
+description = "just solve it fast - rust client for the jsi daemon"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

jsi-client-rs/src/main.rs

@@ -0,0 +1,49 @@
+use std::env;
+use std::io::{Read, Write};
+use std::os::unix::net::UnixStream;
+use std::path::PathBuf;
+use std::process;
+use std::time::Instant;
+
+fn get_server_home() -> Option<PathBuf> {
+    env::var_os("HOME").map(|home| {
+        let mut path = PathBuf::from(home);
+        path.push(".jsi");
+        path.push("daemon");
+        path
+    })
+}
+
+fn send_command(command: &str) -> Result<(), Box<dyn std::error::Error>> {
+    let socket_path = get_server_home().unwrap().join("server.sock");
+    let mut stream = UnixStream::connect(socket_path)?;
+
+    // Send the command
+    stream.write_all(command.as_bytes())?;
+    stream.flush()?;
+
+    // Read the response
+    let start = Instant::now();
+    let mut response = String::new();
+    stream.read_to_string(&mut response)?;
+
+    println!("{}", response);
+    println!("; response time: {:?}", start.elapsed());
+    Ok(())
+}
+
+fn main() {
+    let args: Vec<String> = env::args().collect();
+
+    if args.len() < 2 {
+        eprintln!("Usage: {} <command>", args[0]);
+        process::exit(1);
+    }
+
+    let command = args[1..].join(" ");
+
+    match send_command(&command) {
+        Ok(_) => (),
+        Err(e) => eprintln!("Error: {}", e),
+    }
+}

pyproject.toml

@@ -8,6 +8,7 @@ authors = [
 dependencies = [
     "pyright>=1.1.378",
     "rich>=13.8.1",
+    "python-daemon>=3.0.1",
 ]
 readme = "README.md"
 requires-python = ">= 3.11"

requirements-dev.lock

@@ -14,8 +14,12 @@ click==8.1.7
 colorama==0.4.6 ; sys_platform == 'win32' or platform_system == 'Windows'
     # via click
     # via pytest
+docutils==0.21.2
+    # via python-daemon
 iniconfig==2.0.0
     # via pytest
+lockfile==0.12.2
+    # via python-daemon
 markdown-it-py==3.0.0
     # via rich
 mdurl==0.1.2
@@ -31,5 +35,9 @@ pygments==2.18.0
 pyright==1.1.378
     # via jsi
 pytest==8.3.2
+python-daemon==3.0.1
+    # via jsi
 rich==13.8.1
     # via jsi
+setuptools==75.1.0
+    # via python-daemon

requirements.lock

@@ -10,6 +10,10 @@
 #   universal: false
 
 -e file:.
+docutils==0.21.2
+    # via python-daemon
+lockfile==0.12.2
+    # via python-daemon
 markdown-it-py==3.0.0
     # via rich
 mdurl==0.1.2
@@ -20,7 +24,11 @@ pygments==2.18.0
     # via rich
 pyright==1.1.382.post0
     # via jsi
+python-daemon==3.0.1
+    # via jsi
 rich==13.8.1
     # via jsi
+setuptools==75.1.0
+    # via python-daemon
 typing-extensions==4.12.2
     # via pyright

src/jsi/cli.py

@@ -55,13 +55,15 @@
 import threading
 from functools import partial
 
-from jsi.config.loader import Config, SolverDefinition, load_definitions
+from jsi.config.loader import Config, find_available_solvers, load_definitions
 from jsi.core import (
     Command,
     ProcessController,
     Task,
     TaskResult,
     TaskStatus,
+    base_commands,
+    set_input_output,
 )
 from jsi.utils import (
     LogLevel,
@@ -99,53 +101,6 @@ def get_status():
         return NoopStatus()
 
 
-def find_available_solvers(
-    solver_definitions: dict[str, SolverDefinition],
-) -> dict[str, str]:
-    if os.path.exists(solver_paths):
-        stderr.print(f"loading solver paths from cache ({solver_paths})")
-        import json
-
-        with open(solver_paths) as f:
-            try:
-                paths = json.load(f)
-            except json.JSONDecodeError as err:
-                logger.error(f"error loading solver cache: {err}")
-                paths = {}
-
-        if paths:
-            return paths
-
-    stderr.print("looking for solvers available on PATH:")
-    paths: dict[str, str] = {}
-
-    import shutil
-
-    for solver_name, solver_def in solver_definitions.items():
-        path = shutil.which(solver_def.executable)  # type: ignore
-
-        if path is None:
-            stderr.print(f"{solver_name:>12} not found")
-            continue
-
-        paths[solver_name] = path
-        stderr.print(f"{solver_name:>12} [green]OK[/green]")
-
-    stderr.print()
-
-    # save the paths to the solver_paths file
-    if paths:
-        import json
-
-        if not os.path.exists(jsi_home):
-            os.makedirs(jsi_home)
-
-        with open(solver_paths, "w") as f:
-            json.dump(paths, f)
-
-    return paths
-
-
 def setup_signal_handlers(controller: ProcessController):
     event = threading.Event()
 
@@ -221,6 +176,8 @@ def parse_args(args: list[str]) -> Config:
                 config.csv = True
             case "--supervisor":
                 config.supervisor = True
+            case "--daemon":
+                config.daemon = True
             case "--timeout":
                 config.timeout_seconds = parse_time(args[i])
                 i += 1
@@ -239,14 +196,15 @@ def parse_args(args: list[str]) -> Config:
 
                 config.input_file = arg
 
-    if not config.input_file:
-        raise BadParameterError("no input file provided")
+    if not config.daemon:
+        if not config.input_file:
+            raise BadParameterError("no input file provided")
 
-    if not os.path.exists(config.input_file):
-        raise BadParameterError(f"input file does not exist: {config.input_file}")
+        if not os.path.exists(config.input_file):
+            raise BadParameterError(f"input file does not exist: {config.input_file}")
 
-    if not os.path.isfile(config.input_file):
-        raise BadParameterError(f"input file is not a file: {config.input_file}")
+        if not os.path.isfile(config.input_file):
+            raise BadParameterError(f"input file is not a file: {config.input_file}")
 
     if config.output_dir and not os.path.exists(config.output_dir):
         raise BadParameterError(f"output directory does not exist: {config.output_dir}")
@@ -261,7 +219,7 @@ def parse_args(args: list[str]) -> Config:
         raise BadParameterError(f"invalid interval value: {config.interval_seconds}")
 
     # output directory defaults to the parent of the input file
-    if config.output_dir is None:
+    if config.output_dir is None and config.input_file:
         config.output_dir = os.path.dirname(config.input_file)
 
     return config
@@ -301,71 +259,48 @@ def main(args: list[str] | None = None) -> int:
     if config.debug:
         logger.enable(console=stderr, level=LogLevel.DEBUG)
 
+    if config.daemon:
+        import jsi.server
+
+        # this detaches the server from the current shell,
+        # this returns immediately, leaving the server running in the background
+        jsi.server.daemonize(config)
+        return 0
+
     with timer("load_config"):
-        solver_definitions = load_definitions()
+        solver_definitions = load_definitions(config)
 
     if not solver_definitions:
         stderr.print("error: no solver definitions found", style="red")
         return 1
 
     with timer("find_available_solvers"):
         # maps solver name to executable path
-        available_solvers: dict[str, str] = find_available_solvers(solver_definitions)
+        available_solvers = find_available_solvers(solver_definitions, config)
 
     if not available_solvers:
         stderr.print("error: no solvers found on PATH", style="red")
         return 1
 
     # build the commands to run the solvers
-    file = config.input_file
-    output = config.output_dir
-
-    assert file is not None
-    assert output is not None
-
-    commands: list[Command] = []
-    basename = os.path.basename(file)
-
     # run the solvers in the specified sequence, or fallback to the default order
-    for solver_name in config.sequence or available_solvers:
-        solver_def: SolverDefinition | None = solver_definitions.get(solver_name)
-        if not solver_def:
-            stderr.print(f"error: unknown solver: {solver_name}", style="red")
-            return 1
-
-        executable_path = available_solvers[solver_name]
-        args = [executable_path]
-
-        # append the model option if requested
-        if config.model:
-            if model_arg := solver_def.model:
-                args.append(model_arg)
-            else:
-                stderr.print(f"warn: solver {solver_name} has no model option")
-
-        # append solver-specific extra arguments
-        args.extend(solver_def.args)
-
-        command = Command(
-            name=solver_name,
-            args=args,
-            input_file=file,
-        )
-
-        stdout_file = os.path.join(output, f"{basename}.{solver_name}.out")
-        stderr_file = os.path.join(output, f"{basename}.{solver_name}.err")
-        command.stdout = open(stdout_file, "w")  # noqa: SIM115
-        command.stderr = open(stderr_file, "w")  # noqa: SIM115
-        commands.append(command)
+    commands: list[Command] = base_commands(
+        config.sequence or list(available_solvers.keys()),
+        solver_definitions,
+        available_solvers,
+        config,
+    )
+
+    set_input_output(commands, config)
 
     # initialize the controller
-    task = Task(name=str(file))
+    task = Task(name=str(config.input_file))
     controller = ProcessController(task, commands, config, get_exit_callback())
 
     setup_signal_handlers(controller)
 
     stderr.print(f"starting {len(commands)} solvers")
-    stderr.print(f"output will be written to: {output}{os.sep}")
+    stderr.print(f"output will be written to: {config.output_dir}{os.sep}")
     status = get_status()
     try:
         # all systems go
@@ -414,7 +349,12 @@ def main(args: list[str] | None = None) -> int:
             from jsi.output.basic import get_results_csv
 
             csv = get_results_csv(controller)
-            csv_file = os.path.join(output, f"{basename}.csv")
+
+            assert config.input_file is not None
+            assert config.output_dir is not None
+
+            basename = os.path.basename(config.input_file)
+            csv_file = os.path.join(config.output_dir, f"{basename}.csv")
             stderr.print(f"writing results to: {csv_file}")
             with open(csv_file, "w") as f:
                 f.write(csv)

src/jsi/client.py

@@ -0,0 +1,26 @@
+# client.py
+
+import socket
+import sys
+
+from jsi.server import SOCKET_PATH
+
+
+def send_command(command: str):
+    with socket.socket(socket.AF_UNIX, socket.SOCK_STREAM) as client:
+        try:
+            client.connect(SOCKET_PATH.as_posix())
+            client.sendall(command.encode())
+            response = client.recv(4096).decode()
+            print(response)
+        except OSError as e:
+            print(f"Error: {e}")
+
+
+if __name__ == "__main__":
+    if len(sys.argv) < 2:
+        print("Usage: python client.py <command>")
+        sys.exit(1)
+
+    command = " ".join(sys.argv[1:])
+    send_command(command)

src/jsi/config/definitions.json

@@ -33,7 +33,10 @@
         "executable": "z3",
         "model": "--model",
         "args": []
+    },
+    "always-sat": {
+        "executable": "echo",
+        "model": null,
+        "args": ["sat", "\n; input:"]
     }
 }
-
-