leanknit

A knitr language engine for Lean 4 proof chunks, modeled on duckknit. A lean chunk is appended to a per-document session buffer, compiled against a configured lake project with lake env lean, and its output is captured into the rendered document.

The point is honesty: a failing Lean check fails the render, so a generated document cannot claim a proof that does not actually check.

Usage

Load the package and point it at a lake project in your document’s setup chunk:

library(leanknit)
options(leanknit.project = "proofs")

Then write lean chunks. Definitions accumulate across chunks in a session:

import TccqLir.Core
open TccqLir

#eval (2 + 3 : Int)
#> 5

The axioms chunk option appends #print axioms <name>, asserting in-document that a theorem carries no stray axioms and no sorry:

#print axioms fold_preserves
#> 'TccqLir.fold_preserves' depends on axioms: [propext]

An error=TRUE chunk shows the Lean error without aborting the render, and does not poison later chunks in the session:

theorem bogus : (1 : Int) = 2 := by rfl
#> <lean>:7:36: error: Tactic `rfl` failed: The left-hand side
#>   1
#> is not definitionally equal to the right-hand side
#>   2
#> 
#> ⊢ 1 = 2

Chunk options

• eval — set FALSE to echo the chunk without running Lean.
• session — name an independent accumulating buffer (default: one shared session).
• error — set TRUE to allow (and display) an expected Lean error.
• timeout — per-chunk timeout in milliseconds (default 120000).
• axioms — one or more theorem names; each gets a #print axioms appended.

Configuration

• options(leanknit.project=) — path to the lake project (default "proofs").
• options(leanknit.lake=) — path to lake (default: PATH, then ~/.elan/bin/lake).

lean_sitrep()
#> leanknit situation report
#> =========================
#> 
#> lake
#>   Path:    /root/.elan/bin/lake 
#>   Version: Lake version 5.0.0-src+d024af0 (Lean version 4.30.0) 
#>   Project: /root/Rtinycc/tccquickr/proofs 
#> 
#> Sessions: 1 
#>   - session-1 (3 chunks)  *

Installing Lean

If you do not already have a Lean toolchain, install_lean() provisions one via elan, in the spirit of torch::install_torch():

leanknit::install_lean()              # default "stable" toolchain
leanknit::install_lean("leanprover/lean4:v4.30.0")

leanknit_available() reports whether lake can be found, and lean_version() prints the installed version.