Clojure REPL interface to checked Lean project execution. Core Ansatz can be used alongside this optional module; kernel declaration import is separate.
Clojure REPL interface to checked Lean project execution. Core Ansatz can be used alongside this optional module; kernel declaration import is separate.
(call project name & arguments)(close! value)(function project name)Resolve an admitted checked function as an IFn bound to this Project. Exact integers, Boolean and strings retain ordinary Clojure carriers. Unit is nil; decoded products/lists are vectors, Option is nil or {:some value}. IO returns {:value value :stdout text :stderr text}. Unsupported codecs throw explicitly.
Resolve an admitted checked function as an IFn bound to this Project. Exact
integers, Boolean and strings retain ordinary Clojure carriers. Unit is nil;
decoded products/lists are vectors, Option is nil or {:some value}. IO returns
{:value value :stdout text :stderr text}. Unsupported codecs throw explicitly.(load-artifact runtime input expected-manifest-sha)The caller owns INPUT. EXPECTED-MANIFEST-SHA comes from a trusted descriptor.
The caller owns INPUT. EXPECTED-MANIFEST-SHA comes from a trusted descriptor.
(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.
Load trusted source using explicit compiler options, passed as a map or a ProjectOptions object. No native installation or download is implicit.
(open)(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.
Compile trusted source into OUTPUT without opening a JVM Project. Caller owns OUTPUT; keep the returned manifest hash separately in trusted configuration.
(project-options {:keys [compiler root-module source-root entries]
: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.
Explicit compiler configuration and requested entry names. A vector of names uses native signature discovery; a map can request legacy checked profiles.
(run-main project)cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |