Merge branch 'release-v0.5.5'

* release-v0.5.5: Bump version and update changelogs Fix handling of subshapes (more type errors!) Throw an exception when glob returns an empty list Update rzk.nix Install and use the glob library Use CPP in Main.hs Remove executable from rzk.nix Do not remove rzk.cabal when building with GHCJS Remove hpack and with-utf8 from nix files completely Do not use hpack for the GHCJS build Conditionally depend on with-utf8, only for executable Update rzk.nix Install and use the "with-utf8" package Update site_name in mkdocs.yml Add alex and happy to dependencies Configure mkdocs-plugin-rzk
rzk-lang · Sep 19, 2023 · 640f079 · 640f079
2 parents 5fbbbe7 + 13cdc6d
commit 640f079
Show file tree

Hide file tree

Showing 12 changed files with 159 additions and 59 deletions.
diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
@@ -2,21 +2,21 @@ name: Build with GHCJS and Deploy to GitHub Pages
 
 on:
   push:
-    branches: [ main, develop ]
-    tags: [ v* ]
+    branches: [main, develop]
+    tags: [v*]
     paths:
       - .github/workflows/ghcjs.yml
       - rzk/**
       - try-rzk/**
       - stack.yaml
   pull_request:
-    branches: [ main, develop ]
+    branches: [main, develop]
     paths:
       - rzk/**
       - try-rzk/**
       - stack.yaml
 
-  workflow_dispatch:  # allow triggering this workflow manually
+  workflow_dispatch: # allow triggering this workflow manually
 
 permissions:
   contents: write
@@ -35,7 +35,7 @@ jobs:
             substituters = https://cache.nixos.org/ https://cache.iog.io https://nix-community.cachix.org https://miso-haskell.cachix.org
             trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= nix-community.cachix.org-1:mB9FSh9qf2dCimDSUo8Zy7bkq5CX+/rkCWyvRCYg3Fs= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= miso-haskell.cachix.org-1:6N2DooyFlZOHUfJtAx1Q09H0P5XXYzoxxQYiwn6W1e8=
             keep-outputs = true
-      
+
       - name: Restore and cache Nix store
         uses: nix-community/cache-nix-action@v1
         with:
@@ -44,11 +44,10 @@ jobs:
             ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml') }}
             ${{ runner.os }}-nix-
 
-      - name: 🔨 Remove rzk.cabal, lexer and parser generator files
+      - name: 🔨 Remove lexer and parser generator files
         run: |
           rm -f rzk/src/Language/Rzk/Syntax/Lex.x
           rm -f rzk/src/Language/Rzk/Syntax/Par.y
-          rm -f rzk/rzk.cabal
 
       - name: 🔨 Build GHCJS version with Nix
         run: |
@@ -61,7 +60,7 @@ jobs:
           chmod -R +w dist/
           cp try-rzk/index.html dist/.
 
-      - name: "🚀 Publish JS \"binaries\" (${{ github.ref_name }})"
+      - name: '🚀 Publish JS "binaries" (${{ github.ref_name }})'
         if: ${{ github.ref_name != 'main' && github.event_name == 'push' }}
         uses: JamesIves/github-pages-deploy-action@v4
         with:
@@ -71,7 +70,7 @@ jobs:
           clean: false
           single-commit: true
 
-      - name: "🚀 Publish JS \"binaries\""
+      - name: '🚀 Publish JS "binaries"'
         if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
         uses: JamesIves/github-pages-deploy-action@v4
         with:

diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/getting-started/changelog.md
@@ -6,7 +6,24 @@ 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.5.3 — 2022-07-12
+## v0.5.5 — 2023-09-19
+
+This version contains Unicode and tope logic-related fixes:
+
+1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85));
+2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83));
+3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82));
+4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)).
+5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)).
+
+## v0.5.4 — 2023-08-19
+
+This version contains minor improvements:
+
+1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));
+2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).
+
+## v0.5.3 — 2023-07-12
 
 This version contains a few minor improvements:
 
@@ -17,7 +34,7 @@ This version contains a few minor improvements:
 5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983));
 6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66));
 
-## v0.5.2 — 2022-07-05
+## v0.5.2 — 2023-07-05
 
 This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit:
 
@@ -27,7 +44,7 @@ This version introduces support for Unicode syntax, better recognition of Markdo
 - Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk;
 - Use new cache action for Nix (see [#60](https://github.com/rzk-lang/rzk/pull/60)).
 
-## v0.5.1 — 2022-06-29
+## v0.5.1 — 2023-06-29
 
 This version fixes `Unit` type and makes some changes to documentation:
 
@@ -38,15 +55,15 @@ This version fixes `Unit` type and makes some changes to documentation:
 - Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57));
 - Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b));
 
-## v0.5 — 2022-06-20
+## v0.5 — 2023-06-20
 
 This version contains the following changes:
 
 - `Unit` type (with `unit` value) (see [ede02611](https://github.com/rzk-lang/rzk/commit/ede02611) and [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9);
 - Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53));
 - Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)).
 
-## v0.4.1 — 2022-06-16
+## v0.4.1 — 2023-06-16
 
 This is version contains minor changes, primarily in tools around rzk:
 
@@ -57,7 +74,7 @@ This is version contains minor changes, primarily in tools around rzk:
 - Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2));
 - Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f));
 
-## v0.4.0 — 2022-05-18
+## v0.4.0 — 2023-05-18
 
 This version introduces sections and variables. The feature is similar to <a href="https://coq.inria.fr/refman/language/core/assumptions.html#coq:cmd.Variable" target="_blank">`Variable` command in Coq</a>. An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.
 
@@ -68,7 +85,7 @@ Minor improvements:
 - Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39));
 - Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62));
 
-## v0.3.0 — 2022-04-28
+## v0.3.0 — 2023-04-28
 
 This version introduces an experimental feature for generating visualisations for simplicial terms in SVG.
 To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
@@ -87,7 +104,7 @@ Fixes:
 - Fixed an issue with tope solver when context was empty (see 6196af9e);
 - Fixed #33 (missing coherence check for restricted types).
 
-## v0.2.0 - 2022-04-20
+## v0.2.0 - 2023-04-20
 
 This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.
 

diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
@@ -1,4 +1,4 @@
-site_name: "rzk: an experimental proof assistant for syntheric ∞-categories"
+site_name: "rzk: an experimental proof assistant for synthetic ∞-categories"
 repo_url: https://github.com/rzk-lang/rzk
 repo_name: rzk-lang/rzk
 edit_uri: edit/develop/docs/docs/
@@ -113,5 +113,7 @@ extra:
 
 plugins:
   - mike
-  - rzk
+  - rzk:
+      render_svg: true
+      anchor_definitions: true
   - search
diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md
@@ -6,14 +6,24 @@ 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.5.4 — 2022-08-19
+## v0.5.5 — 2023-09-19
+
+This version contains Unicode and tope logic-related fixes:
+
+1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85));
+2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83));
+3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82));
+4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)).
+5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)).
+
+## v0.5.4 — 2023-08-19
 
 This version contains minor improvements:
 
 1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));
 2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).
 
-## v0.5.3 — 2022-07-12
+## v0.5.3 — 2023-07-12
 
 This version contains a few minor improvements:
 
@@ -24,7 +34,7 @@ This version contains a few minor improvements:
 5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983));
 6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66));
 
-## v0.5.2 — 2022-07-05
+## v0.5.2 — 2023-07-05
 
 This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit:
 
@@ -34,7 +44,7 @@ This version introduces support for Unicode syntax, better recognition of Markdo
 - Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk;
 - Use new cache action for Nix (see [#60](https://github.com/rzk-lang/rzk/pull/60)).
 
-## v0.5.1 — 2022-06-29
+## v0.5.1 — 2023-06-29
 
 This version fixes `Unit` type and makes some changes to documentation:
 
@@ -45,15 +55,15 @@ This version fixes `Unit` type and makes some changes to documentation:
 - Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57));
 - Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b));
 
-## v0.5 — 2022-06-20
+## v0.5 — 2023-06-20
 
 This version contains the following changes:
 
 - `Unit` type (with `unit` value) (see [ede02611](https://github.com/rzk-lang/rzk/commit/ede02611) and [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9);
 - Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53));
 - Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)).
 
-## v0.4.1 — 2022-06-16
+## v0.4.1 — 2023-06-16
 
 This is version contains minor changes, primarily in tools around rzk:
 
@@ -64,7 +74,7 @@ This is version contains minor changes, primarily in tools around rzk:
 - Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2));
 - Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f));
 
-## v0.4.0 — 2022-05-18
+## v0.4.0 — 2023-05-18
 
 This version introduces sections and variables. The feature is similar to <a href="https://coq.inria.fr/refman/language/core/assumptions.html#coq:cmd.Variable" target="_blank">`Variable` command in Coq</a>. An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.
 
@@ -75,7 +85,7 @@ Minor improvements:
 - Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39));
 - Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62));
 
-## v0.3.0 — 2022-04-28
+## v0.3.0 — 2023-04-28
 
 This version introduces an experimental feature for generating visualisations for simplicial terms in SVG.
 To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
@@ -94,7 +104,7 @@ Fixes:
 - Fixed an issue with tope solver when context was empty (see 6196af9e);
 - Fixed #33 (missing coherence check for restricted types).
 
-## v0.2.0 - 2022-04-20
+## v0.2.0 - 2023-04-20
 
 This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.
 

diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs
@@ -1,6 +1,14 @@
+{-# LANGUAGE CPP #-}
 module Main (main) where
 
+#ifndef __GHCJS__
+import           Main.Utf8 (withUtf8)
+#endif
 import qualified Rzk.Main
 
 main :: IO ()
-main = Rzk.Main.main
+main =
+#ifndef __GHCJS__
+  withUtf8
+#endif
+    Rzk.Main.main
diff --git a/rzk/package.yaml b/rzk/package.yaml
@@ -1,5 +1,5 @@
 name: rzk
-version: 0.5.4
+version: 0.5.5
 github: "rzk-lang/rzk"
 license: BSD3
 author: "Nikolai Kudasov"
@@ -18,6 +18,10 @@ category: Dependent Types # same as Agda
 # common to point users to the README.md file.
 description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 
+build-tools:
+  - alex
+  - happy
+
 dependencies:
   - array
   - aeson
@@ -28,6 +32,7 @@ dependencies:
   - template-haskell
   - text
   - optparse-generic
+  - Glob
 
 ghc-options:
   - -Wall
@@ -59,6 +64,10 @@ executables:
       - -with-rtsopts=-N
     dependencies:
       - rzk
+    when:
+      - condition: "!impl(ghcjs)"
+        dependencies:
+          - with-utf8
 
 tests:
   rzk-test:

diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.1.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.5.4
+version:        0.5.5
 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
@@ -46,8 +46,12 @@ library
   hs-source-dirs:
       src
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+  build-tools:
+      alex
+    , happy
   build-depends:
-      aeson
+      Glob
+    , aeson
     , array
     , base >=4.7 && <5
     , bifunctors
@@ -65,8 +69,12 @@ executable rzk
   hs-source-dirs:
       app
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-tools:
+      alex
+    , happy
   build-depends:
-      aeson
+      Glob
+    , aeson
     , array
     , base >=4.7 && <5
     , bifunctors
@@ -77,13 +85,19 @@ executable rzk
     , template-haskell
     , text
   default-language: Haskell2010
+  if !impl(ghcjs)
+    build-depends:
+        with-utf8
 
 test-suite doctests
   type: exitcode-stdio-1.0
   main-is: doctests.hs
   hs-source-dirs:
       test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+  build-tools:
+      alex
+    , happy
   build-depends:
       Glob
     , QuickCheck
@@ -107,8 +121,12 @@ test-suite rzk-test
   hs-source-dirs:
       test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-tools:
+      alex
+    , happy
   build-depends:
-      aeson
+      Glob
+    , aeson
     , array
     , base >=4.7 && <5
     , bifunctors