leanknit registers a
lean knitr engine. A lean chunk is compiled
and checked against a lake project with
lake env lean; its output is captured below it. If no Lean
toolchain is found (see install_lean()), chunks degrade to
a friendly notice so the document still renders.
Definitions accumulate across chunks within a session:
import LeanknitDemo
#eval (1 + 1 : Nat)
#> ## leanknit: lake not found; chunk not evaluated.The axioms chunk option appends
#print axioms <name>. This puts the trust base of a
theorem in the rendered document — and, crucially, fails the render if a
sorry ever sneaks in. The bundled one_add_one
is proved by rfl, so it depends on nothing:
#> ## leanknit: lake not found; chunk not evaluated.A chunk marked error=TRUE shows the Lean error instead
of aborting the render, and does not poison later chunks in the
session:
theorem bogus : (1 : Nat) = 2 := rfl
#> ## leanknit: lake not found; chunk not evaluated.Because a failing check fails the render, a generated
.md/.html cannot claim a proof that does not
actually hold. The document and the proof state cannot drift apart.