diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -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
 
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -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)
-
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -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