使引用本书其他章节的超链接能正常跳转到对应小节

.github/workflows/ci.yml

@@ -51,7 +51,7 @@ jobs:
     - name: Setup mdBook
       uses: peaceiris/actions-mdbook@v1
       with:
-        mdbook-version: '0.4.17'
+        mdbook-version: '0.4.30'
 
     - name: Install mdbook-wordcount
       uses: baptiste0928/cargo-install@v1

functional-programming-lean/scripts/sync-title-id.py

@@ -0,0 +1,113 @@
+#!/usr/bin/env python3
+import sys
+import re
+from pathlib import Path
+from typing import Optional
+
+title_regex = re.compile(r"([^#]*)(#+) +(.*[^} ]) *(?:\{ *#([^} ]+) *\})? *")
+
+
+class Title:
+    def __init__(self, title: str, id: str, level: int, prefix: str):
+        self.title: str = title
+        self.id: str = id
+        self.level: int = level
+        self.prefix: str = prefix
+
+    @classmethod
+    def from_line(cls, line: str) -> "Title":
+        title_match = title_regex.fullmatch(line)
+        assert title_match is not None, "Unsupported title format: " + line
+        prefix, sharps, title, id = title_match.groups()
+        return cls(
+            title=title,
+            id=id or cls.title_to_default_id(title),
+            level=len(sharps),
+            prefix=prefix,
+        )
+
+    def to_line(self) -> str:
+        return f"{self.prefix}{'#'*self.level} {self.title} {{ #{self.id} }}"
+
+    def __repr__(self) -> str:
+        return f"Title(title = {self.title}, id = {self.id}, level = {self.level})"
+
+    @staticmethod
+    def title_to_default_id(title: str):
+        # https://github.com/rust-lang/mdBook/blob/94e0a44e152d8d7c62620e83e0632160977b1dd5/src/utils/mod.rs#L30-L43
+        return "".join(
+            "-" if c.isspace() else c
+            for c in title.lower()
+            if c.isalpha() or c.isspace() or c in ("_", "-")
+        )
+
+    @staticmethod
+    def is_title(title: str) -> bool:
+        if title.startswith("/- "):
+            title = title[len("/- ") :]
+        return title.startswith("#") and title.lstrip("#").startswith(" ")
+
+
+def sync_md_id(src_file: Path, dest_file: Path):
+    print(f"from {src_file} to {dest_file}:")
+    src_titles_reverse = [
+        Title.from_line(line.rstrip("\n"))
+        for line in open(src_file).readlines()[::-1]
+        if Title.is_title(line)
+    ]
+
+    dest_lines = [line.rstrip("\n") for line in open(dest_file).readlines()]
+    in_comment = False
+    for n in range(len(dest_lines)):
+        line = dest_lines[n]
+        if line.strip().startswith("<!--"):
+            in_comment = True
+            continue
+        if line.strip().startswith("-->"):
+            in_comment = False
+            continue
+        if in_comment:
+            continue
+        if not Title.is_title(line):
+            continue
+        title = Title.from_line(line)
+        assert (
+            len(src_titles_reverse) != 0
+        ), f"There are more titles in the destination, one of which is {title}"
+        src_title = src_titles_reverse.pop()
+        title.id = src_title.id
+        assert (
+            title.level == src_title.level
+        ), f"Titles from source and destination have different level: {src_title} {title}"
+        print(src_title, "->", title)
+        dest_lines[n] = title.to_line()
+
+    open(dest_file, "w").write("\n".join(dest_lines))
+
+    assert (
+        len(src_titles_reverse) == 0
+    ), f"There are more titles in the source, which are {src_titles_reverse[::-1]}"
+    print()
+
+
+def main(src: Path, dest: Path, suffix: Optional[str]):
+    if not src.is_dir():
+        sync_md_id(src, dest)
+        return
+    assert suffix is not None
+    for filename in Path(src).rglob("*." + suffix):
+        sync_md_id(filename, dest / filename.relative_to(src))
+
+
+if __name__ == "__main__":
+    if len(sys.argv) < 3:
+        usage = f"""Usage: {sys.argv[0]} upstream_directory translation_directory name_suffix
+   or: {sys.argv[0]} upstream_file translation_file
+Synchronize title IDs from upstream to translation, to make fragment identifier in urls work.
+
+Example: {sys.argv[0]} ./upstream/lean/ ./lean/ lean"""
+        print(usage, file=sys.stderr)
+        exit(1)
+    main(
+        Path(sys.argv[1]), Path(sys.argv[2]), None if len(sys.argv) < 4 else sys.argv[3]
+    )

