From 39f0b2f6da54f3b075508fef75e168f267a84961 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:27:48 +0300 Subject: [PATCH 01/58] add: rzk-playground --- rzk-playground/.eslintrc.json | 5 + rzk-playground/.gitignore | 37 + rzk-playground/README.md | 36 + rzk-playground/app/globals.css | 99 + rzk-playground/app/layout.tsx | 21 + rzk-playground/app/page.tsx | 137 + rzk-playground/components/editor/Editor.tsx | 37 + rzk-playground/components/editor/example.ts | 142 + rzk-playground/components/editor/theme.ts | 199 + rzk-playground/next.config.js | 7 + rzk-playground/package-lock.json | 3676 +++++++++++++++++++ rzk-playground/package.json | 31 + rzk-playground/src/rzk-wrapper.js | 5 + rzk-playground/src/rzk.ts | 8 + rzk-playground/tsconfig.json | 27 + 15 files changed, 4467 insertions(+) create mode 100644 rzk-playground/.eslintrc.json create mode 100644 rzk-playground/.gitignore create mode 100644 rzk-playground/README.md create mode 100644 rzk-playground/app/globals.css create mode 100644 rzk-playground/app/layout.tsx create mode 100644 rzk-playground/app/page.tsx create mode 100644 rzk-playground/components/editor/Editor.tsx create mode 100644 rzk-playground/components/editor/example.ts create mode 100644 rzk-playground/components/editor/theme.ts create mode 100644 rzk-playground/next.config.js create mode 100644 rzk-playground/package-lock.json create mode 100644 rzk-playground/package.json create mode 100644 rzk-playground/src/rzk-wrapper.js create mode 100644 rzk-playground/src/rzk.ts create mode 100644 rzk-playground/tsconfig.json diff --git a/rzk-playground/.eslintrc.json b/rzk-playground/.eslintrc.json new file mode 100644 index 000000000..73601b742 --- /dev/null +++ b/rzk-playground/.eslintrc.json @@ -0,0 +1,5 @@ +{ + "extends": [ + "next" + ] +} \ No newline at end of file diff --git a/rzk-playground/.gitignore b/rzk-playground/.gitignore new file mode 100644 index 000000000..6a01e9822 --- /dev/null +++ b/rzk-playground/.gitignore @@ -0,0 +1,37 @@ +# See https://help.github.com/articles/ignoring-files/ for more about ignoring files. + +# dependencies +/node_modules +/.pnp +.pnp.js + +# testing +/coverage + +# next.js +/.next/ +/out/ + +# production +/build + +# misc +.DS_Store +*.pem + +# debug +npm-debug.log* +yarn-debug.log* +yarn-error.log* + +# local env files +.env*.local + +# vercel +.vercel + +# typescript +*.tsbuildinfo +next-env.d.ts + +public/rzk.js \ No newline at end of file diff --git a/rzk-playground/README.md b/rzk-playground/README.md new file mode 100644 index 000000000..c4033664f --- /dev/null +++ b/rzk-playground/README.md @@ -0,0 +1,36 @@ +This is a [Next.js](https://nextjs.org/) project bootstrapped with [`create-next-app`](https://github.com/vercel/next.js/tree/canary/packages/create-next-app). + +## Getting Started + +First, run the development server: + +```bash +npm run dev +# or +yarn dev +# or +pnpm dev +# or +bun dev +``` + +Open [http://localhost:3000](http://localhost:3000) with your browser to see the result. + +You can start editing the page by modifying `app/page.tsx`. The page auto-updates as you edit the file. + +This project uses [`next/font`](https://nextjs.org/docs/basic-features/font-optimization) to automatically optimize and load Inter, a custom Google Font. + +## Learn More + +To learn more about Next.js, take a look at the following resources: + +- [Next.js Documentation](https://nextjs.org/docs) - learn about Next.js features and API. +- [Learn Next.js](https://nextjs.org/learn) - an interactive Next.js tutorial. + +You can check out [the Next.js GitHub repository](https://github.com/vercel/next.js/) - your feedback and contributions are welcome! + +## Deploy on Vercel + +The easiest way to deploy your Next.js app is to use the [Vercel Platform](https://vercel.com/new?utm_medium=default-template&filter=next.js&utm_source=create-next-app&utm_campaign=create-next-app-readme) from the creators of Next.js. + +Check out our [Next.js deployment documentation](https://nextjs.org/docs/deployment) for more details. diff --git a/rzk-playground/app/globals.css b/rzk-playground/app/globals.css new file mode 100644 index 000000000..114c45fc9 --- /dev/null +++ b/rzk-playground/app/globals.css @@ -0,0 +1,99 @@ +section { + width: 100%; +} + +body { + margin: 0; + background-color: #000; +} + +.row { + display: flex; + justify-content: space-evenly; + margin: 0; + padding: 0; + width: 100%; +} + +.column { + margin-top: 0; + margin-bottom: 0; + width: 100%; +} + +#__codemirror__ { + font-family: Inconsolata, monospace; +} + +#__app__ { + margin: 20px; +} + +/* CSS for response button from https://getcssscan.com/css-buttons-examples (button 61) */ +#btnTypecheck { + align-items: center; + appearance: none; + border-radius: 4px; + border-style: none; + box-shadow: rgba(0, 0, 0, .2) 0 3px 1px -2px, rgba(0, 0, 0, .14) 0 2px 2px 0, rgba(0, 0, 0, .12) 0 1px 5px 0; + box-sizing: border-box; + color: #fff; + cursor: pointer; + display: inline-flex; + font-family: Roboto, sans-serif; + font-size: .875rem; + font-weight: 500; + height: 36px; + justify-content: center; + letter-spacing: .0892857em; + line-height: normal; + min-width: 64px; + outline: none; + overflow: visible; + padding: 0 16px; + position: relative; + text-align: center; + text-decoration: none; + text-transform: uppercase; + transition: box-shadow 280ms cubic-bezier(.4, 0, .2, 1); + user-select: none; + -webkit-user-select: none; + touch-action: manipulation; + vertical-align: middle; + will-change: transform, opacity; +} + +#btnTypecheck:hover { + box-shadow: rgba(0, 0, 0, .2) 0 2px 4px -1px, rgba(0, 0, 0, .14) 0 4px 5px 0, rgba(0, 0, 0, .12) 0 1px 10px 0; +} + +#btnTypecheck:disabled { + background-color: rgba(0, 0, 0, .12); + box-shadow: rgba(0, 0, 0, .2) 0 0 0 0, rgba(0, 0, 0, .14) 0 0 0 0, rgba(0, 0, 0, .12) 0 0 0 0; + color: rgba(0, 0, 0, .37); + cursor: default; + pointer-events: none; +} + +#btnTypecheck:not(:disabled) { + background-color: #6200ee; +} + +#btnTypecheck:focus { + box-shadow: rgba(0, 0, 0, .2) 0 2px 4px -1px, rgba(0, 0, 0, .14) 0 4px 5px 0, rgba(0, 0, 0, .12) 0 1px 10px 0; +} + +#btnTypecheck:active { + box-shadow: rgba(0, 0, 0, .2) 0 5px 5px -3px, rgba(0, 0, 0, .14) 0 8px 10px 1px, rgba(0, 0, 0, .12) 0 3px 14px 2px; + background: #A46BF5; +} + +#message { + background-color: #202028; + color: #eee8d5; + overflow: scroll; +} + +#message pre { + font-family: Inconsolata, monospace; +} \ No newline at end of file diff --git a/rzk-playground/app/layout.tsx b/rzk-playground/app/layout.tsx new file mode 100644 index 000000000..3df54bf87 --- /dev/null +++ b/rzk-playground/app/layout.tsx @@ -0,0 +1,21 @@ +import './globals.css' +import type { Metadata } from 'next' +import { Inter } from 'next/font/google' + +const inter = Inter({ subsets: ['latin'] }) + +export const metadata: Metadata = { + title: 'Try Rzk proof assistant!' +} + +export default function RootLayout({ + children, +}: { + children: React.ReactNode +}) { + return ( + + {children} + + ) +} diff --git a/rzk-playground/app/page.tsx b/rzk-playground/app/page.tsx new file mode 100644 index 000000000..a709af66c --- /dev/null +++ b/rzk-playground/app/page.tsx @@ -0,0 +1,137 @@ +'use client'; + +import { useCallback, useEffect, useState } from 'react'; +import Editor from '../components/editor/Editor'; +import Script from 'next/script'; +import { Resizable } from 're-resizable'; +import React from 'react'; +import { color } from '../components/editor/theme'; +import * as rzk from '../src/rzk'; +import { KeyBindProvider, ShortcutType } from 'react-keybinds'; +import dynamic from 'next/dynamic'; + +const style = { + display: "flex", + alignItems: "center", + justifyContent: "center", + background: color.background +} + +var typecheckedOnStart = false + +declare var window: Window & typeof globalThis; + +function HomeNoSSR() { + const [message, setMessage] = useState("Starting..."); + + const [windowHeight, setWindowHeight] = useState(window.innerHeight) + const [editorHeight, setHeight] = React.useState(windowHeight * 70 / 100) + const [needTypecheck, setNeedTypecheck] = useState(false) + + useEffect(() => { + const handleWindowResize = () => { + setWindowHeight(window.innerHeight) + }; + + window.addEventListener('resize', handleWindowResize); + + return () => { + window.removeEventListener('resize', handleWindowResize); + }; + }, []); + + const [text, setText] = useState("") + + const typecheck = useCallback(() => { + const result = rzk.typecheck(text) + if (result.status == 'ok') { + setMessage(`Everything is OK!`) + } else { + setMessage(result.result) + } + }, [text]) + + useEffect(() => { + function checkFlag() { + if ((!((window as any).rzkTypecheck_) || (text === "")) && !typecheckedOnStart) { + console.warn("something bad") + console.warn((window as any).rzkTypecheck_) + window.setTimeout(checkFlag, 100); /* this checks the flag every 100 milliseconds*/ + } else if (!typecheckedOnStart) { + typecheck() + typecheckedOnStart = true + } + } + + if (!typecheckedOnStart) { + checkFlag(); + } + }, [typecheck, text]) + + useEffect(() => { + if (needTypecheck) { + typecheck() + setNeedTypecheck(false) + } + }, [setNeedTypecheck, needTypecheck, typecheck]) + + const KEYBINDINGS: ShortcutType[] = + [ + { + keys: { + Mac: ['Shift', 'Enter'], + Windows: ['Shift', 'Enter'], + Linux: ['Shift', 'Enter'], + }, + label: 'Test command', + callback: () => { + setNeedTypecheck(true) + }, + }, + ] + ; + + return ( +
+
+ - - - - - - - - - - - - - -
-
-
-
-
-
-
-
-
- - - - diff --git a/try-rzk/result b/try-rzk/result deleted file mode 120000 index 7852af3a6..000000000 --- a/try-rzk/result +++ /dev/null @@ -1 +0,0 @@ -/nix/store/ffp11s3gkqfisqb787rfl2v4vr06rpax-try-rzk-0.1.0 \ No newline at end of file From ef315347d97b110cf2d6f1929bf9854596391dc4 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:29:14 +0300 Subject: [PATCH 03/58] fix: update hs code for ghc 9.6.2 --- rzk/src/Language/Rzk/Free/Syntax.hs | 2 +- rzk/src/Language/Rzk/VSCode/Handlers.hs | 3 ++- rzk/src/Rzk/TypeCheck.hs | 1 + 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs index d9803bcd8..717714281 100644 --- a/rzk/src/Language/Rzk/Free/Syntax.hs +++ b/rzk/src/Language/Rzk/Free/Syntax.hs @@ -94,7 +94,7 @@ data TermF scope term | TypeUnitF | TypeAscF term term | TypeRestrictedF term [(term, term)] - deriving (Eq) + deriving (Eq, Functor) deriveBifunctor ''TermF deriveBifoldable ''TermF deriveBitraversable ''TermF diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index 55c61809c..1037d5fba 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -8,7 +8,8 @@ module Language.Rzk.VSCode.Handlers where import Control.Exception (SomeException, evaluate, try) import Control.Lens -import Control.Monad.Cont (MonadIO (liftIO), forM_) +import Control.Monad (forM_) +import Control.Monad.IO.Class (MonadIO (liftIO)) import Data.Default.Class import Data.List (sort, (\\)) import Data.Maybe (fromMaybe) diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index 7d1353958..3976c55eb 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -10,6 +10,7 @@ module Rzk.TypeCheck where import Control.Applicative ((<|>)) +import Control.Monad (when, forM, forM_, unless, join) import Control.Monad.Except import Control.Monad.Reader import Data.Bifunctor (first) From 85ee7501bbe86f375211e1c226d0b4068719413f Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:30:39 +0300 Subject: [PATCH 04/58] fix: update flake, refactor, add scripts --- default.nix | 10 +++++ flake.lock | 72 +++++++++++++++++++++++++++------ flake.nix | 99 ++++++++++++++++------------------------------ nix/ghcjs.nix | 77 ++++++++++++++++++++++++++++++++++++ nix/js-backend.nix | 79 ++++++++++++++++++++++++++++++++++++ nix/scripts.nix | 94 +++++++++++++++++++++++++++++++++++++++++++ nix/usual.nix | 27 +++++++++++++ rzk/rzk.nix | 32 --------------- shell.nix | 10 +++++ 9 files changed, 392 insertions(+), 108 deletions(-) create mode 100644 default.nix create mode 100644 nix/ghcjs.nix create mode 100644 nix/js-backend.nix create mode 100644 nix/scripts.nix create mode 100644 nix/usual.nix delete mode 100644 rzk/rzk.nix create mode 100644 shell.nix diff --git a/default.nix b/default.nix new file mode 100644 index 000000000..210377e4f --- /dev/null +++ b/default.nix @@ -0,0 +1,10 @@ +let t = (import + ( + let lock = builtins.fromJSON (builtins.readFile ./flake.lock); in + fetchTarball { + url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz"; + sha256 = lock.nodes.flake-compat.locked.narHash; + } + ) + { src = ./.; } +).defaultNix; in t // t.packages.${builtins.currentSystem} \ No newline at end of file diff --git a/flake.lock b/flake.lock index 2170d390e..8f9e48b36 100644 --- a/flake.lock +++ b/flake.lock @@ -1,15 +1,31 @@ { "nodes": { + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1673956053, + "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" }, "locked": { - "lastModified": 1681202837, - "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=", + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", "owner": "numtide", "repo": "flake-utils", - "rev": "cfacdce06f30d2b68473a46042957675eebb3401", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", "type": "github" }, "original": { @@ -18,43 +34,77 @@ "type": "github" } }, + "jsaddle": { + "flake": false, + "locked": { + "lastModified": 1694167118, + "narHash": "sha256-QNWimHH7c0xYe8sVmS2U3CgCR2q2fz2G35XTUywSrk8=", + "owner": "ghcjs", + "repo": "jsaddle", + "rev": "ffcda85943fd4b91a715643b921a10df9aba44e1", + "type": "github" + }, + "original": { + "owner": "ghcjs", + "repo": "jsaddle", + "type": "github" + } + }, "miso": { "flake": false, "locked": { - "lastModified": 1675453995, - "narHash": "sha256-rvNgA1ptB8UTBZMn1pjk6nN0CSNekF7oKc00SlpHX4I=", + "lastModified": 1691794309, + "narHash": "sha256-TQ6SRXDOit24jWnlNAh10FF5NQu8V6tbrY7ry56Cu7w=", "owner": "dmjio", "repo": "miso", - "rev": "5c66ed20818ce4aff81aaefbd5789007717923eb", + "rev": "49edf0677253bbcdd473422b5dd5b4beffd83910", "type": "github" }, "original": { "owner": "dmjio", "repo": "miso", - "rev": "5c66ed20818ce4aff81aaefbd5789007717923eb", + "rev": "49edf0677253bbcdd473422b5dd5b4beffd83910", + "type": "github" + } + }, + "nix-filter": { + "locked": { + "lastModified": 1694857738, + "narHash": "sha256-bxxNyLHjhu0N8T3REINXQ2ZkJco0ABFPn6PIe2QUfqo=", + "owner": "numtide", + "repo": "nix-filter", + "rev": "41fd48e00c22b4ced525af521ead8792402de0ea", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "nix-filter", "type": "github" } }, "nixpkgs": { "locked": { - "lastModified": 1684242266, - "narHash": "sha256-uaCQ2k1bmojHKjWQngvnnnxQJMY8zi1zq527HdWgQf8=", + "lastModified": 1694934517, + "narHash": "sha256-U9aI4/jw+kYTZye4LJC2eIU30SqvZgL/UeRY4VHIjK8=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "7e0743a5aea1dc755d4b761daf75b20aa486fdad", + "rev": "e1b4c97ed4ce160afd9ef1574b6a2ff168482f2a", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixpkgs-unstable", "repo": "nixpkgs", + "rev": "e1b4c97ed4ce160afd9ef1574b6a2ff168482f2a", "type": "github" } }, "root": { "inputs": { + "flake-compat": "flake-compat", "flake-utils": "flake-utils", + "jsaddle": "jsaddle", "miso": "miso", + "nix-filter": "nix-filter", "nixpkgs": "nixpkgs" } }, diff --git a/flake.nix b/flake.nix index 89ae38c2e..cd52fa436 100644 --- a/flake.nix +++ b/flake.nix @@ -1,9 +1,18 @@ { inputs = { flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; + nixpkgs.url = "github:NixOS/nixpkgs/e1b4c97ed4ce160afd9ef1574b6a2ff168482f2a"; miso = { - url = "github:dmjio/miso/5c66ed20818ce4aff81aaefbd5789007717923eb"; + url = "github:dmjio/miso/49edf0677253bbcdd473422b5dd5b4beffd83910"; + flake = false; + }; + flake-compat = { + url = "github:edolstra/flake-compat"; + flake = false; + }; + nix-filter.url = "github:numtide/nix-filter"; + jsaddle = { + url = "github:ghcjs/jsaddle"; flake = false; }; }; @@ -12,84 +21,44 @@ pkgs = inputs.nixpkgs.legacyPackages.${system}; rzk = "rzk"; - try-rzk = "try-rzk"; - ghcVersion = "ghc927"; - - # select a Haskell package set for a specified GHC version - hpkgs = pkgs.haskell.packages.${ghcVersion}; - - inherit (pkgs.haskell.lib) overrideCabal; - - # Provide overrides - # https://nixos.wiki/wiki/Haskell#Overrides - # An override should include a local package into the Haskell package set - override = { - overrides = self: super: { - ${rzk} = overrideCabal (self.callCabal2nix rzk ./${rzk} { }) (x: { - librarySystemDepends = [ pkgs.alex pkgs.happy ] ++ (x.librarySystemDepends or [ ]); - }); - ${try-rzk} = overrideCabal (self.callCabal2nix try-rzk ./${try-rzk} { }) (x: { - executableSystemDepends = [ self.ghcjs-prim self.ghcjs-base ] ++ (x.executableSystemDepends or [ ]); - }); - }; - }; - hpkgs_ = hpkgs.override override; - - # Get all dependencies of local Haskell packages excluding these local packages - # This approach is useful for cases when a local package A depends on a local package B - # In this case, package B won't be built by Nix as a dependency of A - getHaskellPackagesDeps = someHaskellPackages: let l = pkgs.lib.lists; in (l.subtractLists someHaskellPackages (l.concatLists (map (package: l.concatLists (__attrValues package.getCabalDeps)) someHaskellPackages))); - - # build a GHC with the dependencies of local Haskell packages - ghcForPackages = localHaskellPackageNames: hpkgs_.ghcWithPackages (ps: (getHaskellPackagesDeps (map (x: ps.${x}) localHaskellPackageNames) ++ [ ps.haskell-language-server ])); # Why provide HLS here - https://github.com/NixOS/nixpkgs/issues/225895#issuecomment-1509991742 + rzk-js = "rzk-js"; + ghcVersion = "ghc962"; + rzk-src = (inputs.nix-filter { + root = ./${rzk}; + include = [ "app" "src" "test" "package.yaml" ]; + }); + rzk-js-src = (inputs.nix-filter { + root = ./${rzk-js}; + include = [ "Main.hs" "${rzk-js}.cabal" ]; + }); - # GHC with dependencies of local Haskell packages - ghc = ghcForPackages [ rzk try-rzk ]; - - # tools that should be available in a development shell tools = [ pkgs.cabal-install pkgs.hpack - # haskell-language-server is already available as a GHC package - ghc + pkgs.nodejs_18 ]; - misoNix = (import "${inputs.miso.outPath}/default.nix" { inherit system; }); - pkgsMiso = misoNix.pkgs; - - # TODO add jsaddle version of the app - # https://github.com/dmjio/miso/tree/master/sample-app-jsaddle - # try-rzk-dev = - # let - # pkgsDev = pkgsMiso.haskell.packages.ghc865; - # rzk = pkgsDev.callPackage rzk/rzk.nix { inherit (pkgs) hpack; }; - # in - # pkgsDev.callCabal2nix try-rzk ./${try-rzk} { miso = misoNix.miso-jsaddle; rzk = rzk; }; + usual = import ./nix/usual.nix { inherit inputs pkgs rzk rzk-src ghcVersion tools; }; + ghcjs = import ./nix/ghcjs.nix { inherit inputs pkgs scripts rzk rzk-src rzk-js rzk-js-src ghcVersion tools; }; + scripts = import ./nix/scripts.nix { inherit pkgs packages; }; - try-rzk-exe = - let - pkgsRelease = pkgsMiso.haskell.packages.ghcjs; - rzk = pkgsRelease.callPackage rzk/rzk.nix { inherit (pkgs) hpack; }; - in - pkgsRelease.callCabal2nix try-rzk ./${try-rzk} { rzk = rzk; }; packages = { - rzk = hpkgs_.${rzk}; - try-rzk = try-rzk-exe; - }; + default = usual.packages.default; + rzk = usual.packages.${rzk}; + rzk-js = ghcjs.packages.${rzk-js}; + } // scripts; devShells = { - default = pkgs.mkShell { - shellHook = "export LANG=C.utf8"; - buildInputs = tools; + default = usual.devShells.default; + ghcjs = ghcjs.devShells.default; + release = pkgs.mkShell { + buildInputs = [ scripts.release-rzk-playground ]; }; - ghcjs = try-rzk-exe.env.overrideAttrs (old: { - buildInputs = old.buildInputs ++ [ pkgs.cabal-install pkgs.hpack ]; - }); }; in { - inherit packages devShells; + inherit packages devShells usual ghcjs; }); nixConfig = { diff --git a/nix/ghcjs.nix b/nix/ghcjs.nix new file mode 100644 index 000000000..f243e9511 --- /dev/null +++ b/nix/ghcjs.nix @@ -0,0 +1,77 @@ +{ inputs, pkgs, scripts, rzk, rzk-js, rzk-src, rzk-js-src, ghcVersion, tools }: +let + inherit (pkgs.haskell.lib) overrideCabal; + misoNix = (import "${inputs.miso.outPath}/default.nix" { inherit (pkgs) system; }); + pkgsMiso = misoNix.pkgs; + + hpkgs = + # This isn't equivalent to `pkgsMiso.haskell.packages.ghcjs.override` ([link](https://nixos.wiki/wiki/Haskell#Overrides)) + # but avoids multiple rebuilds + pkgsMiso.haskell.packages.ghcjs // + { + rzk = overrideCabal + (hpkgs.callCabal2nix rzk rzk-src { }) + (x: { + isLibrary = true; + isExecutable = false; + doCheck = false; + doHaddock = false; + libraryToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.libraryToolDepends or [ ]); + testToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.testToolDepends or [ ]); + prePatch = "hpack --force"; + }); + rzk-js = overrideCabal + (hpkgs.callCabal2nix rzk-js rzk-js-src { inherit (hpkgs) rzk; }) + (x: { + postInstall = (x.postInstall or "") + '' + cp $out/bin/${rzk-js} . + rm -r $out + cp ${rzk-js} $out + ''; + }); + }; + + hpkgsGHCJS_8_10_7 = pkgs.haskell.packages.ghcjs810.override ({ + overrides = final: prev: { + integer-gmp = final.integer-gmp_1_1; + rzk = overrideCabal + (final.callCabal2nix rzk rzk-src { }) + (x: { + isLibrary = true; + isExecutable = false; + doCheck = false; + doHaddock = false; + libraryToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.libraryToolDepends or [ ]); + testToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.testToolDepends or [ ]); + prePatch = "hpack --force"; + }); + rzk-js = overrideCabal + (final.callCabal2nix rzk-js rzk-js-src { inherit (final) rzk; }) + (x: { + postInstall = (x.postInstall or "") + '' + rm -r $out/bin/${rzk-js}.jsexe + ''; + }); + }; + }); + + packages = { + inherit (hpkgs) rzk rzk-js; + + # Currently not buildable + rzk_8_10_7 = hpkgsGHCJS_8_10_7.rzk; + rzk-js_8_10_7 = hpkgsGHCJS_8_10_7; + }; + + devShells = { + default = (hpkgs.shellFor { + packages = _: [ hpkgs.${rzk} hpkgs.${rzk-js} ]; + nativeBuildInputs = tools ++ [ scripts.build-rzk-js ]; + }).overrideAttrs (x: { + buildInputs = builtins.filter (p: (p.name or "") != "ghc-8.6.4") (x.buildInputs or [ ]); + }); + }; +in +{ + inherit hpkgs devShells packages hpkgsGHCJS_8_10_7; +} diff --git a/nix/js-backend.nix b/nix/js-backend.nix new file mode 100644 index 000000000..976d3d128 --- /dev/null +++ b/nix/js-backend.nix @@ -0,0 +1,79 @@ +# TODO fix builds with JS backend + +{ inputs, pkgs, rzk, rzk-js, rzk-src, rzk-js-src, ghcVersion, tools }: +let + inherit (pkgs.haskell.lib) overrideCabal; + overrideJS = { + overrides = self: super: { + jsaddle = super.callCabal2nix "jsaddle" "${inputs.jsaddle.outPath}/jsaddle" { }; + rzk = overrideCabal + (super.callCabal2nix rzk rzk-src { }) + (x: { + isLibrary = true; + isExecutable = false; + doCheck = false; + doHaddock = false; + libraryToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.libraryToolDepends or [ ]); + testToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.testToolDepends or [ ]); + prePatch = "hpack --force"; + }); + rzk-js = overrideCabal + (super.callCabal2nix rzk-js rzk-js-src { inherit (self) rzk; }) + (x: { + postInstall = (x.postInstall or "") + '' + rm -r $out/bin/${rzk-js}.jsexe + ''; + }); + }; + }; + hpkgs = pkgs.pkgsCross.ghcjs.buildPackages.haskell.packages.${ghcVersion}.override overrideJS; + + # Get all dependencies of local Haskell packages excluding these local packages + # This approach is useful for cases when a local package A depends on a local package B + # In this case, package B won't be built by Nix as a dependency of A + getHaskellPackagesDeps = someHaskellPackages: let l = pkgs.lib.lists; in (l.subtractLists someHaskellPackages (l.concatLists (map (package: l.concatLists (__attrValues package.getCabalDeps)) someHaskellPackages))); + # build a GHC with the dependencies of local Haskell packages + ghcForPackages = hpkgs_: localHaskellPackageNames: hpkgs_.ghcWithPackages (ps: (getHaskellPackagesDeps (map (x: ps.${x}) localHaskellPackageNames) ++ [ ps.haskell-language-server ])); # Why provide HLS here - https://github.com/NixOS/nixpkgs/issues/225895#issuecomment-1509991742 + + ghcWithPackages = ghcForPackages hpkgs [ rzk rzk-js ]; + + ghc = pkgs.pkgsCross.ghcjs.buildPackages.haskell.compiler.${ghcVersion}; + + packages = { + # TODO fix doesn't build .js + inherit (hpkgs) rzk rzk-js; + }; + + devShells = { + # This devshell provides a GHC compiler with packages that are dependencies of `rzk` and `rzk-js` + # It should be a GHC with a JS backend, but it's an ordinary GHC for some reason + + default = hpkgs.shellFor { + packages = ps: [ ps.rzk ps.${rzk-js} ]; + nativeBuildInputs = tools; + }; + + # This devshell provides a GHC compiler with packages that are dependencies of `rzk` and `rzk-js` + # It should be a GHC with a JS backend, but it's an ordinary GHC for some reason + + ghcWithPackages = pkgs.mkShell { + buildInputs = [ ghcWithPackages ] ++ tools; + }; + + # This devshell provides a GHC compiler with JS backend and without extra packages + + # GHC fails to build `rzk-js` + # cabal --with-compiler=javascript-unknown-ghcjs-ghc --with-ghc-pkg=javascript-unknown-ghcjs-ghc-pkg build rzk-js + ghcJS = pkgs.mkShell { + buildInputs = [ ghc ] ++ tools; + }; + + + # TODO incremental builds for ghc with js backend + # Incremental builds work for ghc 9.6+ + # https://github.com/NixOS/nixpkgs/blob/master/doc/languages-frameworks/haskell.section.md#incremental-builds-haskell-incremental-builds + }; +in +{ + inherit hpkgs devShells packages ghc ghcForPackages; +} diff --git a/nix/scripts.nix b/nix/scripts.nix new file mode 100644 index 000000000..46a11e057 --- /dev/null +++ b/nix/scripts.nix @@ -0,0 +1,94 @@ +{ pkgs, packages }: +let scripts = + { + build-rzk-js = pkgs.writeShellApplication { + name = "build-rzk-js"; + text = + let + public = "rzk-playground/public"; + result = "${public}/rzk-js"; + in + '' + cabal install rzk-js --ghcjs --installdir ${result} + rm -f ${public}/rzk.js + + cp ${result}/rzk-js ${public}/rzk.js + printf "Copied ${result}/rzk-js to ${public}/rzk.js\n" + + rm -rf ${result} + printf "Removed ${result}\n" + ''; + }; + + save-flake = pkgs.writeShellApplication { + name = "save-flake"; + runtimeInputs = [ pkgs.jq ]; + text = '' + # save flake inputs - # https://github.com/NixOS/nix/issues/4250#issuecomment-1146878407 + + mkdir -p "/nix/var/nix/gcroots/per-user/$USER" + + gc_root_prefix="/nix/var/nix/gcroots/per-user/$USER/$(systemd-escape -p "$PWD")-flake-" + echo "Adding per-user gcroots..." + rm -f "$gc_root_prefix"* + nix flake archive --json 2>/dev/null \ + | jq -r '.inputs | to_entries[] | "ln -fsT "+.value.path+" \"'"$gc_root_prefix"'"+.key+"\""' \ + | while read -r line; \ + do + eval "$line" + done + + # save scripts + + nix profile install --profile "$gc_root_prefix""${scripts.save-flake.name}" .#${scripts.save-flake.name} + nix profile install --profile "$gc_root_prefix""${scripts.release-rzk-playground.name}" .#${scripts.release-rzk-playground.name} + + printf "Entries saved with prefix %s\n" "$gc_root_prefix" + ''; + }; + + release-rzk-playground = pkgs.writeShellApplication { + name = "release-rzk-playground"; + runtimeInputs = [ pkgs.nodejs_18 packages.build-rzk-js ]; + text = + let + playground = "rzk-playground"; + playground-rzk-js = "${playground}/public/rzk.js"; + config = "next.config.js"; + configTmp = "${config}.tmp"; + configBackup = "${config}.bk"; + release = "rzk-playground-release"; + in + '' + rm -f ${playground-rzk-js} + cp ${packages.rzk-js} ${playground-rzk-js} + + ( + cd ${playground} + npm i + + # empty string by default + + : "''${BASEPATH:=""}" + + # substitute basepath in config + + < ${config} sed "s|'''|'$BASEPATH'|" > ${configTmp} + mv ${config} ${configBackup} + mv ${configTmp} ${config} + + # restore backup anyway + + npm run build || true + mv ${configBackup} ${config} + ) + + rm -rf ${release} + mkdir ${release} + cp -r ${playground}/out/* ${release} + + printf "Wrote release files to '${release}'\n" + ''; + }; + }; +in scripts diff --git a/nix/usual.nix b/nix/usual.nix new file mode 100644 index 000000000..3d0ef9001 --- /dev/null +++ b/nix/usual.nix @@ -0,0 +1,27 @@ +{ inputs, pkgs, ghcVersion, rzk, rzk-src, tools }: +let + inherit (pkgs.haskell.lib) overrideCabal; + # https://nixos.wiki/wiki/Haskell#Overrides + hpkgs = pkgs.haskell.packages.${ghcVersion}.override { + overrides = final: prev: { + ${rzk} = final.callCabal2nix rzk rzk-src { }; + }; + }; + + devShells = { + default = + hpkgs.shellFor { + shellHook = "export LANG=C.utf8"; + packages = ps: [ ps.rzk ]; + nativeBuildInputs = tools ++ [ hpkgs.haskell-language-server ]; + }; + }; + + packages = { + default = pkgs.haskell.lib.justStaticExecutables hpkgs.${rzk}; + rzk = hpkgs.${rzk}; + }; +in +{ + inherit hpkgs devShells packages; +} diff --git a/rzk/rzk.nix b/rzk/rzk.nix deleted file mode 100644 index 4d0b32d95..000000000 --- a/rzk/rzk.nix +++ /dev/null @@ -1,32 +0,0 @@ -{ mkDerivation, aeson, alex, array, base, bifunctors, bytestring -, data-default-class, doctest, filepath, Glob, happy, hpack, lens -, lib, mtl, optparse-generic, QuickCheck, stm, template-haskell -, text, yaml -}: -mkDerivation { - pname = "rzk"; - version = "0.6.2"; - src = ./.; - isLibrary = true; - isExecutable = true; - libraryHaskellDepends = [ - aeson array base bifunctors bytestring data-default-class filepath - Glob lens mtl optparse-generic stm template-haskell text yaml - ]; - libraryToolDepends = [ alex happy hpack ]; - executableHaskellDepends = [ - aeson array base bifunctors bytestring data-default-class filepath - Glob lens mtl optparse-generic stm template-haskell text yaml - ]; - executableToolDepends = [ alex happy ]; - testHaskellDepends = [ - aeson array base bifunctors bytestring data-default-class doctest - filepath Glob lens mtl optparse-generic QuickCheck stm - template-haskell text yaml - ]; - testToolDepends = [ alex happy ]; - prePatch = "hpack"; - homepage = "https://github.com/rzk-lang/rzk#readme"; - description = "An experimental proof assistant for synthetic ∞-categories"; - license = lib.licenses.bsd3; -} diff --git a/shell.nix b/shell.nix new file mode 100644 index 000000000..e479ab41d --- /dev/null +++ b/shell.nix @@ -0,0 +1,10 @@ +let t = (import + ( + let lock = builtins.fromJSON (builtins.readFile ./flake.lock); in + fetchTarball { + url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz"; + sha256 = lock.nodes.flake-compat.locked.narHash; + } + ) + { src = ./.; } +).shellNix; in t // t.devShells.${builtins.currentSystem} \ No newline at end of file From eb8f054c00425ab43b54b7b0754a5cf0dcf64a64 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:30:58 +0300 Subject: [PATCH 05/58] fix: package name try-rzk -> rzk-js --- cabal.project | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index eee6158d6..42f783dbd 100644 --- a/cabal.project +++ b/cabal.project @@ -1 +1 @@ -packages: rzk try-rzk \ No newline at end of file +packages: rzk rzk-js \ No newline at end of file From 1d48d547477dee31cfec13de504aed9ab3d6c293 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:31:22 +0300 Subject: [PATCH 06/58] fix: make direnv work without flakes --- .envrc | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/.envrc b/.envrc index 8ebe67ac3..bccbea9d7 100644 --- a/.envrc +++ b/.envrc @@ -1,2 +1,9 @@ -use flake -eval "$shellHook" \ No newline at end of file +if ! type "nix" > /dev/null; then + use nix -A default + eval "$shellHook" + use nix -A ghcjs +else + use flake .#default + eval "$shellHook" + use flake .#ghcjs +fi \ No newline at end of file From 205622d47af0ff70a4804c2ef637701b25b6d996 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:32:24 +0300 Subject: [PATCH 07/58] fix: update paths and scripts in the ghcjs action --- .github/workflows/ghcjs.yml | 56 +++++++++++++++++++++++++------------ 1 file changed, 38 insertions(+), 18 deletions(-) diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml index c4bd2d0f7..1b3cf17c3 100644 --- a/.github/workflows/ghcjs.yml +++ b/.github/workflows/ghcjs.yml @@ -7,14 +7,18 @@ on: paths: - .github/workflows/ghcjs.yml - rzk/** - - try-rzk/** + - rzk-js/** + - rzk-playground/** - stack.yaml + - '**/*.nix' pull_request: branches: [main, develop] paths: - rzk/** - - try-rzk/** + - rzk-js/** + - rzk-playground/** - stack.yaml + - '**/*.nix' workflow_dispatch: # allow triggering this workflow manually @@ -28,7 +32,7 @@ jobs: - name: πŸ“₯ Checkout repository uses: actions/checkout@v3 - - name: 🧰 Setup nix + - name: ❄️ Install Nix uses: nixbuild/nix-quick-install-action@v25 with: nix_conf: | @@ -36,38 +40,54 @@ jobs: 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 + - name: πŸ‘ Restore and Cache Nix store + uses: nix-community/cache-nix-action@v4 with: - key: ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml') }} + key: ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml', './rzk/rzk.cabal') }} restore-keys: | - ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml') }} + ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml', './rzk/rzk.cabal') }} ${{ runner.os }}-nix- + gc-linux: true + gc-max-store-size-linux: 7000000000 + purge: true + purge-created-max-age: 1209600 + + - name: πŸ‘ Restore and Cache NextJS cache + uses: actions/cache@v3 + with: + key: ${{ runner.os }}-next-${{ hashFiles('**/package-lock.json') }} + restore-keys: | + ${{ runner.os }}-next- + path: | + ~/.npm + rzk-playground/.next/cache - 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 - - name: πŸ”¨ Build GHCJS version with Nix - run: | - nix build .#try-rzk + # Uncomment to debug this job + # - name: Setup tmate session + # uses: mxschmitt/action-tmate@v3 - - name: πŸ”¨ Collect build artifacts + - name: πŸ”¨ Build Playground + env: + BASEPATH: /${{ github.event.repository.name }}/${{ github.ref_name }}/playground run: | - mkdir -p dist/result/bin - cp -r result/bin/try-rzk.jsexe/ dist/result/bin/. - chmod -R +w dist/ - cp try-rzk/index.html dist/. + nix run .#release-rzk-playground + + - name: πŸ”¨ Save flake from garbage collection + run: nix run .#save-flake - name: 'πŸš€ Publish JS "binaries" (${{ github.ref_name }})' if: ${{ github.ref_name != 'main' && github.event_name == 'push' }} uses: JamesIves/github-pages-deploy-action@v4 with: token: ${{ secrets.GITHUB_TOKEN }} - folder: dist + folder: rzk-playground-release target-folder: ${{ github.ref_name }}/playground - clean: false + clean: true single-commit: true - name: 'πŸš€ Publish JS "binaries"' @@ -75,7 +95,7 @@ jobs: uses: JamesIves/github-pages-deploy-action@v4 with: token: ${{ secrets.GITHUB_TOKEN }} - folder: dist + folder: rzk-playground-release target-folder: playground clean: false single-commit: true From ef2408e897ff9530ee648b78684252c5a6f7d9f9 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:32:39 +0300 Subject: [PATCH 08/58] add: gitignore artifacts --- .gitignore | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index e943c8b5b..27563190a 100644 --- a/.gitignore +++ b/.gitignore @@ -32,4 +32,5 @@ __pycache__ *.fdb_latexmk *.fls *.log -rzk/doc/ \ No newline at end of file +rzk/doc/ +/rzk-playground-release \ No newline at end of file From 143808fb5e30883703ef225788ecb296c7ce9caf Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:32:54 +0300 Subject: [PATCH 09/58] add: hls hie config --- hie.yaml | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 hie.yaml diff --git a/hie.yaml b/hie.yaml new file mode 100644 index 000000000..f0c7014d7 --- /dev/null +++ b/hie.yaml @@ -0,0 +1,2 @@ +cradle: + cabal: \ No newline at end of file From 54a9c18e87a94efd9ddf18e0ae71f11967aaed30 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 21:33:17 +0300 Subject: [PATCH 10/58] fix: format README, update development instructions --- README.md | 237 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 167 insertions(+), 70 deletions(-) diff --git a/README.md b/README.md index 1b4958718..6d80f9335 100644 --- a/README.md +++ b/README.md @@ -10,25 +10,27 @@ An experimental proof assistant for synthetic ∞-categories. ## About this project -This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://rzk-lang.github.io/rzk/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: https://github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda. `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma. +This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://rzk-lang.github.io/rzk/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: and . `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma. Internally, `rzk` uses a version of second-order abstract syntax allowing relatively straightforward handling of binders (such as lambda abstraction). In the future, `rzk` aims to support dependent type inference relying on E-unification for second-order abstract syntax [2]. Using such representation is motivated by automatic handling of binders and easily automated boilerplate code. The idea is that this should keep the implementation of `rzk` relatively small and less error-prone than some of the existing approaches to implementation of dependent type checkers. -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 https://github.com/fizruk/simple-topes. `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. +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. ## How to use `rzk` -For relatively small single-file formalisations, you can use the online playground at https://rzk-lang.github.io/rzk/playground.html +For relatively small single-file formalisations, you can use the online playground at However, for larger and multi-file formalisations you should install a version of `rzk` locally: - You can install the latest "stable" version of `rzk` from Hackage: + ```sh cabal install rzk ``` - You can install the latest "development" version of `rzk` from the [`develop` branch](https://github.com/rzk-lang/rzk/tree/develop) of this repository: + ```sh git clone https://github.com/rzk-lang/rzk.git cd rzk @@ -50,7 +52,7 @@ rzk typecheck first.rzk second.rzk third.rzk A proper support for inter-file dependencies will be implemented in the future. Until then, it is recommented to start names of files with a number, ensuring correct order when using a wildcard (`*`). For example: -``` +```console . β”œβ”€β”€ 0-common.md β”œβ”€β”€ 1-paths.md @@ -85,21 +87,21 @@ Now, you can build and serve the documentation locally by running mkdocs serve --config-file docs/mkdocs.yml ``` -The (locally built) documentation should be available at http://127.0.0.1:8000 +The (locally built) documentation should be available at The pages of the documentation are the `*.md` files in [docs/docs](docs/docs) directory and its subdirectories. To add a new page, you can create a new `*.md` file and add it to the navigation by modifying [docs/mkdocs.yml](docs/mkdocs.yml). -### Development +## Development -The project is developed with both Stack and Nix (for GHCJS version). +The project is developed with both [stack](https://docs.haskellstack.org/en/stable/README/) and [nix](https://nixos.org/manual/nix/unstable/introduction). -#### Building with GHC +## Develop `rzk` with stack -For quick local development and testing it is recommended to work with a GHC version, using [Stack tool](https://docs.haskellstack.org/en/stable/README/). Clone this project and simply run `stack build`: +For quick local development and testing it is recommended to work with a GHC version, using the `stack` tool. Clone this project and run `stack build`: ```sh -git clone git@github.com:rzk-lang/rzk.git +git clone https://github.com/rzk-lang/rzk.git cd rzk stack build ``` @@ -110,96 +112,191 @@ The build provides an executable `rzk` which can be used to typecheck files: stack exec -- rzk typecheck FILE ``` -#### Building with GHCJS +## Develop with `nix` -`try-rzk` package is designed to be compiled using GHCJS for an in-browser version of the proof assistant. To build this package you need to use Nix. It is recommended that you use Cachix to avoid recompiling lots of dependencies: +1. Install `nix`: -```sh -# Install Nix -curl https://nixos.org/nix/install | sh -# (optionally) Install Cachix -nix-env -iA cachix -f https://cachix.org/api/v1/install -# (optionally) Use cached miso from Cachix -cachix use miso-haskell + ```console + sh <(curl -L https://nixos.org/nix/install) --no-daemon + ``` + +2. (Optionally) Permanently [enable nix flakes](https://nixos.wiki/wiki/Flakes#Permanent) to use faster and more convenient experimental (but quite stable) commands. +3. Use `cachix` to avoid building multiple dependencies: + 1. Without flakes: `nix-shell -p cachix --command 'cachix use miso-haskell'` + 2. With flakes: `nix shell nixpkgs#cachix -c cachix use miso-haskell` +4. (Optionally) Install [direnv](https://direnv.net/#basic-installation) to start the `devShell` when you enter the repository directory. + 1. The `nix-direnv` repo shows [installation options](https://github.com/nix-community/nix-direnv#installation). +5. (Optionally) If you use VS Code, you can install `mkhl.direnv` extension that loads `direnv` environments. + +6. Clone this repository and enter it + + ```console + git clone git@github.com:rzk-lang/rzk.git + cd rzk + ``` + +7. Run `direnv allow` in the repository root. +8. Use `cabal` for development. + - `cabal` performs incremental builds meaning it will build only the parts that are changed. This is quite fast. + - `nix` will rebuild the package `A` when its dependency `B` changes. Moreover, `nix` will rebuild all packages that are dependencies of `A` and that depend on `B`. This is much slower than incremental builds. + - So, use `nix` for setting up the environment with necessary tools that don't need rebuilds. +9. The following sections provide commands to build and run packages. They should be executed from the root directory of this repository. +10. The commands `nix-shell`, `nix shell`, and `nix develop` start shells with necessary tools. + Run subsequent commands from code blocks in these shells. + +## Permanently install `rzk` + +### without flakes + +```console +nix-env -iA default -f default.nix +rzk version ``` -Clone the repository, enter `try-rzk` directory and use `nix-build`: -```sh -git clone git@github.com:rzk-lang/rzk.git -cd rzk/try-rzk -nix-build +### with flakes + +```console +nix profile install +rzk version ``` -Now open `playground.html` to see the result. Note that if local GHCJS build is unavailable, `playground.html` will use the [JS file from GitHub Pages](https://rzk-lang.github.io/rzk/v0.1.0/result/bin/try-rzk.jsexe/all.js) as a fallback. +Also see [nix profile remove](https://nixos.org/manual/nix/unstable/command-ref/new-cli/nix3-profile-remove). -##### Flake +## Develop `rzk` -The flake in this repository allows to build `try-rzk` incrementally and reproducibly. +`nix-shell` and `nix develop` start shells with `cabal`, `ghc` with packages, `hpack`, `haskell-language-server`. -1. Install `Nix` via single-user [installation](https://nixos.org/download.html#download-nix): +### without flakes - 1. Run script +#### `cabal` - ```sh - sh <(curl -L https://nixos.org/nix/install) --no-daemon - ``` +```console +nix-shell -A default +# (Optionally) build +cabal build rzk +cabal run rzk -- version +``` - 1. Permanently [enable](https://nixos.wiki/wiki/Flakes#Permanent) flakes +#### `nix-build` -1. Enter the `devShell` with `GHC` (not `GHCJS`). Answer `y` to `Nix` prompts to use binary caches. +```console +nix-build -A default +./result/bin/rzk version +``` - ```sh - nix develop - ``` +### with flakes -1. The shell provides `ghc`, `haskell-language-server`, `cabal-install`, `hpack`. +#### `cabal` -1. (Optionally) Install [direnv](https://direnv.net/) to start the `devShell` when you enter the repository directory. +```console +nix develop +# (Optionally) build +cabal build rzk +cabal run rzk -- version +``` -1. Build `rzk`. +#### `nix build` - ```sh - cabal build - ``` +```console +nix build +./result/bin/rzk version +``` -1. Enter the `devShell` with `GHCJS`. +#### `nix run` - ```sh - nix develop .#ghcjs - ``` +```console +nix run .# -- version +``` -1. Build `try-rzk`. This may require ~10 GB of RAM. +#### `nix shell` - ```sh - cabal build --ghcjs - ``` +```console +nix shell +rzk version +``` -1. (Optionally) Build `rzk` via `Nix`. The resulting executable will be in `result/bin/rzk`. +## Build `rzk-js` - ```sh - nix build .#rzk - ``` +[rzk-js](./rzk-js/) is a wrapper around `rzk`. +Building `rzk-js` via `GHCJS` produces a `JavaScript` script used in `rzk-playground`. -1. (Optionally) Run `rzk` via `Nix`. +### without flakes - ```sh - nix run .#rzk - ``` +#### `cabal` + +```console +nix-shell -A ghcjs +build-rzk-js +``` -1. (Optionally) Build `try-rzk` via `Nix`. This may require ~10 GB of RAM. The resulting executable will be in `try-rzk/result/bin/try-rzk.jsexe`. +#### `nix-build` - ```sh - nix build .#try-rzk --out-link try-rzk/result - ``` +```console +rm -rf rzk-playground/public/rzk.js +nix-build -A rzk-js -o rzk-playground/public/rzk.js +``` -1. Open the app in a browser. +### with flakes - ```sh - firefox try-rzk/playground.html - ``` +#### `cabal` + +```console +nix develop .#ghcjs +build-rzk-js +``` + +#### `nix build` + +```console +rm -rf rzk-playground/public/rzk.js +nix build .#rzk-js -o rzk-playground/public/rzk.js +``` + +## `rzk-playground` + +[rzk-playground](./rzk-playground/) is a `JavaScript` application that combines an editor and basic `rzk` functionality. + +### Develop + +1. Load `nodejs` + - without flakes: `nix-shell` + - with flakes: `nix develop` + +1. Start a development server and open in a browser a link given by the server. + + ```console + cd rzk-playground + npm run dev + ``` + +### Release + +Build a static site to be hosted, e.g., on `GitHub Pages`. +The `release-rzk-playground` script will write files to the `rzk-playground-release` directory. + +#### without flakes + +```console +nix-shell -A release +release-rzk-playground +``` + +#### with flakes + +##### `nix develop` + +```console +nix develop .#release +release-rzk-playground +``` + +##### `nix run` + +```console +nix run .#release-rzk-playground +``` ## References -1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442 -2. Nikolai Kudasov. E-unification for Second-Order Abstract Syntax. 2023. https://arxiv.org/abs/2302.05815 - +1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. +2. Nikolai Kudasov. E-unification for Second-Order Abstract Syntax. 2023. From 91a5302acac6001bc3aaffadde919c8f00be5d73 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Mon, 25 Sep 2023 22:04:11 +0300 Subject: [PATCH 11/58] fix: create parent dir for rzk.js --- nix/scripts.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/nix/scripts.nix b/nix/scripts.nix index 46a11e057..8687cd2a4 100644 --- a/nix/scripts.nix +++ b/nix/scripts.nix @@ -61,6 +61,7 @@ let scripts = in '' rm -f ${playground-rzk-js} + mkdir -p "$(dirname ${playground-rzk-js})" cp ${packages.rzk-js} ${playground-rzk-js} ( From bd99bf4bbe9db7ba16fa5998c33972317ecdffd3 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Tue, 26 Sep 2023 02:21:27 +0300 Subject: [PATCH 12/58] fix: scrolling - now I resize the output panel since it's cheaper than resizing the editor. --- rzk-playground/app/globals.css | 8 --- rzk-playground/app/page.tsx | 61 ++++++++----------- rzk-playground/components/editor/Editor.tsx | 33 ++++++---- .../components/editor/cursor-height.ts | 27 ++++++++ 4 files changed, 74 insertions(+), 55 deletions(-) create mode 100644 rzk-playground/components/editor/cursor-height.ts diff --git a/rzk-playground/app/globals.css b/rzk-playground/app/globals.css index 114c45fc9..0059a118c 100644 --- a/rzk-playground/app/globals.css +++ b/rzk-playground/app/globals.css @@ -21,14 +21,6 @@ body { width: 100%; } -#__codemirror__ { - font-family: Inconsolata, monospace; -} - -#__app__ { - margin: 20px; -} - /* CSS for response button from https://getcssscan.com/css-buttons-examples (button 61) */ #btnTypecheck { align-items: center; diff --git a/rzk-playground/app/page.tsx b/rzk-playground/app/page.tsx index a709af66c..8e60dff1c 100644 --- a/rzk-playground/app/page.tsx +++ b/rzk-playground/app/page.tsx @@ -5,18 +5,10 @@ import Editor from '../components/editor/Editor'; import Script from 'next/script'; import { Resizable } from 're-resizable'; import React from 'react'; -import { color } from '../components/editor/theme'; import * as rzk from '../src/rzk'; import { KeyBindProvider, ShortcutType } from 'react-keybinds'; import dynamic from 'next/dynamic'; -const style = { - display: "flex", - alignItems: "center", - justifyContent: "center", - background: color.background -} - var typecheckedOnStart = false declare var window: Window & typeof globalThis; @@ -25,7 +17,6 @@ function HomeNoSSR() { const [message, setMessage] = useState("Starting..."); const [windowHeight, setWindowHeight] = useState(window.innerHeight) - const [editorHeight, setHeight] = React.useState(windowHeight * 70 / 100) const [needTypecheck, setNeedTypecheck] = useState(false) useEffect(() => { @@ -91,39 +82,39 @@ function HomeNoSSR() { ] ; + const [outputHeight, setOutputHeight] = useState(windowHeight * 30 / 100) + return (