Merge branch 'release-v0.7.1'

* release-v0.7.1:
  Bump version and update changelogs
  Format recId.rzk.md
  Fix the LSP flag/CPP
  Fix rzk/ChangeLog.md
  Fix MkDocs workflow: remove --rebase for mike

Author: fizruk

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

docs/docs/CHANGELOG.md

@@ -6,6 +6,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.7.1 — 2023-12-08
+
+- Fix default build to include Rzk Language Server (`rzk lsp`) (see [`9b78a15`](https://github.com/rzk-lang/rzk/commit/9b78a15c750699afa93c4dab3735c2aa31e6faac));
+- Apply formatting to `recId.rzk.md` example (see [`4032724`](https://github.com/rzk-lang/rzk/commit/40327246954332f40cd82c48d102bf4257ad719e));
+
 ## v0.7.0 — 2023-12-08
 
 Major changes:

docs/docs/examples/recId.rzk.md

@@ -13,40 +13,50 @@ We begin by introducing common HoTT definitions:
 #lang rzk-1
 
 -- 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
+#define iscontr (A : U)
+  : U
+  := Σ ( 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
+#define isaprop (A : U)
+  : U
+  := ( 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)
+#define isaset (A : U)
+  : U
+  := ( x : A) → (y : A) → isaprop (x =_{A} y)
 
 -- Non-dependent product of A and B
-#define prod (A : U) (B : U) : U
-  := Σ (x : A), B
+#define prod (A : U) (B : U)
+  : U
+  := Σ ( x : A) , B
 
 -- 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), prod ((x : A) → g (f x) =_{A} x) ((y : B) → f (g y) =_{B} y)
+#define isweq (A : U) (B : U) (f : A → B)
+  : U
+  := Σ ( 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), isweq A B f
+#define weq (A : U) (B : U)
+  : U
+  := Σ ( f : A → B)
+  , isweq A B f
 
 -- Transport along a path
 #define transport
-    (A : U)
-    (C : A → U)
-    (x y : A)
-    (p : x =_{A} y)
-    : C x → C y
-  := \ cx → idJ(A, x, (\z q → C z), cx, y, p)
+  ( A : U)
+  ( C : A → U)
+  ( x y : A)
+  ( p : x =_{A} y)
+  : C x → C y
+  := \ cx → idJ(A , x , (\ z q → C z) , cx , y , p)
 ```
 
 ## Relative function extensionality
@@ -55,26 +65,30 @@ We can now define relative function extensionality. There are several formulatio
 
 ```rzk
 -- [RS17, Axiom 4.6] Relative function extensionality.
-#define relfunext : U
-  := (I : CUBE)
-  → (ψ : I → TOPE)
-  → (φ : ψ → TOPE)
-  → (A : ψ → U)
-  → ((t : ψ) → iscontr (A t))
-  → (a : (t : φ) → A t)
-  → (t : ψ) → A t [ φ t ↦ a t]
+#define relfunext
+  : U
+  := ( I : CUBE)
+  → ( ψ : I → TOPE)
+  → ( φ : ψ → TOPE)
+  → ( A : ψ → U)
+  → ( ( t : ψ) → iscontr (A t))
+  → ( a : ( t : φ) → A t)
+  → ( t : ψ) → A t [ φ t ↦ a t]
 
 -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
-#define relfunext2 : U
-  := (I : CUBE)
-  → (ψ : I → TOPE)
-  → (φ : ψ → TOPE)
-  → (A : ψ → U)
-  → (a : (t : φ) → A t)
-  → (f : (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 ])
+#define relfunext2
+  : U
+  :=
+    ( I : CUBE)
+  → ( ψ : I → TOPE)
+  → ( φ : ψ → TOPE)
+  → ( A : ψ → U)
+  → ( a : ( t : φ) → A t)
+  → ( f : (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 ])
 ```
 
 ## Construction of `recId`
@@ -93,14 +107,14 @@ 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)
-  : (t : I | ψ t ∧ φ 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)
-  : (t : I | ψ t ∧ φ t) → A t
+  ( a : ( t : ψ) → A t)
+  : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 ```
 
@@ -109,14 +123,16 @@ 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)
-  : (t : ψ) → A t [ ψ t ∧ φ t ↦ restrict_psi 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)
-  : (t : φ) → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
+  ( a : ( t : φ) → A t)
+  : ( t : φ)
+  → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
   := a  -- type is coerced automatically here
 ```
 
@@ -125,17 +141,20 @@ Now, assuming relative function extensionality, we construct a path between rest
 ```rzk
 -- Transform extension of an identity into an identity of restrictions.
 #define restricts-path
-    (a_psi : (t : ψ) → A t)
-    (a_phi : (t : φ) → A t)
-    (e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
-  : restrict_psi a_psi = restrict_phi a_phi
-  := (first (second (r I
-      (\t → ψ t ∧ φ t)
-      (\t → BOT)
-      (\t → A t)
-      (\t → recBOT)
-      (\t → a_psi t)
-      (\t → a_phi t)))) e
+  ( a_psi : (t : ψ) → A t)
+  ( a_phi : (t : φ) → A t)
+  : ( e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
+  → restrict_psi a_psi = restrict_phi a_phi
+  :=
+  first
+  ( second
+    ( r I
+      ( \ t → ψ t ∧ φ t)
+      ( \ t → BOT)
+      ( \ t → A t)
+      ( \ t → recBOT)
+      ( \ t → a_psi t)
+      ( \ t → a_phi t)))
 ```
 
 Finally, we bring everything together into `recId`:
@@ -145,20 +164,22 @@ Finally, we bring everything together into `recId`:
 -- recOR(ψ, φ, a, b) demands that for ψ ∧ φ we have a == b (definitionally)
 -- (recId ψ φ a b e) demands that e is the proof that a = b (intensionally) for ψ ∧ φ
 #define recId uses (r) -- we declare that recId is using r on purpose
-    (a_psi : (t : ψ) → A t)
-    (a_phi : (t : φ) → A t)
-    (e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
-  : (t : I | ψ t ∨ φ t) → A t
-  := \t → recOR(
-        ψ t ↦ transport
-          ((s : I | ψ s ∧ φ s) → A s)
-          (\ra → (s : ψ) → A s [ ψ s ∧ φ s ↦ ra s ])
-          (restrict_psi a_psi)
-          (restrict_phi a_phi)
-          (restricts-path a_psi a_phi e)
-          (ext-of-restrict_psi a_psi)
-          t,
-        φ t ↦ ext-of-restrict_phi a_phi t
+  ( a_psi : (t : ψ) → A t)
+  ( a_phi : (t : φ) → A t)
+  ( e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
+  : ( t : I | ψ t ∨ φ t) → A t
+  := \ t → recOR(
+        ψ t ↦
+          transport
+          ( ( s : I | ψ s ∧ φ s) → A s)
+          ( \ ra → (s : ψ) → A s [ ψ s ∧ φ s ↦ ra s ])
+          ( restrict_psi a_psi)
+          ( restrict_phi a_phi)
+          ( restricts-path a_psi a_phi e)
+          ( ext-of-restrict_psi a_psi)
+          ( t)
+      , φ t ↦
+          ext-of-restrict_phi a_phi t
       )
 
 #end construction-of-recId
@@ -173,18 +194,20 @@ whenever we can show that they are equal on the intersection of shapes:
 -- If two extension types are equal along two subshapes,
 -- then they are also equal along their union.
 #define id-along-border
-    (r : relfunext2)
-    (I : CUBE)
-    (ψ : I → TOPE)
-    (φ : I → TOPE)
-    (A : (t : I | ψ t ∨ φ t) → U)
-    (a b : (t : I | ψ t ∨ φ t) → A t)
-    (e_psi : (t : ψ) → a t = b t)
-    (e_phi : (t : φ) → a t = b t)
-    (border-is-a-set : (t : I | ψ t ∧ φ t) → isaset (A t))
-  : (t : I | ψ t ∨ φ t) → a t = b t
-  := recId r I ψ φ
-        (\t → a t = b t)
-        e_psi e_phi
-        (\t → border-is-a-set t (a t) (b t) (e_psi t) (e_phi t))
+  ( r : relfunext2)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( φ : I → TOPE)
+  ( A : (t : I | ψ t ∨ φ t) → U)
+  ( a b : (t : I | ψ t ∨ φ t) → A t)
+  ( e_psi : (t : ψ) → a t = b t)
+  ( e_phi : (t : φ) → a t = b t)
+  ( border-is-a-set : (t : I | ψ t ∧ φ t) → isaset (A t))
+  : ( t : I | ψ t ∨ φ t) → a t = b t
+  :=
+  recId r I ψ φ
+  ( \ t → a t = b t)
+  ( e_psi)
+  ( e_phi)
+  ( \ t → border-is-a-set t (a t) (b t) (e_psi t) (e_phi t))
 ```

rzk/ChangeLog.md

@@ -6,9 +6,33 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.7.1 — 2023-12-08
+
+- Fix default build to include Rzk Language Server (`rzk lsp`) (see [`9b78a15`](https://github.com/rzk-lang/rzk/commit/9b78a15c750699afa93c4dab3735c2aa31e6faac));
+- Apply formatting to `recId.rzk.md` example (see [`4032724`](https://github.com/rzk-lang/rzk/commit/40327246954332f40cd82c48d102bf4257ad719e));
+
 ## v0.7.0 — 2023-12-08
 
+Major changes:
+
+- Add an experimental `rzk format` command (by [Abdelrahman Abounegm](https://github.com/aabounegm), with feedback by [Fredrik Bakke](https://github.com/fredrik-bakke) (see [sHoTT#142](https://github.com/rzk-lang/sHoTT/pull/142)) and [Nikolai Kudasov](https://github.com/fizruk)):
+  - Automatically format files, partially automating the [Code Style of the sHoTT project](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/)
+  - Notable features:
+    - Adds a space after the opening parenthesis to help with the [code tree structure](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/#the-tree-structure-of-constructions)
+    - Puts the definition conclusion (type, starting with `:`) and construction (body, starting with `:=`) on new lines
+    - Adds a space after the `\` of a lambda term and around binary operators (like `,`)
+    - Moves binary operators to the beginning of the next line if they appear at the end of the previous one.
+    - Replaces [common ASCII sequences](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/#use-of-unicode-characters) with their Unicode equivalent
+    - A CLI subcommand (`rzk format`) with `--check` and `--write` options
+  - Known limitations
+    - The 80 character line limit is currently not enforced due to the difficulty of determining where to add line breaks (for reference, check out [this post](https://journal.stuffwithstuff.com/2015/09/08/the-hardest-program-ive-ever-written/) by a Dart `fmt` engineer)
+    - Fixing indentation is not yet implemented due to the need for more semantics than the lexer provides to determine indentation level.
+    - There may be rare edge cases in which applying the formatter twice could result in additional edits that were not detected the first time.
+
+Minor changes:
 
+- Fix "latest" Rzk Playground link (see [#137](https://github.com/rzk-lang/rzk/pull/137));
+- Add more badges to README (see [#136](https://github.com/rzk-lang/rzk/pull/136));
 
 ## v0.6.7 — 2023-10-07
 

rzk/app/Main.hs

@@ -23,7 +23,7 @@ import           Language.Rzk.VSCode.Lsp (runLsp)
 import           Options.Generic
 import           System.Exit             (exitFailure, exitSuccess)
 
-import           Data.Functor            ((<&>))
+import           Data.Functor            (void, (<&>))
 import           Paths_rzk               (version)
 import           Rzk.Format              (formatFile, formatFileWrite,
                                           isWellFormattedFile)
@@ -90,4 +90,3 @@ main = do
             exitSuccess
 
     Version -> putStrLn (showVersion version)
-

rzk/package.yaml

@@ -1,5 +1,5 @@
 name: rzk
-version: 0.7.0
+version: 0.7.1
 github: "rzk-lang/rzk"
 license: BSD3
 author: "Nikolai Kudasov"
@@ -26,6 +26,10 @@ flags:
     manual: true
     default: true
 
+when:
+  - condition: flag(lsp) && !impl(ghcjs)
+    cpp-options: -DLSP
+
 custom-setup:
   dependencies:
     base: ">= 4.11.0.0 && < 5.0"
@@ -86,7 +90,6 @@ library:
         lsp: ">= 2.2.0.0"
         lsp-types: ">= 2.0.2.0"
         stm: ">= 2.5.0.0"
-      cpp-options: -DLSP
 
 executables:
   rzk: