| Title: | A 'knitr' Engine for Lean 4 Proof Chunks |
|---|---|
| Description: | Provides a 'knitr' language engine that compiles and checks Lean 4 code chunks against a 'lake' project, capturing proof output (including the result of '#print axioms') into rendered documents. Modeled on the 'duckknit' engine. Because a failing Lean check fails the render, a generated document cannot claim a proof that does not actually check. Also provides install_lean() to provision a Lean toolchain through 'elan', in the spirit of torch::install_torch(). |
| Authors: | Sounkou Mahamane Toure [aut, cre] |
| Maintainer: | Sounkou Mahamane Toure <[email protected]> |
| License: | GPL (>= 3) |
| Version: | 0.0.0.9000 |
| Built: | 2026-06-11 00:21:36 UTC |
| Source: | https://github.com/sounkou-bioinfo/leanknit |
lean knitr engineRegistered as knitr::knit_engines$get("lean") on package load. Not normally
called directly.
eng_lean(options)eng_lean(options)
options |
A knitr chunk options list. |
Rendered chunk output (from knitr::engine_output()).
lake binaryResolution order: the leanknit.lake option, then lake on PATH, then the
default elan install location ~/.elan/bin/lake.
find_lake()find_lake()
Absolute path to lake.
Downloads and runs the official elan
installer, which provisions elan, lake, and a Lean toolchain under
~/.elan. This mirrors the convenience of torch::install_torch(): the
heavy external toolchain is fetched on demand rather than vendored.
install_lean(toolchain = "stable", modify_path = FALSE, quiet = FALSE)install_lean(toolchain = "stable", modify_path = FALSE, quiet = FALSE)
toolchain |
Lean toolchain channel or version to install as default,
e.g. |
modify_path |
If |
quiet |
Suppress installer output. |
After installation lake lives at ~/.elan/bin/lake, which find_lake()
discovers automatically. To use lake from an interactive shell, add
~/.elan/bin to your PATH (the installer can do this for you).
The path to the elan bin directory, invisibly.
Prints the resolved lake path and version, the configured project, and any
active sessions. Useful in a document setup chunk to confirm the engine can
run before relying on it.
lean_sitrep()lean_sitrep()
A list with lake, version, project, and sessions, invisibly.
Report the installed Lean version
lean_version()lean_version()
The lean --version string, or NA if Lean is not available.
Is a usable Lean toolchain available?
leanknit_available()leanknit_available()
TRUE if find_lake() succeeds, otherwise FALSE.
Copies the small Lean project shipped under inst/lean to a fresh temporary
directory and returns its path. Used by the vignette and tests so that build
artifacts never land in the installed package. Point leanknit.project at the
returned path.
leanknit_example_project()leanknit_example_project()
Path to a writable copy of the example project.
Writes code to a temporary .lean file inside project (so import
resolves) and runs lake env lean on it.
leanknit_exec(project, code, timeout = 120000L)leanknit_exec(project, code, timeout = 120000L)
project |
Path to the lake project. |
code |
Lean source as a single string. |
timeout |
Timeout in milliseconds. |
A list with stdout, stderr, and integer status.
Get a leanknit session, creating it if absent
leanknit_get_session(name)leanknit_get_session(name)
name |
Session name. |
The session environment, invisibly.
List active leanknit sessions
leanknit_list_sessions()leanknit_list_sessions()
A data frame of session names, accumulated chunk counts, and which session is active.
Start (or reset) a leanknit session
leanknit_start_session(name)leanknit_start_session(name)
name |
Session name. |
The session environment, invisibly.