deprecate mdgen, try mdbook

Author: subfish-zhou

.github/workflows/book.yml

@@ -1,10 +1,15 @@
-name: Deploy to github pages
+# Sample workflow for building and deploying a mdBook site to GitHub Pages
+#
+# To get started with mdBook see: https://rust-lang.github.io/mdBook/index.html
+#
+name: Deploy mdBook site to Pages
 
 on:
-  pull_request:
+  # Runs on pushes targeting the default branch
   push:
-    branches:
-      - master
+    branches: ["master"]
+
+  # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
@@ -20,35 +25,30 @@ concurrency:
   cancel-in-progress: false
 
 jobs:
+  # Build job
   build:
     runs-on: ubuntu-latest
+    env:
+      MDBOOK_VERSION: 0.4.36
     steps:
-      - name: checkout
-        uses: actions/checkout@v4
-
-      - name: install elan
+      - uses: actions/checkout@v4
+      - name: Install mdBook
         run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: build markdown files by mdgen
-        run: lake run mdbuild
-
-      - name: setup mdBook
-        uses: peaceiris/actions-mdbook@v1
-        with:
-          mdbook-version: '0.4.35'
-
-      - name: build html from markdown
+          curl --proto '=https' --tlsv1.2 https://sh.rustup.rs -sSf -y | sh
+          rustup update
+          cargo install --version ${MDBOOK_VERSION} mdbook
+      - name: Setup Pages
+        id: pages
+        uses: actions/configure-pages@v4
+      - name: Build with mdBook
         run: mdbook build
-
-      - name: upload artifact
+      - name: Upload artifact
         uses: actions/upload-pages-artifact@v3
         with:
           path: ./book
 
+  # Deployment job
   deploy:
-    if: github.ref == 'refs/heads/master'
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
@@ -57,4 +57,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v4
+        uses: actions/deploy-pages@v4

.github/workflows/ci.yml

@@ -2,9 +2,9 @@
 
 这是一本关于 Lean 4 内核和实现外部类型检查器的书；它是用 mdBook 构建的。
 
-原作者：[Chris Bailey](https://github.com/ammkrn) 原文地址：[https://ammkrn.github.io/type_checking_in_lean4/](https://ammkrn.github.io/type_checking_in_lean4/)
+原作者：[Christopher A. Bailey](https://github.com/ammkrn) 原文地址：[https://ammkrn.github.io/type_checking_in_lean4/](https://ammkrn.github.io/type_checking_in_lean4/)
 
-译者：[subfish_zhou](https://github.com/subfish-zhou)
+译者：[subfish_zhou](https://github.com/subfish-zhou) 译本地址：[http://www.leanprover.cn/type-checking-in-lean-zh/](http://www.leanprover.cn/type-checking-in-lean-zh/)
 
 ## 贡献
 

.github/workflows/deploy.yml .github/workflows/mdbook.yml.github/workflows/deploy.yml renamed to .github/workflows/mdbook.yml

@@ -6,7 +6,7 @@ src = "src"
 title = "Lean 4 类型检查"
 
 [output.html]
-git-repository-url = "https://github.com/Lean-zh/type_checking"
+git-repository-url = "https://github.com/Lean-zh/type-checking-in-lean-zh"
 additional-css = ["./assets/pagetoc.css"]
 additional-js = [
   "assets/blockPlay.js",
@@ -15,7 +15,7 @@ additional-js = [
 ]
 
 # Settings to overwrite the edit button and make it a code execution button.
-# edit-url-template = "https://raw.githubusercontent.com/Lean-zh/type_checking/master/{path}"
+# edit-url-template = "https://raw.githubusercontent.com/Lean-zh/type-checking-in-lean-zh/master/{path}"
 
 # To ensure that the 404 page functions properly.
-# site-url = "https://github.com/Lean-zh/type_checking"
+# site-url = "https://github.com/Lean-zh/type-checking-in-lean-zh"

README.md

@@ -1,3 +1,3 @@
-# Type Checking in Lean 4
+# Lean 4 类型检查
 
-This document exists to help readers better understand Lean's kernel, clarify the trust assumptions involved in using Lean, and serve as a resource for those who wish to write their own external type checkers for Lean's kernel language.
+本文档旨在帮助读者更好地理解 Lean 的内核，解释使用 Lean 所涉及的信任假设，并为希望为 Lean 内核语言编写自己的外部类型检查器的读者提供资源。