Merge pull request #178 from rzk-lang/tiny-docs-fixes-2024-04-04

Small docs fixes/improvement
rzk-lang · Apr 4, 2024 · 1450c1c · 1450c1c
2 parents d522791 + 0aae3bf
commit 1450c1c
Show file tree

Hide file tree

Showing 3 changed files with 41 additions and 31 deletions.
diff --git a/docs/docs/en/related.md b/docs/docs/en/related.md
@@ -39,13 +39,13 @@ Aya is implemented in Java.
 
     I do not know of existing formalization libraries in Aya.
 
-## The <b><span style="color: red">red</span>*</b> family
+## The <b><span style="color: red">red</span>\*</b> family
 
 [<b><span style="color: #135cb7;">cool</span>tt</b>](https://github.com/redprl/cooltt), [<b><span style="color: red">red</span>tt</b>](https://github.com/redprl/redtt), and [<b><span style="color: red">Red</span>PRL</b>](https://redprl.readthedocs.io/en/latest/) are a family of experimental proof assistants developed by the [<b><span style="color: red">Red</span>PRL</b> Development Team](https://redprl.org).
 
 There is a [<b><span style="color: red">red</span>tt</b> mathematical library](https://github.com/RedPRL/redtt/tree/master/library)
 
-The <b><span style="color: red">red</span>*</b> family of proof assistants is implemented in OCaml.
+The <b><span style="color: red">red</span>\*</b> family of proof assistants is implemented in OCaml.
 The developers also have a related [<b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b> project](https://redprl.org/#algae),
 which aims to provide composable (OCaml) libraries that facilitate the construction of a usable proof assistant from a core type checker.
 
@@ -60,6 +60,7 @@ Other notable formalizations of HoTT in Coq include [Coq-HoTT](https://github.co
 Coq is implemented in OCaml.
 
 ## Cubical Agda
+
 [Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) is a mode extending Agda with a variety of features from Cubical Type Theory[^1] [^2].
 
 Although technical a mode within Agda, it is probably best seen as a separate language.
@@ -89,7 +90,11 @@ Hence, a formalization of [HoTT in Lean 2](https://github.com/leanprover/lean2/t
 However, since Lean 2 is not supported anymore, the formalization is also unmantained.
 
 Lean 3 and 4 has dropped the mode that allowed (direct) HoTT formalization.
-There is, however, an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3).
+However, the [Ground Zero](https://github.com/forked-from-1kasper/ground_zero) project
+attempts to formalize HoTT in Lean 4. The project makes use of the [large elimination checker](https://github.com/forked-from-1kasper/ground_zero/blob/d8c41ea2910d81d3c1bf6c2762663473368016ab/GroundZero/Meta/HottTheory.lean),
+ported from an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3),
+which enables HoTT and non-HoTT scopes to coexist consistently (as the project authors believe).
+In particular, attempting to show UIP results in a type error under HoTT scope in the Ground Zero project.
 
 Lean 2 and 3 are implemented in C++.
 Lean 4 is implemented in itself (and a bit of C++)!
@@ -102,22 +107,19 @@ Lean 4 is implemented in itself (and a bit of C++)!
     <https://doi.org/10.4230/LIPIcs.TYPES.2015.5>
 
 [^2]:
-    Thierry Coquand, Simon Huber, and Anders Mörtberg.
-    2018. _On Higher Inductive Types in Cubical Type Theory_.
+    Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. _On Higher Inductive Types in Cubical Type Theory_.
     In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
     Association for Computing Machinery, New York, NY, USA, 255–264.
     <https://doi.org/10.1145/3209108.3209197>
 
 [^3]:
-    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
-    2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
+    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
     In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017).
     Association for Computing Machinery, New York, NY, USA, 164–172.
     <https://doi.org/10.1145/3018610.3018615>
 
 [^4]:
-    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz.
-    2017. _Homotopy Type Theory in Lean_.
+    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. _Homotopy Type Theory in Lean_.
     In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017.
     Lecture Notes in Computer Science(), vol 10499. Springer, Cham.
     <https://doi.org/10.1007/978-3-319-66107-0_30>
diff --git a/docs/docs/ru/related.md b/docs/docs/ru/related.md
@@ -44,7 +44,7 @@ Aya реализована на Java.
 
     Мне неизвестны библиотеки формализации на Aya.
 
-## Семейство <b><span style="color: red">red</span>*</b>
+## Семейство <b><span style="color: red">red</span>\*</b>
 
 [<b><span style="color: #135cb7;">cool</span>tt</b>](https://github.com/redprl/cooltt),
 [<b><span style="color: red">red</span>tt</b>](https://github.com/redprl/redtt),
@@ -54,8 +54,8 @@ Aya реализована на Java.
 
 Существует формализация [математической библиотеки <b><span style="color: red">red</span>tt</b>](https://github.com/RedPRL/redtt/tree/master/library)
 
-Семейство решателей <b><span style="color: red">red</span>*</b> реализовано на языке программирования OCaml.
-Создатели семества решателей также работают над  [проектом <b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b>](https://redprl.org/#algae),
+Семейство решателей <b><span style="color: red">red</span>\*</b> реализовано на языке программирования OCaml.
+Создатели семества решателей также работают над [проектом <b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b>](https://redprl.org/#algae),
 который нацелен на реализацию ряда удобных библиотек (для OCaml) для помощи в реализации
 решателей теорем на основе проверки типов для ядра решателя.
 
@@ -70,6 +70,7 @@ Coq — это зрелый решатель теорем, основанный
 Coq реализован на OCaml.
 
 ## Cubical Agda
+
 [Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) (кубическая Агда)
 — это расширение Agda набором возможностей кубической теории типов[^1] [^2].
 
@@ -102,7 +103,12 @@ Lean 2, как и Agda, поддерживал режим без уникаль
 Однако, Lean 2 больше не поддерживается и формализация, соответственно, тоже.
 
 Lean 3 и 4 убрали режим, допускающий (прямую) формализацию гомотопической теории типов.
-Однако, существует ныне неподдерживаемый [проект по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3).
+Несмотря на это проект [Ground Zero](https://github.com/forked-from-1kasper/ground_zero)
+продолжает формализацию HoTT на Lean 4. Проект использует [проверку элиминации](https://github.com/forked-from-1kasper/ground_zero/blob/d8c41ea2910d81d3c1bf6c2762663473368016ab/GroundZero/Meta/HottTheory.lean),
+портированную из неподдерживаемого [проекта по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3).
+Эта проверка позволяет поддерживать окружение HoTT, совместимое со стандартным окружением Lean (по крайней мере по убеждениям авторов проекта).
+В частности, попытка (напрямую) доказать принцип неразличимости доказательств равенства (Uniqueness of Identity Proofs)
+приводит к ошибки типизации в рамках проекта Ground Zero.
 
 Lean 2 и 3 реализованы на C++.
 Lean 4 реализован в основном на самом себе (и немного на C++)!
@@ -115,22 +121,19 @@ Lean 4 реализован в основном на самом себе (и н
     <https://doi.org/10.4230/LIPIcs.TYPES.2015.5>
 
 [^2]:
-    Thierry Coquand, Simon Huber, and Anders Mörtberg.
-    2018. _On Higher Inductive Types in Cubical Type Theory_.
+    Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. _On Higher Inductive Types in Cubical Type Theory_.
     In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
     Association for Computing Machinery, New York, NY, USA, 255–264.
     <https://doi.org/10.1145/3209108.3209197>
 
 [^3]:
-    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
-    2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
+    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
     In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017).
     Association for Computing Machinery, New York, NY, USA, 164–172.
     <https://doi.org/10.1145/3018610.3018615>
 
 [^4]:
-    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz.
-    2017. _Homotopy Type Theory in Lean_.
+    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. _Homotopy Type Theory in Lean_.
     In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017.
     Lecture Notes in Computer Science(), vol 10499. Springer, Cham.
     <https://doi.org/10.1007/978-3-319-66107-0_30>
diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md
@@ -9,6 +9,7 @@ and this project adheres to the
 ## v0.7.4 — 2024-04-01
 
 Fixes:
+
 - Fix caching in Rzk Language Server, especially in presence of errors (see [#167](https://github.com/rzk-lang/rzk/pull/167))
 - Fix CI for the Rzk Playground (see [#174](https://github.com/rzk-lang/rzk/pull/174))
 
@@ -18,33 +19,37 @@ and a typo fix (see [#171](https://github.com/rzk-lang/rzk/pull/171)).
 ## v0.7.3 — 2023-12-16
 
 Fixes:
+
 - Fix overlapping edits in the formatter, hopefully making it idempotent (see [#160](https://github.com/rzk-lang/rzk/pull/160));
 - Fix formatter crashing the language server (see [#161](https://github.com/rzk-lang/rzk/pull/161));
 - Avoid unnecessary typechecking when semantics of a file has not changed (see [#159](https://github.com/rzk-lang/rzk/pull/159));
 - Stop typechecking after the first parse error (avoid invalid cache) (see [`68ab0b4`](https://github.com/rzk-lang/rzk/commit/68ab0b4dd3d627756e10adb55cb16845b08d09d9));
 
 Other:
+
 - Add unit tests for the formatter (see [#157](https://github.com/rzk-lang/rzk/pull/157));
 
 ## v0.7.2 — 2023-12-12
 
 Fixes:
+
 - Fixes for `rzk format`:
-    - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));
-    - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));
+  - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));
+  - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));
 - Throw an error when `rzk.yaml`'s `include` is empty (see [#154](https://github.com/rzk-lang/rzk/pull/154));
 
 Changes to the Rzk website:
-  - Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));
-      - English is the default;
-      - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;
-  - Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));
-      - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;
-  - Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));
-  - Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))
-  - Add (default) social cards
-  - Integrate ToC on the left
-  - Use Inria Sans for English, PT Sans for Russian
+
+- Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));
+  - English is the default;
+  - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;
+- Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));
+  - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;
+- Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));
+- Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))
+- Add (default) social cards
+- Integrate ToC on the left
+- Use Inria Sans for English, PT Sans for Russian
 
 ## v0.7.1 — 2023-12-08