functional-programming-lean/src/SUMMARY.md

@@ -1,4 +1,4 @@
-# Lean 函数式编程
+# Lean 函数式编程 { #functional-programming-in-lean }
 
 [Lean 函数式编程](./title.md)
 [引言](./introduction.md)
@@ -70,4 +70,4 @@
   - [特殊类型](programs-proofs/special-types.md)
   - [总结](programs-proofs/summary.md)
 
-[下一步](next-steps.md)
+[下一步](next-steps.md)

functional-programming-lean/src/acknowledgments.md

@@ -2,7 +2,7 @@
 # Acknowledgments
 -->
 
-# 鸣谢
+# 鸣谢 { #acknowledgments }
 
 <!--
 This free online book was made possible by the generous support of Microsoft Research, who paid for it to be written and given away.
@@ -43,4 +43,4 @@ Evgenia Karunus、eyelash、Floris van Doorn、František Silváši、Henrik Bö
 Ian Young、Jeremy Salwen、Jireh Loreaux、Kevin Buzzard、Lars Ericson、Liu Yuxi、
 Mac Malone、Malcolm Langfield、Mario Carneiro、Newell Jensen、Patrick Massot、
 Paul Chisholm、Pietro Monticone、Tomas Puverle、Yaël Dillies、Zhiyuan Bao
-和 Zyad Hassan 提出的许多建议，包括风格和技术方面的建议。
+和 Zyad Hassan 提出的许多建议，包括风格和技术方面的建议。

functional-programming-lean/src/dependent-types.md

@@ -2,7 +2,7 @@
 # Programming with Dependent Types
 -->
 
-# 使用依值类型编程
+# 使用依值类型编程 { #programming-with-dependent-types }
 
 <!-- 
 In most statically-typed programming languages, there is a hermetic seal between the world of types and the world of programs.
@@ -76,4 +76,4 @@ While this chapter scratches the surface of dependently typed programming, it is
 然而，使用依值类型进行编程是一个非常复杂的问题，需要一些一般函数式编程中不会用到的技能。
 依值类型编程中很可能出现“设计了一个复杂类型以表达一个非常细致的规范，但是无法写出满足这个类型的程序”之类的问题。
 当然，这些问题也经常会引发对问题的新的理解，从而得到一个更加细化且可以被满足的类型。
-虽然本章只是简单介绍使用依值类型编程，但它是一个值得花一整本书专门讨论的深刻主题。
+虽然本章只是简单介绍使用依值类型编程，但它是一个值得花一整本书专门讨论的深刻主题。

functional-programming-lean/src/dependent-types/indexed-families.md

@@ -2,7 +2,7 @@
 # Indexed Families
 -->
 
-# 索引族
+# 索引族 { #indexed-families }
 
 <!--
 Polymorphic inductive types take type arguments.
@@ -344,7 +344,7 @@ The refinement of the length can be observed by making `n` into an explicit argu
 ## Exercises
 -->
 
-## 练习
+## 练习 { #exercises }
 
 <!--
 Getting a feel for programming with dependent types requires experience, and the exercises in this section are very important.
@@ -408,4 +408,4 @@ This is also a good way to develop a feel for the error messages.
  * Define a function `Vect.take` with type `(n : Nat) → Vect α (k + n) → Vect α n` that returns the first `n` entries in the `Vect`. Check that it works on an example.
  -->
 
- * 定义一个函数 `Vect.take`。它的类型为 `(n : Nat) → Vect α (k + n) → Vect α n`。它返回 `Vect` 中的前 `n` 个条目。检查它在一个例子上的结果。 
+ * 定义一个函数 `Vect.take`。它的类型为 `(n : Nat) → Vect α (k + n) → Vect α n`。它返回 `Vect` 中的前 `n` 个条目。检查它在一个例子上的结果。 

functional-programming-lean/src/dependent-types/indices-parameters-universes.md

@@ -1,7 +1,7 @@
 <!--
 # Indices, Parameters, and Universe Levels
 -->
-# 索引、参量和宇宙层级
+# 索引、参量和宇宙层级 { #indices-parameters-and-universe-levels }
 
 <!--
 The distinction between indices and parameters of an inductive type is more than just a way to describe arguments to the type that either vary or do not between the constructors.

