rzk 0.7.1 → 0.7.2

raw patch · 4 files changed

+39/−13 lines, 4 files

Files

• ChangeLog.md +20/−0
• rzk.cabal +1/−1
• src/Rzk/Format.hs +10/−6
• src/Rzk/Main.hs +8/−6

@@ -6,6 +6,26 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.2 — 2023-12-12++Fixes:+- Fixes for `rzk format`:+    - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));+    - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));+- Throw an error when `rzk.yaml`'s `include` is empty (see [#154](https://github.com/rzk-lang/rzk/pull/154));++Changes to the Rzk website:+  - Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));+      - English is the default;+      - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;+  - Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));+      - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;+  - Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));+  - Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))+  - Add (default) social cards+  - Integrate ToC on the left+  - Use Inria Sans for English, PT Sans for Russian+ ## 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));

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

@@ -59,6 +59,10 @@     rzkBlocks = tryExtractMarkdownCodeBlocks "rzk" contents -- TODO: replace tabs with spaces     contentLines line = lines rzkBlocks !! (line - 1) -- Sorry     toks = resolveLayout True (tokens rzkBlocks)+    lineTokensBefore line col = filter isBefore toks+      where+        isBefore (PT (Pn _ l c) _) = l == line && c < col+        isBefore _                 = False     unicodeTokens =       [ ("->", "→")       , ("|->", "↦")@@ -120,15 +124,15 @@       where         spaceCol = col + 1         lineContent = contentLines line-        -- | This is similar to (\\) but removes all occurrences (not just the first one)-        setDifference xs excludes = filter (not . (`elem` excludes)) xs-        precededBySingleCharOnly = null $ foldl' setDifference (take (col - 1) lineContent) punctuations+        precededBySingleCharOnly = all isPunctuation (lineTokensBefore line col)+        singleCharUnicodeTokens = filter (\(_, unicode) -> length unicode == 1) unicodeTokens         punctuations = concat-          [ map fst unicodeTokens -- ASCII sequences will be converted soon-          , map snd unicodeTokens+          [ map fst singleCharUnicodeTokens -- ASCII sequences will be converted soon+          , map snd singleCharUnicodeTokens           , ["(", ":", ",", "="]-          , [" ", "\t"]           ]+        isPunctuation (Token tk _ _) = tk `elem` punctuations+        isPunctuation _              = False         spacesAfter = length $ takeWhile (== ' ') (drop col lineContent)         isLastNonSpaceChar = all (== ' ') (drop col lineContent) 

@@ -5,12 +5,13 @@  module Rzk.Main where -import           Control.Monad           (forM, when)-import           Data.List               (sort)-import qualified Data.Yaml               as Yaml-import           System.Directory        (doesPathExist)-import           System.FilePath.Glob    (glob)-import qualified Language.Rzk.Syntax     as Rzk+import           Control.Monad        (forM, when)+import           Data.List            (sort)+import qualified Data.Yaml            as Yaml+import           System.Directory     (doesPathExist)+import           System.FilePath.Glob (glob)++import qualified Language.Rzk.Syntax  as Rzk import           Rzk.Project.Config import           Rzk.TypeCheck @@ -69,6 +70,7 @@       then do         putStrLn ("Using Rzk project stucture specified in " <> rzkYamlPath)         paths <- extractFilesFromRzkYaml rzkYamlPath+        when (null paths) (error $ "No Rzk files specified in the config file at " <> rzkYamlPath)         parseRzkFilesOrStdin paths       else do         rzkModule <- parseStdin