Bump version and update changelogs (and CITATION.cff)

CITATION.cff

@@ -3,6 +3,10 @@ authors:
   - family-names: Kudasov
     given-names: Nikolai
     orcid: "https://orcid.org/0000-0001-6572-7292"
+  - family-names: Abounegm
+    given-names: Abdelrahman
+  - family-names: Danko
+    given-names: Danila
 title: "Rzk: a  proof assistant for synthetic $\\infty$-categories"
-version: 0.6.7
+version: 0.7.0
 url: "https://github.com/rzk-lang/rzk"

docs/docs/CHANGELOG.md

@@ -6,6 +6,29 @@ 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.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
 
 - Fix build on some systems (fix `BNFC:bnfc` executable dependency, see [#125](https://github.com/rzk-lang/rzk/pull/125))

rzk/ChangeLog.md

@@ -6,6 +6,10 @@ 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.0 — 2023-12-08
+
+
+
 ## v0.6.7 — 2023-10-07
 
 - Fix build on some systems (fix `BNFC:bnfc` executable dependency, see [#125](https://github.com/rzk-lang/rzk/pull/125))

rzk/package.yaml

@@ -1,5 +1,5 @@
 name: rzk
-version: 0.6.7
+version: 0.7.0
 github: "rzk-lang/rzk"
 license: BSD3
 author: "Nikolai Kudasov"

rzk/rzk.cabal

@@ -5,7 +5,7 @@ cabal-version: 1.24
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.6.7
+version:        0.7.0
 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