From abb9c274e33056d0533fc4c279dc82890cb5b3f4 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 2 Oct 2023 00:00:21 +0300 Subject: [PATCH 1/6] Do not run BNFC on Windows (rely on pre-generated files) --- rzk/Setup.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/rzk/Setup.hs b/rzk/Setup.hs index 9f58444e6..f310944b7 100644 --- a/rzk/Setup.hs +++ b/rzk/Setup.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} -- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262 -- | Custom Setup that runs bnfc to generate the language sub-libraries @@ -18,7 +19,9 @@ main :: IO () main = defaultMainWithHooks $ simpleUserHooks { hookedPrograms = [ bnfcProgram ] , postConf = \args flags packageDesc localBuildInfo -> do +#ifndef mingw32_HOST_OS _ <- system "bnfc -d -p Language.Rzk --generic --functor -o src/ grammar/Syntax.cf" +#endif postConf simpleUserHooks args flags packageDesc localBuildInfo } From af5b3ee4c57859f4a7544609c73774cbb7bbdba6 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 2 Oct 2023 00:00:36 +0300 Subject: [PATCH 2/6] Run GHC workflow on 3 platforms --- .github/workflows/ghc.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ghc.yml b/.github/workflows/ghc.yml index bf96b76f3..094bd65eb 100644 --- a/.github/workflows/ghc.yml +++ b/.github/workflows/ghc.yml @@ -33,7 +33,10 @@ permissions: jobs: build: name: "Build and test with GHC" - runs-on: ubuntu-latest + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, windows-latest, macos-latest] steps: - name: 📥 Checkout repository From cf5595399ae043920c156db2e3cfed1739fc4e6b Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 2 Oct 2023 00:57:34 +0300 Subject: [PATCH 3/6] Use -optP-Wno-nonportable-include-path to fix an issue on macOS --- rzk/package.yaml | 1 + rzk/rzk.cabal | 8 ++++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/rzk/package.yaml b/rzk/package.yaml index 18f4125b7..d0b4e4a7e 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -60,6 +60,7 @@ ghc-options: - -Wmissing-home-modules - -Wpartial-fields - -Wredundant-constraints + - -optP-Wno-nonportable-include-path library: source-dirs: src diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 039ad700a..bf2784caa 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -56,7 +56,7 @@ library Paths_rzk hs-source-dirs: src - ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path build-tools: alex >=3.2.4 , happy >=1.19.9 @@ -99,7 +99,7 @@ executable rzk Paths_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 + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N build-tools: alex >=3.2.4 , happy >=1.19.9 @@ -128,7 +128,7 @@ test-suite doctests 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 + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path build-tools: alex >=3.2.4 , happy >=1.19.9 @@ -157,7 +157,7 @@ test-suite rzk-test Paths_rzk 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 + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N build-tools: alex >=3.2.4 , happy >=1.19.9 From 4314408d0ea612c174b3f4b7db956f6f482a3cfc Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 2 Oct 2023 01:29:52 +0300 Subject: [PATCH 4/6] Run tar in bash on Windows --- .github/workflows/ghc.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ghc.yml b/.github/workflows/ghc.yml index 094bd65eb..67dfd150c 100644 --- a/.github/workflows/ghc.yml +++ b/.github/workflows/ghc.yml @@ -50,6 +50,7 @@ jobs: mkdir -p bin/ cp $(stack exec -- which rzk) bin/. tar -cvzf rzk-bin.tar.gz bin/ + shell: bash - name: Upload rzk binary as Artifact uses: actions/upload-artifact@v3 From 87b2dd17334573213c792797caab8a175d7117cb Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 2 Oct 2023 02:03:24 +0300 Subject: [PATCH 5/6] Use a more specific artifact name for rzk binaries --- .github/workflows/ghc.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ghc.yml b/.github/workflows/ghc.yml index 67dfd150c..6f03698e3 100644 --- a/.github/workflows/ghc.yml +++ b/.github/workflows/ghc.yml @@ -56,7 +56,7 @@ jobs: uses: actions/upload-artifact@v3 with: path: rzk-bin.tar.gz - name: rzk-bin + name: rzk-${{ runner.os }}-${{ runner.arch }}.tar.gz if-no-files-found: error haddock: @@ -99,7 +99,7 @@ jobs: id: download uses: actions/download-artifact@v3 with: - name: rzk-bin + name: rzk-${{ runner.os }}-${{ runner.arch }}.tar.gz - name: Unpack rzk-bin.tar.gz run: | From 3942b8276ee38c440c47161380cd8f83ae6ced8a Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 2 Oct 2023 02:44:02 +0300 Subject: [PATCH 6/6] Bump version and update changelog, move changelog in docs --- CITATION.cff | 2 +- docs/docs/{getting-started/changelog.md => CHANGELOG.md} | 4 ++++ docs/docs/index.md | 2 +- docs/mkdocs.yml | 2 +- rzk/ChangeLog.md | 4 ++++ rzk/package.yaml | 2 +- rzk/rzk.cabal | 2 +- 7 files changed, 13 insertions(+), 5 deletions(-) rename docs/docs/{getting-started/changelog.md => CHANGELOG.md} (99%) diff --git a/CITATION.cff b/CITATION.cff index 7dd423d6c..3518f0999 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -4,5 +4,5 @@ authors: given-names: Nikolai orcid: "https://orcid.org/0000-0001-6572-7292" title: "Rzk: a proof assistant for synthetic $\\infty$-categories" -version: 0.6.5 +version: 0.6.6 url: "https://github.com/rzk-lang/rzk" diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/CHANGELOG.md similarity index 99% rename from docs/docs/getting-started/changelog.md rename to docs/docs/CHANGELOG.md index 4bbfc6fe2..39a65be92 100644 --- a/docs/docs/getting-started/changelog.md +++ b/docs/docs/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.6.6 — 2023-10-02 + +- Fix builds on Windows (and macOS) (see [#121](https://github.com/rzk-lang/rzk/pull/121)) + ## v0.6.5 — 2023-10-01 This version contains mostly intrastructure improvements: diff --git a/docs/docs/index.md b/docs/docs/index.md index 17f0a8ed6..a6a8b1340 100644 --- a/docs/docs/index.md +++ b/docs/docs/index.md @@ -14,4 +14,4 @@ Using such representation is motivated by automatic handling of binders and easi An important part of `rzk` is a tope layer solver, which is essentially a theorem prover for a part of the type theory. A related project, dedicated just to that part is available at . `simple-topes` supports used-defined cubes, topes, and tope layer axioms. Once stable, `simple-topes` will be merged into `rzk`, expanding the proof assistant to the type theory with shapes, allowing formalisations for (variants of) cubical, globular, and other geometric versions of HoTT. -See the list of contributors at [docs/docs/CONTRIBUTORS.md](docs/docs/CONTRIBUTORS.md). +See the list of contributors at [CONTRIBUTORS.md](CONTRIBUTORS.md). diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index 815cb6c59..0860dfe4a 100644 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -7,11 +7,11 @@ nav: - General: - About: index.md - Contributors: CONTRIBUTORS.md + - Changelog: CHANGELOG.md - Getting Started: - Install: getting-started/install.md - Quickstart: getting-started/quickstart.rzk.md - Publishing with MkDocs: getting-started/publishing-with-mkdocs.md - - Changelog: getting-started/changelog.md - Reference: - Introduction: reference/introduction.rzk.md - Cube layer: reference/cube-layer.rzk.md diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index 4bbfc6fe2..39a65be92 100644 --- a/rzk/ChangeLog.md +++ b/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.6.6 — 2023-10-02 + +- Fix builds on Windows (and macOS) (see [#121](https://github.com/rzk-lang/rzk/pull/121)) + ## v0.6.5 — 2023-10-01 This version contains mostly intrastructure improvements: diff --git a/rzk/package.yaml b/rzk/package.yaml index d0b4e4a7e..a76e7f9f2 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,5 +1,5 @@ name: rzk -version: 0.6.5 +version: 0.6.6 github: 'rzk-lang/rzk' license: BSD3 author: 'Nikolai Kudasov' diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index bf2784caa..7a39c812c 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -5,7 +5,7 @@ cabal-version: 1.24 -- see: https://github.com/sol/hpack name: rzk -version: 0.6.5 +version: 0.6.6 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types