Merge branch 'release-v0.7.5'

* release-v0.7.5: Bump version and update changelog Support newer lsp Switch to macos-12 (since macos-latest does not have Stack yet) Update all actions Made naming consistent for Sigma Tuples Added tuple patterns Support tuple patterns (desugared to left-associative nested pairs) Added lsp tokenization Added ASCII and Unicode rules Corrected overlapping rule Implemented syntactic sugar for nested sigma types Bump nixpkgs version Improve error reporting for unused variables Mention Ground Zero project (HoTT formalization in Lean 4) Fix Markdown formatting in the changelog Correct location for parse error diagnostics
rzk-lang · Aug 18, 2024 · 25dd17a · 25dd17a
2 parents 0ac6736 + 566a6e9
commit 25dd17a
Show file tree

Hide file tree

Showing 25 changed files with 317 additions and 123 deletions.
diff --git a/.github/workflows/ghc.yml b/.github/workflows/ghc.yml
@@ -36,14 +36,14 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-latest]
+        os: [ubuntu-latest, windows-latest, macos-12]
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
 
       - name: Tar and strip the binary
         run: |
@@ -53,7 +53,7 @@ jobs:
         shell: bash
 
       - name: Upload rzk binary as Artifact
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           path: rzk-bin.tar.gz
           name: rzk-${{ runner.os }}-${{ runner.arch }}.tar.gz
@@ -67,10 +67,10 @@ jobs:
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
 
       - name: 🔨 Build Haddock Documentation (with Stack)
         run: |
@@ -93,11 +93,11 @@ jobs:
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 📥 Download rzk
         id: download
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: rzk-${{ runner.os }}-${{ runner.arch }}.tar.gz
 

diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
@@ -35,7 +35,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: ❄️ Install Nix
-        uses: nixbuild/nix-quick-install-action@v25
+        uses: nixbuild/nix-quick-install-action@v27
         with:
           nix_conf: |
             substituters = https://cache.nixos.org/ https://cache.iog.io https://nix-community.cachix.org https://miso-haskell.cachix.org

diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml
@@ -2,7 +2,7 @@ name: MKDocs
 
 on:
   push:
-    branches: [develop,mkdocs-*]
+    branches: [develop, mkdocs-*]
     tags: [v*]
     paths:
       - .github/workflows/mkdocs.yml
@@ -19,12 +19,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 
       - name: 🧰 Set up Python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: "3.9"
           cache: "pip" # caching pip dependencies
@@ -38,15 +38,13 @@ jobs:
           chmod: 0755
 
       - name: Check Rzk files for each language
-        run:
-          for lang_dir in $(ls -d docs/docs/*/); do
-            pushd ${lang_dir} && rzk typecheck; popd ;
+        run: for lang_dir in $(ls -d docs/docs/*/); do
+          pushd ${lang_dir} && rzk typecheck; popd ;
           done
 
       - name: Check Rzk formatting for each language
-        run:
-          for lang_dir in $(ls -d docs/docs/*/); do
-            pushd ${lang_dir} && rzk format --check; popd ;
+        run: for lang_dir in $(ls -d docs/docs/*/); do
+          pushd ${lang_dir} && rzk format --check; popd ;
           done
 
       - name: 🔨 Install MkDocs Material and mike

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -12,10 +12,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
         with:
           fast: false
 
@@ -37,10 +37,10 @@ jobs:
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
         with:
           fast: false
 

diff --git a/CITATION.cff b/CITATION.cff
@@ -8,5 +8,5 @@ authors:
   - family-names: Danko
     given-names: Danila
 title: "Rzk: a  proof assistant for synthetic $\\infty$-categories"
-version: 0.7.4
+version: 0.7.5
 url: "https://github.com/rzk-lang/rzk"
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/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -1,9 +1,9 @@
 {
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
-    nixpkgs.url = "github:NixOS/nixpkgs/d1c3a8112f9d5d4840e0669727222e5fd9243451";
+    nixpkgs.url = "github:NixOS/nixpkgs/2436aaf8fad634ee66a6280fb82a19c1771c173f";
     miso = {
-      url = "github:dmjio/miso/49edf0677253bbcdd473422b5dd5b4beffd83910";
+      url = "github:dmjio/miso/8277ac79941825abaf50b917e074e3df7ef6d213";
       flake = false;
     };
     flake-compat = {
@@ -22,7 +22,7 @@
 
       rzk = "rzk";
       rzk-js = "rzk-js";
-      ghcVersion = "ghc962";
+      ghcVersion = "ghc963";
       rzk-src = (inputs.nix-filter {
         root = ./${rzk};
         include = [ "app" "src" "test" "package.yaml" ];