From 13759e8347b7c76daabced8522528792502e556f Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 8 Dec 2023 15:50:05 +0300 Subject: [PATCH 1/5] Fix MkDocs workflow: remove --rebase for mike --- .github/workflows/mkdocs.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml index 5aa5f4b3d..dc7d2f3ce 100644 --- a/.github/workflows/mkdocs.yml +++ b/.github/workflows/mkdocs.yml @@ -48,9 +48,9 @@ jobs: - name: 🚀 Deploy with mike (${{ github.ref_name }}, latest) if: ${{ github.ref_name != 'develop' }} run: | - mike deploy --rebase --push --update-aliases --config-file docs/mkdocs.yml ${{ github.ref_name }} latest + mike deploy --push --update-aliases --config-file docs/mkdocs.yml ${{ github.ref_name }} latest - name: 🚀 Deploy with mike (${{ github.ref_name }}) if: ${{ github.ref_name == 'develop' }} run: | - mike deploy --rebase --push --config-file docs/mkdocs.yml ${{ github.ref_name }} + mike deploy --push --config-file docs/mkdocs.yml ${{ github.ref_name }} From 26445417c29d8f95d25afe94c52f334ac2b9d3b1 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 8 Dec 2023 16:31:34 +0300 Subject: [PATCH 2/5] Fix rzk/ChangeLog.md --- rzk/ChangeLog.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index cdec72ed9..dedf7a500 100644 --- a/rzk/ChangeLog.md +++ b/rzk/ChangeLog.md @@ -8,7 +8,26 @@ and this project adheres to the ## 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 From 9b78a15c750699afa93c4dab3735c2aa31e6faac Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 8 Dec 2023 16:55:29 +0300 Subject: [PATCH 3/5] Fix the LSP flag/CPP --- rzk/app/Main.hs | 3 +-- rzk/package.yaml | 5 ++++- rzk/rzk.cabal | 9 ++++++++- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs index fcef0a7cf..d2f6c4c40 100644 --- a/rzk/app/Main.hs +++ b/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) - diff --git a/rzk/package.yaml b/rzk/package.yaml index 6bfaa278f..e9adf3ee0 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -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: diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 5245b3c7c..c89f98be6 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -75,6 +75,8 @@ library , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010 + if flag(lsp) && !impl(ghcjs) + cpp-options: -DLSP if flag(lsp) && !impl(ghcjs) exposed-modules: Language.Rzk.VSCode.Config @@ -83,7 +85,6 @@ library Language.Rzk.VSCode.Logging Language.Rzk.VSCode.Lsp Language.Rzk.VSCode.Tokenize - cpp-options: -DLSP build-depends: aeson >=1.4.2.0 , co-log-core >=0.3.2.0 @@ -119,6 +120,8 @@ executable rzk , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010 + if flag(lsp) && !impl(ghcjs) + cpp-options: -DLSP if !impl(ghcjs) build-depends: optparse-generic >=1.4.0 @@ -149,6 +152,8 @@ test-suite doctests , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010 + if flag(lsp) && !impl(ghcjs) + cpp-options: -DLSP test-suite rzk-test type: exitcode-stdio-1.0 @@ -176,3 +181,5 @@ test-suite rzk-test , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010 + if flag(lsp) && !impl(ghcjs) + cpp-options: -DLSP From 40327246954332f40cd82c48d102bf4257ad719e Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 8 Dec 2023 17:00:21 +0300 Subject: [PATCH 4/5] Format recId.rzk.md --- docs/docs/examples/recId.rzk.md | 189 ++++++++++++++++++-------------- 1 file changed, 106 insertions(+), 83 deletions(-) diff --git a/docs/docs/examples/recId.rzk.md b/docs/docs/examples/recId.rzk.md index 9637578ca..94ffcff85 100644 --- a/docs/docs/examples/recId.rzk.md +++ b/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)) ``` From 0a271e6432dc5fb73dd118e4ede2b609dcbf4ff5 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 8 Dec 2023 17:03:37 +0300 Subject: [PATCH 5/5] Bump version and update changelogs --- CITATION.cff | 2 +- docs/docs/CHANGELOG.md | 5 +++++ rzk/ChangeLog.md | 5 +++++ rzk/package.yaml | 2 +- rzk/rzk.cabal | 2 +- 5 files changed, 13 insertions(+), 3 deletions(-) diff --git a/CITATION.cff b/CITATION.cff index 8f1b81569..7842254e4 100644 --- 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.0 +version: 0.7.1 url: "https://github.com/rzk-lang/rzk" diff --git a/docs/docs/CHANGELOG.md b/docs/docs/CHANGELOG.md index dedf7a500..3d1ab925c 100644 --- a/docs/docs/CHANGELOG.md +++ b/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: diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index dedf7a500..3d1ab925c 100644 --- a/rzk/ChangeLog.md +++ b/rzk/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: diff --git a/rzk/package.yaml b/rzk/package.yaml index e9adf3ee0..4b4f3b999 100644 --- a/rzk/package.yaml +++ b/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" diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index c89f98be6..90603d5ac 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -5,7 +5,7 @@ cabal-version: 1.24 -- see: https://github.com/sol/hpack name: rzk -version: 0.7.0 +version: 0.7.1 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types