rzk 0.7.0 → 0.7.1
raw patch · 3 files changed
+34/−4 lines, 3 files
Files
- ChangeLog.md +24/−0
- app/Main.hs +1/−2
- rzk.cabal +9/−2
ChangeLog.md view
@@ -6,9 +6,33 @@ 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
app/Main.hs view
@@ -23,7 +23,7 @@ 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 @@ exitSuccess Version -> putStrLn (showVersion version)-
rzk.cabal view
@@ -5,7 +5,7 @@ -- 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 <https://github.com/rzk-lang/rzk#readme> category: Dependent Types@@ -76,6 +76,8 @@ , 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 Language.Rzk.VSCode.Env@@ -83,7 +85,6 @@ 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 @@ , 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 @@ , 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 @@ , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010+ if flag(lsp) && !impl(ghcjs)+ cpp-options: -DLSP