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:
leanknit_0.0.0.9000.tar.gz
leanknit_0.0.0.9000.zip(r-4.7)leanknit_0.0.0.9000.zip(r-4.6)leanknit_0.0.0.9000.zip(r-4.5)
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✨
card.svg |card.png
leanknit/json (API)
NEWS
| # 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
Last updated from:0fc77e836c. Checks:9 OK. Indexed: yes.
| Target | Result | Time | Files | Syslog |
|---|---|---|---|---|
| linux-devel-x86_64 | OK | 97 | ||
| source / vignettes | OK | 170 | ||
| linux-release-x86_64 | OK | 112 | ||
| macos-release-arm64 | OK | 94 | ||
| macos-oldrel-arm64 | OK | 96 | ||
| windows-devel | OK | 67 | ||
| windows-release | OK | 76 | ||
| windows-oldrel | OK | 68 | ||
| wasm-release | OK | 113 |
Exports:eng_leanfind_lakeinstall_leanlean_sitreplean_versionleanknit_availableleanknit_example_projectleanknit_execleanknit_get_sessionleanknit_list_sessionsleanknit_start_session
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 |
