Init

Author: lzy0505

.github/workflows/deploy.yml

@@ -0,0 +1,71 @@
+name: Build and Deploy Book
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+# Allow the deploy job to publish to GitHub Pages.
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+# Allow only one concurrent deployment; let in-progress runs finish.
+concurrency:
+  group: pages
+  cancel-in-progress: false
+
+jobs:
+  build:
+    name: Build book
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      # Installs the toolchain pinned in `lean-toolchain`, runs `lake build`
+      # (elaborating every chapter / type-checking all proofs), and caches
+      # `.lake` so the verso and iris-lean dependency builds are reused.
+      - name: Build and check proofs
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+
+      # `lake build` above already compiled everything; this runs the
+      # `textbook` executable to render the HTML book and extract the
+      # example code into `_out/`.
+      - name: Render book and extract example code
+        run: lake exe textbook
+
+      - name: Assemble site (html + code.zip)
+        run: |
+          rm -rf _site
+          mkdir -p _site
+          cp -r _out/html-multi/. _site/
+          (cd _out && zip -r "$GITHUB_WORKSPACE/_site/code.zip" example-code)
+
+      # On PRs the full build above already runs, catching breakage early.
+      # Only upload the Pages artifact for push/manual runs that will deploy
+      # (this also avoids restricted-permission warnings on PRs from forks).
+      - name: Upload Pages artifact
+        if: github.event_name != 'pull_request'
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: _site
+
+  deploy:
+    name: Deploy to GitHub Pages
+    needs: build
+    runs-on: ubuntu-latest
+    # Publish only for pushes to main and manual runs — never for PRs.
+    if: github.event_name != 'pull_request'
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - name: Deploy
+        id: deployment
+        uses: actions/deploy-pages@v4

.gitignore

@@ -0,0 +1,6 @@
+# Lean / Lake build artifacts
+.lake
+
+# Book build outputs
+_out
+out

TextbookTemplate/Meta/Lean.lean BookGen/Meta/Lean.leanTextbookTemplate/Meta/Lean.lean renamed to BookGen/Meta/Lean.lean

@@ -11,7 +11,7 @@ open Verso.Doc Elab
 open Verso.ArgParse
 open Lean
 
-namespace TextbookTemplate
+namespace BookGen
 
 block_extension Block.savedLean (file : String) (source : String) where
   data := .arr #[.str file, .str source]

TextbookTemplateMain.lean BookGenMain.leanTextbookTemplateMain.lean renamed to BookGenMain.lean

@@ -1,19 +1,19 @@
 /-
 Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: David Thrane Christiansen
+Author: David Thrane Christiansen, Zongyuan Liu
 -/
 
 import Std.Data.HashMap
 import VersoManual
-import TextbookTemplate
+import IrisTutorialBook
 
 open Verso Doc
 open Verso.Genre Manual
 
 open Std (HashMap)
 
-open TextbookTemplate
+open BookGen
 
 
 -- Computes the path of this very `main`, to ensure that examples get names relative to it
@@ -31,7 +31,7 @@ partial def buildExercises (mode : Mode) (logError : String → IO Unit) (cfg :
   let code := (← part text |>.run {}).snd
   let dest := cfg.destination / "example-code"
   let some mainDir := mainFileName.parent
-    | throw <| IO.userError "Can't find directory of `TextbookTemplateMain.lean`"
+    | throw <| IO.userError "Can't find directory of `BookGenMain.lean`"
 
   IO.FS.createDirAll <| dest
   for ⟨fn, f⟩ in code do
@@ -86,4 +86,4 @@ def config : RenderConfig where
   emitHtmlMulti := .immediately
   htmlDepth := 2
 
-def main := manualMain (%doc TextbookTemplate) (extraSteps := [buildExercises]) (config := config)
+def main := manualMain (%doc IrisTutorialBook) (extraSteps := [buildExercises]) (config := config)

IrisTutorial.lean

@@ -0,0 +1,21 @@
+import IrisTutorial.Basics
+import IrisTutorial.Pure
+import IrisTutorial.Lang
+import IrisTutorial.Specifications
+import IrisTutorial.Persistently
+import IrisTutorial.LinkedLists
+import IrisTutorial.Later
+import IrisTutorial.Arrays
+import IrisTutorial.GrPredicates
+import IrisTutorial.ResourceAlgebra
+import IrisTutorial.Invariants
+import IrisTutorial.Timeless
+import IrisTutorial.StructuredConc
+import IrisTutorial.Counter
+import IrisTutorial.SpinLock
+import IrisTutorial.TicketLock
+import IrisTutorial.TicketLockAdvanced
+import IrisTutorial.Adequacy
+import IrisTutorial.MergeSort
+import IrisTutorial.CustomRa
+import IrisTutorial.Ofe

IrisTutorial/Adequacy.lean

@@ -0,0 +1,13 @@
+import VersoManual
+import BookGen.Meta.Lean
+
+open Verso.Genre Manual
+open Verso.Genre.Manual.InlineLean
+open BookGen
+
+set_option pp.rawOnError true
+
+#doc (Manual) "Adequacy" =>
+
+This chapter has not yet been ported. The Rocq source is
+`iris-tutorial/theories/adequacy.v`.

IrisTutorial/Arrays.lean

@@ -0,0 +1,13 @@
+import VersoManual
+import BookGen.Meta.Lean
+
+open Verso.Genre Manual
+open Verso.Genre.Manual.InlineLean
+open BookGen
+
+set_option pp.rawOnError true
+
+#doc (Manual) "Arrays in HeapLang" =>
+
+This chapter has not yet been ported. The Rocq source is
+`iris-tutorial/theories/arrays.v`.