Package: leanknit 0.0.0.9000

leanknit: A 'knitr' Engine for Lean 4 Proof Chunks

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]

leanknit_0.0.0.9000.tar.gz
leanknit_0.0.0.9000.zip(r-4.7-any)leanknit_0.0.0.9000.zip(r-4.6-any)leanknit_0.0.0.9000.zip(r-4.5-any)
leanknit_0.0.0.9000.tgz(r-4.6-any)leanknit_0.0.0.9000.tgz(r-4.5-any)
leanknit_0.0.0.9000.tar.gz(r-4.7-any)leanknit_0.0.0.9000.tar.gz(r-4.6-any)
leanknit_0.0.0.9000.tgz(r-4.6-emscripten)
manual.pdf |manual.html✨
DESCRIPTION |NEWS
card.svg |card.png
leanknit/json (API)

# Install 'leanknit' in R:

install.packages('leanknit', repos = c('https://sounkou-bioinfo.r-universe.dev', 'https://cloud.r-project.org'))

Bug tracker:https://github.com/sounkou-bioinfo/leanknit/issues

On CRAN:

2.70 score 4 scripts 11 exports 8 dependencies

Last updated from:0fc77e836c. Checks:9 OK. Indexed: yes.

Target	Result	Time
linux-devel	OK	101
source / vignettes	OK	150
linux-release	OK	98
macos-release	OK	111
macos-oldrel	OK	97
windows-devel	OK	67
windows-release	OK	70
windows-oldrel	OK	65
wasm-release	OK	87

Exports:eng_lean find_lake install_lean lean_sitrep lean_version leanknit_available leanknit_example_project leanknit_exec leanknit_get_session leanknit_list_sessions leanknit_start_session

Dependencies:evaluate highr knitr processx ps R6 xfun yaml

Checking Lean proofs in knitr documents

Running Lean | Asserting the axiom base | Expected errors | Why this matters

Rendered fromleanknit.Rmdusingknitr::rmarkdown

Last update: 2026-06-10
Started: 2026-06-10

Citation

Development and contributors

Readme and manuals

Help Manual

Help page	Topics
The 'lean' knitr engine	eng_lean
Locate the 'lake' binary	find_lake
Install the Lean 4 toolchain	install_lean
Report the leanknit / Lean toolchain situation	lean_sitrep
Report the installed Lean version	lean_version
Is a usable Lean toolchain available?	leanknit_available
A disposable copy of the bundled example lake project	leanknit_example_project
Compile a Lean source string against a lake project	leanknit_exec
Get a leanknit session, creating it if absent	leanknit_get_session
List active leanknit sessions	leanknit_list_sessions
Start (or reset) a leanknit session	leanknit_start_session