ansatz.lean.jvm — org.replikativ/ansatz-lean-jvm 0.2.586

Clojure REPL interface to checked Lean project execution. Core Ansatz can be used alongside this optional module; kernel declaration import is separate.

call clj

(call project name & arguments)

call-with-options clj

(call-with-options project name options & arguments)

close! clj

(close! value)

function clj

(function project name)

(function project name options)

Retain a callable. With invocation options, each call starts fresh finite stdin; IO results additionally include defensive stdout/stderr byte arrays.

invocation-options clj

(invocation-options options)

Immutable per-call finite stdin and byte output limits. Text and bytes are mutually exclusive. Invalid options are rejected before guest execution.

load-artifact clj

(load-artifact runtime input expected-manifest-sha)

The caller owns INPUT. EXPECTED-MANIFEST-SHA comes from a trusted descriptor.

load-project clj

(load-project runtime directory options)

Load trusted source using explicit compiler options, passed as a map or a ProjectOptions object. No native installation or download is implicit.

open clj

(open)

prepare-project clj

(prepare-project directory options output)

Compile trusted source into OUTPUT without opening a JVM Project. Caller owns OUTPUT; keep the returned manifest hash separately in trusted configuration.

project-options clj

(project-options {:keys [compiler root-module source-root entries
                         installed-imports]
                  :or {root-module "Main" source-root "."}})

Explicit compiler configuration and requested entry names. A vector of names uses native signature discovery; a map can request legacy checked profiles.

run-main clj

(run-main project)