functional-programming-lean/src/dependent-types/pitfalls.md

@@ -2,7 +2,7 @@
 # Pitfalls of Programming with Dependent Types
 -->
 
-# 使用依值类型编程的陷阱
+# 使用依值类型编程的陷阱 { #pitfalls-of-programming-with-dependent-types }
 
 <!--
 The flexibility of dependent types allows more useful programs to be accepted by a type checker, because the language of types is expressive enough to describe variations that less-expressive type systems cannot.
@@ -104,7 +104,7 @@ Here, `n✝` represents the `Nat` that is one less than the argument `n`.
 ## Definitional Equality
 -->
 
-## 定义相等性
+## 定义相等性 { #definitional-equality }
 
 <!--
 In the definition of `plusL`, there is a pattern case `0, k => k`.
@@ -328,7 +328,7 @@ In particular, the fact that `plusL` is used in the type of `appendL` means that
 ## Getting Stuck on Addition
 -->
 
-## 在加法上卡住
+## 在加法上卡住 { #getting-stuck-on-addition }
 
 <!--
 What happens if append is defined with `plusR` instead?
@@ -403,7 +403,7 @@ Getting it unstuck requires [propositional equality](../type-classes/standard-cl
 ## Propositional Equality
 -->
 
-## 命题相等性
+## 命题相等性 { #propositional-equality }
 
 <!--
 Propositional equality is the mathematical statement that two expressions are equal.
@@ -630,7 +630,7 @@ However, Lean's type checker has enough information to fill them in automaticall
 ## Pros and Cons
 -->
 
-## 优势和劣势
+## 优势和劣势 { #pros-and-cons }
 
 <!--
 Indexed families have an important property: pattern matching on them affects definitional equality.
@@ -702,7 +702,7 @@ Fluency in their use is an important part of knowing when to use them.
 ## Exercises
 -->
 
-## 练习
+## 练习 { #exercises }
 
  <!--
  * Using a recursive function in the style of `plusR_succ_left`, prove that for all `Nat`s `n` and `k`, `n.plusR k = n + k`.
@@ -714,5 +714,4 @@ Fluency in their use is an important part of knowing when to use them.
  * Write a function on `Vect` for which `plusR` is more natural than `plusL`, where `plusL` would require proofs to be used in the definition.
  -->
 
- * 写一个在 `Vect` 上的函数，其中 `plusR` 比 `plusL` 更自然：`plusL` 需要在定义中显示使用（命题相等性的）证明。
-
+ * 写一个在 `Vect` 上的函数，其中 `plusR` 比 `plusL` 更自然：`plusL` 需要在定义中显示使用（命题相等性的）证明。

functional-programming-lean/src/dependent-types/summary.md

@@ -2,13 +2,13 @@
 # Summary
 -->
 
-# 总结
+# 总结 { #summary }
 
 <!--
 ## Dependent Types
 -->
 
-## 依值类型
+## 依值类型 { #dependent-types }
 
 <!--
 Dependent types, where types contain non-type code such as function calls and ordinary data constructors, lead to a massive increase in the expressive power of a type system.
@@ -52,7 +52,7 @@ Type-level computation can be seen as a kind of partial evaluation, where only t
 ## The Universe Pattern
 -->
 
-# 宇宙设计模式
+## 宇宙设计模式 { #the-universe-pattern }
 
 <!--
 A common pattern when working with dependent types is to section off some subset of the type system.
@@ -87,7 +87,7 @@ Defining a custom universe has a number of advantages over using the types direc
 ## Indexed Families
 -->
 
-## 索引族
+## 索引族 { #indexed-families }
 
 <!--
 Datatypes can take two separate kinds of arguments: _parameters_ are identical in each constructor of the datatype, while _indices_ may vary between constructors.
@@ -137,7 +137,7 @@ Avoiding these slowdowns for complicated programs can require specialized techni
 ## Definitional and Propositional Equality
 -->
 
-## 定义相等性和命题相等性
+## 定义相等性和命题相等性 { #definitional-and-propositional-equality }
 
 <!--
 Lean's type checker must, from time to time, check whether two types should be considered interchangeable.
@@ -186,4 +186,4 @@ When propositional equality is instead used to prove that a program meets a spec
 或者使用其他的技术来保证程序不变性。<!-- TODO: enforce -->
 当命题相等被用来证明程序满足规范，
 或作为子类型的一部分时，
-则是一种常见的模式。
+则是一种常见的模式。