Merge branch 'release-v0.7.3'

* release-v0.7.3:
  Bump version and update changelog
  Stop typechecking after a parse error in some file (avoid invalid cache)
  Fix warning
  Make formatFile strict
  Clean up formatting code
  Check Rzk formatting for all languages before rendering MkDocs
  Apply autoformatting to docs
  Make safer resolveLayout, use that in the formatter, drop deepseq dependency
  Convert `formatTextEdits` to IO to catch errors
  Add DeepSeq package to dependencies
  Add a couple of logs for errors while typechecking
  Split the space edits around bin ops into 2 to avoid overlapping with possible unicode edits
  Skip typechecking when the decls have not changed
  Add some tests for the formatter
  Install HSpec and configure HSpec-Discover
  Unignore the tests directory

Author: fizruk

.github/workflows/mkdocs.yml

@@ -43,6 +43,12 @@ jobs:
             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 ;
+          done
+
       - name: 🔨 Install MkDocs Material and mike
         run: pip install -r docs/requirements.txt
 

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.2
+version: 0.7.3
 url: "https://github.com/rzk-lang/rzk"

docs/docs/en/examples/recId.rzk.md

@@ -19,33 +19,33 @@ We begin by introducing common HoTT definitions:
 -- A is contractible there exists x : A such that for any y : A we have x = y.
 #define iscontr (A : U)
   : U
-  := Σ ( a : A) , (x : A) → a =_{A} x
+  := Σ (a : A) , (x : A) → a =_{A} x
 
 -- A is a proposition if for any x, y : A we have x = y
 #define isaprop (A : U)
   : U
-  := ( x : A) → (y : A) → x =_{A} y
+  := (x : A) → (y : A) → x =_{A} y
 
 -- A is a set if for any x, y : A the type x =_{A} y is a proposition
 #define isaset (A : U)
   : U
-  := ( x : A) → (y : A) → isaprop (x =_{A} y)
+  := (x : A) → (y : A) → isaprop (x =_{A} y)
 
 -- A function f : A → B is an equivalence
 -- if there exists g : B → A
 -- such that for all x : A we have g (f x) = x
 -- and for all y : B we have f (g y) = y
 #define isweq (A : U) (B : U) (f : A → B)
   : U
-  := Σ ( g : B → A)
+  := Σ (g : B → A)
   , prod
     ( ( x : A) → g (f x) =_{A} x)
     ( ( y : B) → f (g y) =_{B} y)
 
 -- Equivalence of types A and B
 #define weq (A : U) (B : U)
   : U
-  := Σ ( f : A → B)
+  := Σ (f : A → B)
   , isweq A B f
 
 -- Transport along a path
@@ -66,12 +66,12 @@ We can now define relative function extensionality. There are several formulatio
 -- [RS17, Axiom 4.6] Relative function extensionality.
 #define relfunext
   : U
-  := ( I : CUBE)
+  := (I : CUBE)
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
   → ( ( t : ψ) → iscontr (A t))
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( t : ψ) → A t [ φ t ↦ a t]
 
 -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
@@ -82,9 +82,9 @@ We can now define relative function extensionality. There are several formulatio
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( f : (t : ψ) → A t [ φ t ↦ a t ])
-  → ( g : ( t : ψ) → A t [ φ t ↦ a t ])
+  → ( g : (t : ψ) → A t [ φ t ↦ a t ])
   → weq
     ( f = g)
     ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ])
@@ -106,13 +106,13 @@ First, we define how to restrict an extension type to a subshape:
 
 -- Restrict extension type to a subshape.
 #define restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 
 -- Restrict extension type to a subshape.
 #define restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 ```
@@ -122,14 +122,14 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
 ```rzk
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : ψ)
   → A t [ ψ t ∧ φ t ↦ restrict_psi a t ]
   := a  -- type is coerced automatically here
 
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : φ)
   → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
   := a  -- type is coerced automatically here

docs/docs/en/getting-started/dependent-types.rzk.md

@@ -79,7 +79,7 @@ which we will discuss soon. For now, we give definition of product types:
 #define prod
   ( A B : U)
   : U
-  := Σ ( _ : A) , B
+  := Σ (_ : A) , B
 ```
 
 The type `#!rzk prod A B` corresponds to the product type $A \times B$.
