A Lean 4 port of the Iris tutorial, originally developed as a Rocq tutorial, based on iris-lean.

The book is written in Verso: prose and Lean proofs live together in the same .lean files, and every proof is elaborated (type-checked) by the same toolchain that renders the book.

The build produces two outputs from one source:

• the rendered HTML book, and
• a downloadable code.zip of the extracted, compilable example modules.

This is a work in progress. The following chapters are fully ported and type-checked:

• Basics
• Pure
• Lang
• Specifications
• Persistently
• Linked Lists
• Later

The remaining chapters are stubs ("This chapter has not yet been ported") pending translation from their Rocq sources.

The Lean toolchain is pinned to leanprover/lean4:v4.32.2 in lean-toolchain, matching iris-lean. lakefile.toml pins iris-lean to upstream HEAD as of 2026-09-05 (728a17140939e49af9236f7cb0d037da9ec52435) and Verso to v4.32.0. Keep dependency revisions compatible with the toolchain.

• IrisTutorialBook.lean — the #doc book root: front matter, authors, and the {include} directives that order the chapters.
• IrisTutorial/*.lean — one file per chapter, aggregated by IrisTutorial.lean.
• BookGen/, BookGenMain.lean — book-generation infrastructure inherited from the Verso textbook template (the textbook executable and the custom savedLean / savedImport / savedComment code-block elaborators that make a block both type-checked inline and extracted to a file).

The Lean port is released under the MIT License, matching the upstream tutorial. It derives from the Iris Tutorial originally written by Lars Birkedal, Simon Gregersen, Mathias Adam Møller, Mathias Pedersen, and Amin Timany (Aarhus University). Lean port by Zongyuan Liu.

The files under BookGen/ and BookGenMain.lean are inherited from the Verso textbook template and remain under their original copyright (Lean FRO LLC, Apache 2.0).