@@ -188,7 +188,7 @@ For example, for the product type `#!rzk prod A B`, recursion principle looks li
   ( C : U)
   ( f : A → B → C)
   : prod A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 For the `#!rzk Unit` type, recursion principle is trivial:
@@ -223,7 +223,7 @@ For example, for the product type `#!rzk prod A B`, induction principle looks li
   ( C : prod A B → U)
   ( f : (a : A) → (b : B) → C (a , b))
   : ( z : prod A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 We can use `#!rzk ind-prod` to prove the uniqueness principle for products.
@@ -313,7 +313,7 @@ The first projection can be easily defined in terms of pattern matching:
   ( A : U)
   ( B : A → U)
   : ( Σ ( a : A) , B a) → A
-  := \ ( a , _) → a
+  := \ (a , _) → a
 ```
 
 However, second projection requires some care. For instance, we might try this:
@@ -339,7 +339,7 @@ To access it, we need a dependent function:
   ( A : U)
   ( B : A → U)
   : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
-  := \ ( _ , b) → b
+  := \ (_ , b) → b
 ```
 
 In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types (as in "total spaces"):
@@ -349,7 +349,7 @@ In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types
   ( A : U)
   ( B : A → U)
   : U
-  := Σ ( a : A) , B a
+  := Σ (a : A) , B a
 ```
 
 We can use pattern matching in the function type and this new definition to write
@@ -376,7 +376,7 @@ the recursion principle for product types:
   ( C : U)
   ( f : (a : A) → B a → C)
   : total-type A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 The induction principle is, again, a generalization of the recursion
@@ -389,7 +389,7 @@ principle to dependent types:
   ( C : total-type A B → U)
   ( f : (a : A) → (b : B a) → C (a , b))
   : ( z : total-type A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 As before, using `#!rzk ind-Σ` we may prove the uniqueness principle, now for Σ-types:
@@ -424,7 +424,7 @@ Using `#!rzk ind-Σ` we can also prove a type-theoretic axiom of choice:
 ```rzk
 #define AxiomOfChoice
   : U
-  := ( A : U)
+  := (A : U)
     → ( B : U)
     → ( R : A → B → U)
     → ( ( x : A) → Σ (y : B) , R x y)

docs/docs/ru/examples/recId.rzk.md

@@ -19,33 +19,33 @@ We begin by introducing common HoTT definitions:
 -- A is contractible there exists x : A such that for any y : A we have x = y.
 #define iscontr (A : U)
   : U
-  := Σ ( a : A) , (x : A) → a =_{A} x
+  := Σ (a : A) , (x : A) → a =_{A} x
 
 -- A is a proposition if for any x, y : A we have x = y
 #define isaprop (A : U)
   : U
-  := ( x : A) → (y : A) → x =_{A} y
+  := (x : A) → (y : A) → x =_{A} y
 
 -- A is a set if for any x, y : A the type x =_{A} y is a proposition
 #define isaset (A : U)
   : U
-  := ( x : A) → (y : A) → isaprop (x =_{A} y)
+  := (x : A) → (y : A) → isaprop (x =_{A} y)
 
 -- A function f : A → B is an equivalence
 -- if there exists g : B → A
 -- such that for all x : A we have g (f x) = x
 -- and for all y : B we have f (g y) = y
 #define isweq (A : U) (B : U) (f : A → B)
   : U
-  := Σ ( g : B → A)
+  := Σ (g : B → A)
   , prod
     ( ( x : A) → g (f x) =_{A} x)
     ( ( y : B) → f (g y) =_{B} y)
 
 -- Equivalence of types A and B
 #define weq (A : U) (B : U)
   : U
-  := Σ ( f : A → B)
+  := Σ (f : A → B)
   , isweq A B f
 
 -- Transport along a path
@@ -66,12 +66,12 @@ We can now define relative function extensionality. There are several formulatio
 -- [RS17, Axiom 4.6] Relative function extensionality.
 #define relfunext
   : U
-  := ( I : CUBE)
+  := (I : CUBE)
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
   → ( ( t : ψ) → iscontr (A t))
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( t : ψ) → A t [ φ t ↦ a t]
 
 -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
@@ -82,9 +82,9 @@ We can now define relative function extensionality. There are several formulatio
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( f : (t : ψ) → A t [ φ t ↦ a t ])
-  → ( g : ( t : ψ) → A t [ φ t ↦ a t ])
+  → ( g : (t : ψ) → A t [ φ t ↦ a t ])
   → weq
     ( f = g)
     ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ])
@@ -106,13 +106,13 @@ First, we define how to restrict an extension type to a subshape:
 
 -- Restrict extension type to a subshape.
 #define restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 
 -- Restrict extension type to a subshape.
 #define restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 ```
@@ -122,14 +122,14 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
 ```rzk
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : ψ)
   → A t [ ψ t ∧ φ t ↦ restrict_psi a t ]
   := a  -- type is coerced automatically here
 
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : φ)
   → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
   := a  -- type is coerced automatically here

docs/docs/ru/getting-started/dependent-types.rzk.md

@@ -83,7 +83,7 @@ Rzk не предоставляет встроенных типов-произв
 #define prod
   ( A B : U)
   : U
-  := Σ ( _ : A) , B
+  := Σ (_ : A) , B
 ```
 
 Запись `#!rzk prod A B` соответствует типу-произведению $A \times B$.
@@ -193,7 +193,7 @@ Rzk не предоставляет встроенных типов-произв
   ( C : U)
   ( f : A → B → C)
   : prod A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Для типа `#!rzk Unit`, принцип рекурсии тривиален:
@@ -228,7 +228,7 @@ Rzk не предоставляет встроенных типов-произв
   ( C : prod A B → U)
   ( f : (a : A) → (b : B) → C (a , b))
   : ( z : prod A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Мы можем использовать `#!rzk ind-prod` для доказательства принципа уникальности.
@@ -318,7 +318,7 @@ Rzk не предоставляет встроенных типов-произв
   ( A : U)
   ( B : A → U)
   : ( Σ ( a : A) , B a) → A
-  := \ ( a , _) → a
+  := \ (a , _) → a
 ```
 
 Однако, для определения второй проекции нужна осторожность. В частности, следующее определение не сработает:
@@ -344,7 +344,7 @@ undefined variable: a
   ( A : U)
   ( B : A → U)
   : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
-  := \ ( _ , b) → b
+  := \ (_ , b) → b
 ```
 
 Иногда о Σ-типах удобнее говорить как о тотальных (общих?) типах (аналогично "total spaces"):
@@ -354,7 +354,7 @@ undefined variable: a
   ( A : U)
   ( B : A → U)
   : U
-  := Σ ( a : A) , B a
+  := Σ (a : A) , B a
 ```
 
 Мы можем переписать более компактно определение второй проекции,
@@ -381,7 +381,7 @@ undefined variable: a
   ( C : U)
   ( f : (a : A) → B a → C)
   : total-type A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Аналогично с принципом индукции:
@@ -393,7 +393,7 @@ undefined variable: a
   ( C : total-type A B → U)
   ( f : (a : A) → (b : B a) → C (a , b))
   : ( z : total-type A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Как и раньше, мы можем использовать `#!rzk ind-Σ` для доказательства принципа уникальности,
@@ -431,7 +431,7 @@ undefined variable: a
 ```rzk
 #define AxiomOfChoice
   : U
-  := ( A : U)
+  := (A : U)
     → ( B : U)
     → ( R : A → B → U)
     → ( ( x : A) → Σ (y : B) , R x y)

rzk/.gitignore

@@ -2,4 +2,3 @@
 *~
 *.bak
 .DS_Store
-Test