diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml index 391d65630..b45b88c16 100644 --- a/.github/workflows/ghcjs.yml +++ b/.github/workflows/ghcjs.yml @@ -32,7 +32,7 @@ jobs: runs-on: ubuntu-latest steps: - name: ๐Ÿ“ฅ Checkout repository - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: โ„๏ธ Install Nix uses: nixbuild/nix-quick-install-action@v25 @@ -43,26 +43,26 @@ jobs: keep-outputs = true - name: ๐Ÿ‘ Restore and Cache Nix store - uses: nix-community/cache-nix-action@v4 + uses: nix-community/cache-nix-action@v5 with: - key: ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml', './rzk/rzk.cabal') }} - restore-keys: | + primary-key: ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml', './rzk/rzk.cabal') }} + restore-prefixes-first-match: | ${{ 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 + gc-max-store-size: 7000000000 purge: true - purge-created-max-age: 1209600 + purge-prefixes: ${{ runner.os }}-nix- + purge-created: 0 + purge-primary-key: never - - name: ๐Ÿ‘ Restore and Cache NextJS cache - uses: actions/cache@v3 + - name: ๐Ÿ‘ Restore and cache NodeJS deps + uses: actions/cache@v4 with: - key: ${{ runner.os }}-next-${{ hashFiles('**/package-lock.json') }} + key: ${{ runner.os }}-node-${{ hashFiles('**/package-lock.json') }} restore-keys: | - ${{ runner.os }}-next- + ${{ runner.os }}-node- path: | ~/.npm - rzk-playground/.next/cache - name: ๐Ÿ”จ Remove lexer and parser generator files run: | @@ -76,8 +76,7 @@ jobs: - name: ๐Ÿ”จ Build Playground env: ASSET_URL: /${{ github.event.repository.name }}/${{ github.ref_name }}/playground - run: | - nix run .#release-rzk-playground + run: nix run .#release-rzk-playground - name: ๐Ÿ”จ Save flake from garbage collection run: nix run .#save-flake diff --git a/CITATION.cff b/CITATION.cff index e7fea8dc0..6b01db532 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -8,5 +8,5 @@ authors: - family-names: Danko given-names: Danila title: "Rzk: a proof assistant for synthetic $\\infty$-categories" -version: 0.7.3 +version: 0.7.4 url: "https://github.com/rzk-lang/rzk" diff --git a/docs/config/en/mkdocs.yml b/docs/config/en/mkdocs.yml index 71b0200f2..32f44759b 100644 --- a/docs/config/en/mkdocs.yml +++ b/docs/config/en/mkdocs.yml @@ -19,7 +19,7 @@ nav: - getting-started/index.md - Install: getting-started/install.md - Quickstart: getting-started/quickstart.rzk.md - - Depedent Types: getting-started/dependent-types.rzk.md + - Dependent Types: getting-started/dependent-types.rzk.md - Setting up an Rzk project: getting-started/project.md - Reference: - Introduction: reference/introduction.rzk.md diff --git a/rzk-playground/README.md b/rzk-playground/README.md index c4033664f..0d6babedd 100644 --- a/rzk-playground/README.md +++ b/rzk-playground/README.md @@ -1,36 +1,30 @@ -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). +# React + TypeScript + Vite -## Getting Started +This template provides a minimal setup to get React working in Vite with HMR and some ESLint rules. -First, run the development server: +Currently, two official plugins are available: -```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. +- [@vitejs/plugin-react](https://github.com/vitejs/vite-plugin-react/blob/main/packages/plugin-react/README.md) uses [Babel](https://babeljs.io/) for Fast Refresh +- [@vitejs/plugin-react-swc](https://github.com/vitejs/vite-plugin-react-swc) uses [SWC](https://swc.rs/) for Fast Refresh -## Learn More +## Expanding the ESLint configuration -To learn more about Next.js, take a look at the following resources: +If you are developing a production application, we recommend updating the configuration to enable type aware lint rules: -- [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. +- Configure the top-level `parserOptions` property like this: -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. +```js +export default { + // other rules... + parserOptions: { + ecmaVersion: 'latest', + sourceType: 'module', + project: ['./tsconfig.json', './tsconfig.node.json'], + tsconfigRootDir: __dirname, + }, +} +``` -Check out our [Next.js deployment documentation](https://nextjs.org/docs/deployment) for more details. +- Replace `plugin:@typescript-eslint/recommended` to `plugin:@typescript-eslint/recommended-type-checked` or `plugin:@typescript-eslint/strict-type-checked` +- Optionally add `plugin:@typescript-eslint/stylistic-type-checked` +- Install [eslint-plugin-react](https://github.com/jsx-eslint/eslint-plugin-react) and add `plugin:react/recommended` & `plugin:react/jsx-runtime` to the `extends` list diff --git a/rzk-playground/package-lock.json b/rzk-playground/package-lock.json index b1e36441c..e316748c0 100644 --- a/rzk-playground/package-lock.json +++ b/rzk-playground/package-lock.json @@ -140,6 +140,22 @@ "w3c-keyname": "^2.2.4" } }, + "node_modules/@esbuild/aix-ppc64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/aix-ppc64/-/aix-ppc64-0.19.12.tgz", + "integrity": "sha512-bmoCYyWdEL3wDQIVbcyzRyeKLgk2WtWLTWz1ZIAZF/EGbNOwSA6ew3PftJ1PqMiOOGu0OyFMzG53L0zqIpPeNA==", + "cpu": [ + "ppc64" + ], + "dev": true, + "optional": true, + "os": [ + "aix" + ], + "engines": { + "node": ">=12" + } + }, "node_modules/@esbuild/android-arm": { "version": "0.18.20", "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.18.20.tgz", @@ -597,11 +613,10 @@ "integrity": "sha512-XPIN3cYDXsoJI/oDWoR2tD++juVrhgIago9xyKhZ7IhGlzdDM9QgC8D8saKNCz5pindGcznFr2HBSsEQSWnSjw==" }, "node_modules/@lezer/generator": { - "version": "1.5.1", - "resolved": "git+ssh://git@github.com/deemp/generator.git#cc38c10ab0d9d6e9b0e6daf1659e7a15dad86649", - "integrity": "sha512-r2wTPQgpGKFSMyRo7hAa8PaSg3XVcmkX7PCnSWlXoK4d3Y6ZHTNbLD1cdczmrO1D+fLPMimtIcjgYiXQKnVRHQ==", + "version": "1.7.0", + "resolved": "https://registry.npmjs.org/@lezer/generator/-/generator-1.7.0.tgz", + "integrity": "sha512-IJ16tx3biLKlCXUzcK4v8S10AVa2BSM2rB12rtAL6f1hL2TS/HQQlGCoWRvanlL2J4mCYEEIv9uG7n4kVMkVDA==", "dev": true, - "license": "MIT", "dependencies": { "@lezer/common": "^1.1.0", "@lezer/lr": "^1.3.0" @@ -619,9 +634,9 @@ } }, "node_modules/@lezer/lr": { - "version": "1.3.12", - "resolved": "https://registry.npmjs.org/@lezer/lr/-/lr-1.3.12.tgz", - "integrity": "sha512-5nwY1JzCueUdRtlMBnlf1SUi69iGCq2ABq7WQFQMkn/kxPvoACAEnTp4P17CtXxYr7WCwtYPLL2AEvxKPuF1OQ==", + "version": "1.4.0", + "resolved": "https://registry.npmjs.org/@lezer/lr/-/lr-1.4.0.tgz", + "integrity": "sha512-Wst46p51km8gH0ZUmeNrtpRYmdlRHUpN1DQd3GFAyKANi8WVz8c2jHYTf1CVScFaCjQw1iO3ZZdqGDxQPRErTg==", "dependencies": { "@lezer/common": "^1.0.0" } @@ -910,10 +925,13 @@ "dev": true }, "node_modules/@types/node": { - "version": "20.6.3", - "resolved": "https://registry.npmjs.org/@types/node/-/node-20.6.3.tgz", - "integrity": "sha512-HksnYH4Ljr4VQgEy2lTStbCKv/P590tmPe5HqOnv9Gprffgv5WXAY+Y5Gqniu0GGqeTCUdBnzC3QSrzPkBkAMA==", - "dev": true + "version": "20.12.2", + "resolved": "https://registry.npmjs.org/@types/node/-/node-20.12.2.tgz", + "integrity": "sha512-zQ0NYO87hyN6Xrclcqp7f8ZbXNbRfoGWNcMvHTPQp9UUrwI0mI7XBz+cu7/W6/VClYo2g63B0cjull/srU7LgQ==", + "dev": true, + "dependencies": { + "undici-types": "~5.26.4" + } }, "node_modules/@types/prop-types": { "version": "15.7.6", @@ -1665,12 +1683,6 @@ "node": ">=8" } }, - "node_modules/buffer-from": { - "version": "1.1.2", - "resolved": "https://registry.npmjs.org/buffer-from/-/buffer-from-1.1.2.tgz", - "integrity": "sha512-E+XQCRwSbaaiChtv6k6Dwgc+bx+Bs6vuKJHHl5kox/BaKbhiXzqQOwK4cO22yElGp2OCmjwVhT3HmxgyPGnJfQ==", - "dev": true - }, "node_modules/call-bind": { "version": "1.0.2", "resolved": "https://registry.npmjs.org/call-bind/-/call-bind-1.0.2.tgz", @@ -4148,15 +4160,6 @@ "node": ">=8" } }, - "node_modules/source-map": { - "version": "0.6.1", - "resolved": "https://registry.npmjs.org/source-map/-/source-map-0.6.1.tgz", - "integrity": "sha512-UjgapumWlbMhkBgzT7Ykc5YXUT46F0iKu8SGXq0bcwP5dz/h0Plj6enJqjz1Zbq2l5WaqYnrVbwWOWMyF3F47g==", - "dev": true, - "engines": { - "node": ">=0.10.0" - } - }, "node_modules/source-map-js": { "version": "1.0.2", "resolved": "https://registry.npmjs.org/source-map-js/-/source-map-js-1.0.2.tgz", @@ -4166,16 +4169,6 @@ "node": ">=0.10.0" } }, - "node_modules/source-map-support": { - "version": "0.5.21", - "resolved": "https://registry.npmjs.org/source-map-support/-/source-map-support-0.5.21.tgz", - "integrity": "sha512-uBHU3L3czsIyYXKX88fdrGovxdSCoTGDRZ6SYXtSRxLZUzHg5P/66Ht6uoUlHu9EZod+inXhKo3qQgwXUT/y1w==", - "dev": true, - "dependencies": { - "buffer-from": "^1.0.0", - "source-map": "^0.6.0" - } - }, "node_modules/string.prototype.matchall": { "version": "4.0.10", "resolved": "https://registry.npmjs.org/string.prototype.matchall/-/string.prototype.matchall-4.0.10.tgz", @@ -4363,22 +4356,414 @@ "peer": true }, "node_modules/tsx": { - "version": "3.13.0", - "resolved": "https://registry.npmjs.org/tsx/-/tsx-3.13.0.tgz", - "integrity": "sha512-rjmRpTu3as/5fjNq/kOkOtihgLxuIz6pbKdj9xwP4J5jOLkBxw/rjN5ANw+KyrrOXV5uB7HC8+SrrSJxT65y+A==", + "version": "4.7.1", + "resolved": "https://registry.npmjs.org/tsx/-/tsx-4.7.1.tgz", + "integrity": "sha512-8d6VuibXHtlN5E3zFkgY8u4DX7Y3Z27zvvPKVmLon/D4AjuKzarkUBTLDBgj9iTQ0hg5xM7c/mYiRVM+HETf0g==", "dev": true, "dependencies": { - "esbuild": "~0.18.20", - "get-tsconfig": "^4.7.2", - "source-map-support": "^0.5.21" + "esbuild": "~0.19.10", + "get-tsconfig": "^4.7.2" }, "bin": { "tsx": "dist/cli.mjs" }, + "engines": { + "node": ">=18.0.0" + }, "optionalDependencies": { "fsevents": "~2.3.3" } }, + "node_modules/tsx/node_modules/@esbuild/android-arm": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.19.12.tgz", + "integrity": "sha512-qg/Lj1mu3CdQlDEEiWrlC4eaPZ1KztwGJ9B6J+/6G+/4ewxJg7gqj8eVYWvao1bXrqGiW2rsBZFSX3q2lcW05w==", + "cpu": [ + "arm" + ], + "dev": true, + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/android-arm64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.19.12.tgz", + "integrity": "sha512-P0UVNGIienjZv3f5zq0DP3Nt2IE/3plFzuaS96vihvD0Hd6H/q4WXUGpCxD/E8YrSXfNyRPbpTq+T8ZQioSuPA==", + "cpu": [ + "arm64" + ], + "dev": true, + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/android-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.19.12.tgz", + "integrity": "sha512-3k7ZoUW6Q6YqhdhIaq/WZ7HwBpnFBlW905Fa4s4qWJyiNOgT1dOqDiVAQFwBH7gBRZr17gLrlFCRzF6jFh7Kew==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/darwin-arm64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.19.12.tgz", + "integrity": "sha512-B6IeSgZgtEzGC42jsI+YYu9Z3HKRxp8ZT3cqhvliEHovq8HSX2YX8lNocDn79gCKJXOSaEot9MVYky7AKjCs8g==", + "cpu": [ + "arm64" + ], + "dev": true, + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/darwin-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.19.12.tgz", + "integrity": "sha512-hKoVkKzFiToTgn+41qGhsUJXFlIjxI/jSYeZf3ugemDYZldIXIxhvwN6erJGlX4t5h417iFuheZ7l+YVn05N3A==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/freebsd-arm64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.19.12.tgz", + "integrity": "sha512-4aRvFIXmwAcDBw9AueDQ2YnGmz5L6obe5kmPT8Vd+/+x/JMVKCgdcRwH6APrbpNXsPz+K653Qg8HB/oXvXVukA==", + "cpu": [ + "arm64" + ], + "dev": true, + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/freebsd-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.19.12.tgz", + "integrity": "sha512-EYoXZ4d8xtBoVN7CEwWY2IN4ho76xjYXqSXMNccFSx2lgqOG/1TBPW0yPx1bJZk94qu3tX0fycJeeQsKovA8gg==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-arm": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.19.12.tgz", + "integrity": "sha512-J5jPms//KhSNv+LO1S1TX1UWp1ucM6N6XuL6ITdKWElCu8wXP72l9MM0zDTzzeikVyqFE6U8YAV9/tFyj0ti+w==", + "cpu": [ + "arm" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-arm64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.19.12.tgz", + "integrity": "sha512-EoTjyYyLuVPfdPLsGVVVC8a0p1BFFvtpQDB/YLEhaXyf/5bczaGeN15QkR+O4S5LeJ92Tqotve7i1jn35qwvdA==", + "cpu": [ + "arm64" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-ia32": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.19.12.tgz", + "integrity": "sha512-Thsa42rrP1+UIGaWz47uydHSBOgTUnwBwNq59khgIwktK6x60Hivfbux9iNR0eHCHzOLjLMLfUMLCypBkZXMHA==", + "cpu": [ + "ia32" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-loong64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.19.12.tgz", + "integrity": "sha512-LiXdXA0s3IqRRjm6rV6XaWATScKAXjI4R4LoDlvO7+yQqFdlr1Bax62sRwkVvRIrwXxvtYEHHI4dm50jAXkuAA==", + "cpu": [ + "loong64" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-mips64el": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.19.12.tgz", + "integrity": "sha512-fEnAuj5VGTanfJ07ff0gOA6IPsvrVHLVb6Lyd1g2/ed67oU1eFzL0r9WL7ZzscD+/N6i3dWumGE1Un4f7Amf+w==", + "cpu": [ + "mips64el" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-ppc64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.19.12.tgz", + "integrity": "sha512-nYJA2/QPimDQOh1rKWedNOe3Gfc8PabU7HT3iXWtNUbRzXS9+vgB0Fjaqr//XNbd82mCxHzik2qotuI89cfixg==", + "cpu": [ + "ppc64" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-riscv64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.19.12.tgz", + "integrity": "sha512-2MueBrlPQCw5dVJJpQdUYgeqIzDQgw3QtiAHUC4RBz9FXPrskyyU3VI1hw7C0BSKB9OduwSJ79FTCqtGMWqJHg==", + "cpu": [ + "riscv64" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-s390x": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.19.12.tgz", + "integrity": "sha512-+Pil1Nv3Umes4m3AZKqA2anfhJiVmNCYkPchwFJNEJN5QxmTs1uzyy4TvmDrCRNT2ApwSari7ZIgrPeUx4UZDg==", + "cpu": [ + "s390x" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.19.12.tgz", + "integrity": "sha512-B71g1QpxfwBvNrfyJdVDexenDIt1CiDN1TIXLbhOw0KhJzE78KIFGX6OJ9MrtC0oOqMWf+0xop4qEU8JrJTwCg==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/netbsd-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.19.12.tgz", + "integrity": "sha512-3ltjQ7n1owJgFbuC61Oj++XhtzmymoCihNFgT84UAmJnxJfm4sYCiSLTXZtE00VWYpPMYc+ZQmB6xbSdVh0JWA==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/openbsd-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.19.12.tgz", + "integrity": "sha512-RbrfTB9SWsr0kWmb9srfF+L933uMDdu9BIzdA7os2t0TXhCRjrQyCeOt6wVxr79CKD4c+p+YhCj31HBkYcXebw==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/sunos-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.19.12.tgz", + "integrity": "sha512-HKjJwRrW8uWtCQnQOz9qcU3mUZhTUQvi56Q8DPTLLB+DawoiQdjsYq+j+D3s9I8VFtDr+F9CjgXKKC4ss89IeA==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "sunos" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/win32-arm64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.19.12.tgz", + "integrity": "sha512-URgtR1dJnmGvX864pn1B2YUYNzjmXkuJOIqG2HdU62MVS4EHpU2946OZoTMnRUHklGtJdJZ33QfzdjGACXhn1A==", + "cpu": [ + "arm64" + ], + "dev": true, + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/win32-ia32": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.19.12.tgz", + "integrity": "sha512-+ZOE6pUkMOJfmxmBZElNOx72NKpIa/HFOMGzu8fqzQJ5kgf6aTGrcJaFsNiVMH4JKpMipyK+7k0n2UXN7a8YKQ==", + "cpu": [ + "ia32" + ], + "dev": true, + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/@esbuild/win32-x64": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.19.12.tgz", + "integrity": "sha512-T1QyPSDCyMXaO3pzBkF96E8xMkiRYbUEZADd29SyPGabqxMViNoii+NcK7eWJAEoU6RZyEm5lVSIjTmcdoB9HA==", + "cpu": [ + "x64" + ], + "dev": true, + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=12" + } + }, + "node_modules/tsx/node_modules/esbuild": { + "version": "0.19.12", + "resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.19.12.tgz", + "integrity": "sha512-aARqgq8roFBj054KvQr5f1sFu0D65G+miZRCuJyJ0G13Zwx7vRar5Zhn2tkQNzIXcBrNVsv/8stehpj+GAjgbg==", + "dev": true, + "hasInstallScript": true, + "bin": { + "esbuild": "bin/esbuild" + }, + "engines": { + "node": ">=12" + }, + "optionalDependencies": { + "@esbuild/aix-ppc64": "0.19.12", + "@esbuild/android-arm": "0.19.12", + "@esbuild/android-arm64": "0.19.12", + "@esbuild/android-x64": "0.19.12", + "@esbuild/darwin-arm64": "0.19.12", + "@esbuild/darwin-x64": "0.19.12", + "@esbuild/freebsd-arm64": "0.19.12", + "@esbuild/freebsd-x64": "0.19.12", + "@esbuild/linux-arm": "0.19.12", + "@esbuild/linux-arm64": "0.19.12", + "@esbuild/linux-ia32": "0.19.12", + "@esbuild/linux-loong64": "0.19.12", + "@esbuild/linux-mips64el": "0.19.12", + "@esbuild/linux-ppc64": "0.19.12", + "@esbuild/linux-riscv64": "0.19.12", + "@esbuild/linux-s390x": "0.19.12", + "@esbuild/linux-x64": "0.19.12", + "@esbuild/netbsd-x64": "0.19.12", + "@esbuild/openbsd-x64": "0.19.12", + "@esbuild/sunos-x64": "0.19.12", + "@esbuild/win32-arm64": "0.19.12", + "@esbuild/win32-ia32": "0.19.12", + "@esbuild/win32-x64": "0.19.12" + } + }, "node_modules/type-check": { "version": "0.4.0", "resolved": "https://registry.npmjs.org/type-check/-/type-check-0.4.0.tgz", @@ -4469,9 +4854,9 @@ } }, "node_modules/typescript": { - "version": "5.2.2", - "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.2.2.tgz", - "integrity": "sha512-mI4WrpHsbCIcwT9cF4FZvr80QUeKvsUsUvKDoR+X/7XHQH98xYD8YHZg7ANtz2GtZt/CBq2QJ0thkGJMHfqc1w==", + "version": "5.4.3", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.4.3.tgz", + "integrity": "sha512-KrPd3PKaCLr78MalgiwJnA25Nm8HAmdwN3mYUYZgG/wizIo9EainNVQI9/yDavtVFRN2h3k8uf3GLHuhDMgEHg==", "dev": true, "bin": { "tsc": "bin/tsc", @@ -4496,6 +4881,12 @@ "url": "https://github.com/sponsors/ljharb" } }, + "node_modules/undici-types": { + "version": "5.26.5", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-5.26.5.tgz", + "integrity": "sha512-JlCMO+ehdEIKqlFxk6IfVoAUVmgz7cU7zD/h9XZ0qzeosSHmUJVOzSQvvYSYWXkFXC+IfLKSIffhv0sVZup6pA==", + "dev": true + }, "node_modules/uri-js": { "version": "4.4.1", "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz", @@ -4722,12 +5113,14 @@ "rzk-lezer": { "version": "0.1.0", "dependencies": { - "@lezer/lr": "^1.3.12" + "@lezer/lr": "^1.4.0" }, "devDependencies": { "@lezer-unofficial/printer": "^1.0.1", - "@lezer/generator": "deemp/generator#cc38c10ab0d9d6e9b0e6daf1659e7a15dad86649", - "tsx": "^3.13.0" + "@lezer/generator": "1.7.0", + "@types/node": "^20.12.2", + "tsx": "^4.7.0", + "typescript": "5.4.3" } } } diff --git a/rzk-playground/rzk-lezer/package-lock.json b/rzk-playground/rzk-lezer/package-lock.json index a6b15a062..2c2ef0ddd 100644 --- a/rzk-playground/rzk-lezer/package-lock.json +++ b/rzk-playground/rzk-lezer/package-lock.json @@ -12,8 +12,10 @@ }, "devDependencies": { "@lezer-unofficial/printer": "^1.0.1", - "@lezer/generator": "deemp/generator#cc38c10ab0d9d6e9b0e6daf1659e7a15dad86649", - "tsx": "^3.13.0" + "@lezer/generator": "1.7.0", + "@types/node": "^20.12.2", + "tsx": "^3.13.0", + "typescript": "5.4.3" } }, "node_modules/@codemirror/state": { @@ -390,11 +392,10 @@ "integrity": "sha512-XPIN3cYDXsoJI/oDWoR2tD++juVrhgIago9xyKhZ7IhGlzdDM9QgC8D8saKNCz5pindGcznFr2HBSsEQSWnSjw==" }, "node_modules/@lezer/generator": { - "version": "1.5.1", - "resolved": "git+ssh://git@github.com/deemp/generator.git#cc38c10ab0d9d6e9b0e6daf1659e7a15dad86649", - "integrity": "sha512-r2wTPQgpGKFSMyRo7hAa8PaSg3XVcmkX7PCnSWlXoK4d3Y6ZHTNbLD1cdczmrO1D+fLPMimtIcjgYiXQKnVRHQ==", + "version": "1.7.0", + "resolved": "https://registry.npmjs.org/@lezer/generator/-/generator-1.7.0.tgz", + "integrity": "sha512-IJ16tx3biLKlCXUzcK4v8S10AVa2BSM2rB12rtAL6f1hL2TS/HQQlGCoWRvanlL2J4mCYEEIv9uG7n4kVMkVDA==", "dev": true, - "license": "MIT", "dependencies": { "@lezer/common": "^1.1.0", "@lezer/lr": "^1.3.0" @@ -411,6 +412,15 @@ "@lezer/common": "^1.0.0" } }, + "node_modules/@types/node": { + "version": "20.12.2", + "resolved": "https://registry.npmjs.org/@types/node/-/node-20.12.2.tgz", + "integrity": "sha512-zQ0NYO87hyN6Xrclcqp7f8ZbXNbRfoGWNcMvHTPQp9UUrwI0mI7XBz+cu7/W6/VClYo2g63B0cjull/srU7LgQ==", + "dev": true, + "dependencies": { + "undici-types": "~5.26.4" + } + }, "node_modules/buffer-from": { "version": "1.1.2", "resolved": "https://registry.npmjs.org/buffer-from/-/buffer-from-1.1.2.tgz", @@ -524,6 +534,25 @@ "optionalDependencies": { "fsevents": "~2.3.3" } + }, + "node_modules/typescript": { + "version": "5.4.3", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.4.3.tgz", + "integrity": "sha512-KrPd3PKaCLr78MalgiwJnA25Nm8HAmdwN3mYUYZgG/wizIo9EainNVQI9/yDavtVFRN2h3k8uf3GLHuhDMgEHg==", + "dev": true, + "bin": { + "tsc": "bin/tsc", + "tsserver": "bin/tsserver" + }, + "engines": { + "node": ">=14.17" + } + }, + "node_modules/undici-types": { + "version": "5.26.5", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-5.26.5.tgz", + "integrity": "sha512-JlCMO+ehdEIKqlFxk6IfVoAUVmgz7cU7zD/h9XZ0qzeosSHmUJVOzSQvvYSYWXkFXC+IfLKSIffhv0sVZup6pA==", + "dev": true } } } diff --git a/rzk-playground/rzk-lezer/package.json b/rzk-playground/rzk-lezer/package.json index d28d592a5..72350c67f 100644 --- a/rzk-playground/rzk-lezer/package.json +++ b/rzk-playground/rzk-lezer/package.json @@ -4,12 +4,14 @@ "type": "module", "module": "dist/index.js", "devDependencies": { - "@lezer/generator": "deemp/generator#cc38c10ab0d9d6e9b0e6daf1659e7a15dad86649", "@lezer-unofficial/printer": "^1.0.1", - "tsx": "^3.13.0" + "@lezer/generator": "1.7.0", + "@types/node": "^20.12.2", + "tsx": "^4.7.0", + "typescript": "5.4.3" }, "dependencies": { - "@lezer/lr": "^1.3.12" + "@lezer/lr": "^1.4.0" }, "files": [ "examples" diff --git a/rzk-playground/rzk-lezer/src/run-examples.ts b/rzk-playground/rzk-lezer/src/run-examples.ts index a8cfd62b2..fac453819 100644 --- a/rzk-playground/rzk-lezer/src/run-examples.ts +++ b/rzk-playground/rzk-lezer/src/run-examples.ts @@ -3,7 +3,7 @@ import { printTree } from "@lezer-unofficial/printer" import { readFileSync, readdirSync, writeFileSync, mkdirSync, existsSync } from "fs" const src = "examples/src" -const exampleNames = readdirSync(src) +const exampleNames: string[] = readdirSync(src) const tree = "examples/tree" if (!existsSync(tree)) mkdirSync(tree, { recursive: true }) diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index 974b9f2d0..99618aaf3 100644 --- a/rzk/ChangeLog.md +++ b/rzk/ChangeLog.md @@ -6,6 +6,15 @@ 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.7.4 โ€” 2024-04-01 + +Fixes: +- Fix caching in Rzk Language Server, especially in presence of errors (see [#167](https://github.com/rzk-lang/rzk/pull/167)) +- Fix CI for the Rzk Playground (see [#174](https://github.com/rzk-lang/rzk/pull/174)) + +This release also contains minor refactoring (see [#165](https://github.com/rzk-lang/rzk/pull/165)) +and a typo fix (see [#171](https://github.com/rzk-lang/rzk/pull/171)). + ## v0.7.3 โ€” 2023-12-16 Fixes: @@ -82,7 +91,7 @@ Minor changes: ## v0.6.5 โ€” 2023-10-01 -This version contains mostly intrastructure improvements: +This version contains mostly infrastructure improvements: - Typecheck using `rzk.yaml` if it exists (see [#119](https://github.com/rzk-lang/rzk/pull/119)) - Update Rzk Playground and Nix Flake (see [#84](https://github.com/rzk-lang/rzk/pull/84)) @@ -91,7 +100,7 @@ This version contains mostly intrastructure improvements: - GHCJS 9.6 is now used - Support `snippet={code}` or `code={code}` param (see [#118](https://github.com/rzk-lang/rzk/pull/118)) - Support for `snippet_url={URL}` is temporarily dropped -- Update to GHC 9.6, latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116)) +- Update to GHC 9.6, the latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116)) - Add logging for Rzk Language Server (see [#114](https://github.com/rzk-lang/rzk/pull/114)) Fixes: @@ -100,7 +109,7 @@ Fixes: ## v0.6.4 โ€” 2023-09-27 -This version improves the stucture of the project, in particular w.r.t dependencies: +This version improves the structure of the project, in particular w.r.t dependencies: - Add custom snapshot and explicit lower bounds (see [#108](https://github.com/rzk-lang/rzk/pull/108)) @@ -111,7 +120,7 @@ This version contains a fix for the command line interface of `rzk`: - Fix command line `rzk typecheck` (see [#106](https://github.com/rzk-lang/rzk/pull/106)) - Previous version ignored failures in the command line - (the bug was introced when allowing better autocompletion in LSP). + (the bug was introduced when allowing better autocompletion in LSP). ## v0.6.2 โ€” 2023-09-26 @@ -145,14 +154,14 @@ This version contains two fixes (see [#88](https://github.com/rzk-lang/rzk/pull/ ## v0.5.6 โ€” 2023-09-19 -This version fixes the behaviour of glob (see [`77b7cc0`](https://github.com/rzk-lang/rzk/commit/77b7cc0494fe0bfd1c9f1aa83db20f42cfda5794)). +This version fixes the behavior of glob (see [`77b7cc0`](https://github.com/rzk-lang/rzk/commit/77b7cc0494fe0bfd1c9f1aa83db20f42cfda5794)). ## 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)); +2. Allow handling 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)). @@ -172,7 +181,7 @@ This version contains a few minor improvements: 2. Hint about possible shape coercions (see [#67](https://github.com/rzk-lang/rzk/pull/67)); 3. Enable doctests (see [#68](https://github.com/rzk-lang/rzk/pull/68)); 4. Improve documentation (add recommended installation instructions via VS Code) -5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983)); +5. Migrate from `fizruk` to `rzk-lang` organization 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 โ€” 2023-07-05 @@ -228,7 +237,7 @@ Minor improvements: ## v0.3.0 โ€” 2023-04-28 -This version introduces an experimental feature for generating visualisations for simplicial terms in SVG. +This version introduces an experimental feature for generating visualizations for simplicial terms in SVG. To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`): ```rzk @@ -252,7 +261,7 @@ This version was a complete rewrite of the proof assistant, using a new parser, ### Language Syntax is almost entirely backwards compatible with version 0.1.0. -Typechecking has been fixed and improved. +Type checking has been fixed and improved. #### Breaking Changes @@ -293,7 +302,7 @@ Otherwise, syntax is now made more flexible: := (t : ฮ”ยน) -> A [ โˆ‚ฮ”ยน t |-> recOR(t === 0_2, t === 1_2, x, y) ] ``` -6. Restrictions can now support multiple subshapes, effectively internalising `recOR`: +6. Restrictions can now support multiple subshapes, effectively internalizing `recOR`: ```rzk #def hom (A : U) (x y : A) : U @@ -308,7 +317,7 @@ Otherwise, syntax is now made more flexible: 9. `recOR` now supports alternative syntax with an arbitrary number of subshapes: `recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )` -10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalisations, or to upcast types. +10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalizations, or to upcast types. 11. New (better) commands are now supported: @@ -350,8 +359,8 @@ The output and error messages have been slightly improved, but not in a major wa ### Internal representation A new internal representation (a version of second-order abstract syntax) -allows to stop worrying about name captures in substitutions, +allows stopping worrying about name captures in substitutions, so the implementation is much more trustworthy. -The new representation will also allow to bring in higher-order unification in the future, for better type inference, matching, etc. +The new representation will also allow bringing in higher-order unification in the future, for better type inference, matching, etc. New representation also allowed annotating each (sub)term with its type to avoid recomputations and some other minor speedups. There are still some performance issues, which need to be debugged, but overall it is much faster than version 0.1.0 already. diff --git a/rzk/package.yaml b/rzk/package.yaml index f7bdb9133..dcc75ae77 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,5 +1,5 @@ name: rzk -version: 0.7.3 +version: 0.7.4 github: "rzk-lang/rzk" license: BSD3 author: "Nikolai Kudasov" diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 2901f4eff..803f863b7 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.7.3 +version: 0.7.4 synopsis: An experimental proof assistant for synthetic โˆž-categories description: Please see the README on GitHub at category: Dependent Types diff --git a/rzk/src/Language/Rzk/VSCode/Env.hs b/rzk/src/Language/Rzk/VSCode/Env.hs index 1305f78e7..f2328e33e 100644 --- a/rzk/src/Language/Rzk/VSCode/Env.hs +++ b/rzk/src/Language/Rzk/VSCode/Env.hs @@ -3,12 +3,18 @@ module Language.Rzk.VSCode.Env where import Control.Concurrent.STM import Control.Monad.Reader import Language.LSP.Server +import Language.Rzk.Free.Syntax (VarIdent) import Language.Rzk.VSCode.Config (ServerConfig) -import Rzk.TypeCheck (Decl') +import Rzk.TypeCheck (Decl', TypeErrorInScopedContext) -type RzkTypecheckCache = [(FilePath, [Decl'])] +data RzkCachedModule = RzkCachedModule + { cachedModuleDecls :: [Decl'] + , cachedModuleErrors :: [TypeErrorInScopedContext VarIdent] + } + +type RzkTypecheckCache = [(FilePath, RzkCachedModule)] -data RzkEnv = RzkEnv +newtype RzkEnv = RzkEnv { rzkEnvTypecheckCache :: TVar RzkTypecheckCache } @@ -18,7 +24,6 @@ defaultRzkEnv = do return RzkEnv { rzkEnvTypecheckCache = typecheckCache } - type LSP = LspT ServerConfig (ReaderT RzkEnv IO) -- | Override the cache with given typechecked modules. diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index 5af6bb276..49ecdf329 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -1,21 +1,28 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE RecordWildCards #-} module Language.Rzk.VSCode.Handlers ( typecheckFromConfigFile, provideCompletions, formatDocument, + provideSemanticTokens, + handleFilesChanged, ) where import Control.Exception (SomeException, evaluate, try) import Control.Lens import Control.Monad (forM_, when) +import Control.Monad.Except (ExceptT (ExceptT), + MonadError (throwError), + modifyError, runExceptT) import Control.Monad.IO.Class (MonadIO (..)) import Data.Default.Class -import Data.List (sort, (\\)) +import Data.List (isSuffixOf, sort, (\\)) import Data.Maybe (fromMaybe, isNothing) import qualified Data.Text as T import qualified Data.Yaml as Yaml @@ -25,7 +32,7 @@ import Language.LSP.Protocol.Lens (HasDetail (detail), HasLabel (label), HasParams (params), HasTextDocument (textDocument), - HasUri (uri)) + HasUri (uri), changes, uri) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server @@ -36,10 +43,12 @@ import System.FilePath.Glob (compile, globDir) import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition), VarIdent (getVarIdent)) import Language.Rzk.Syntax (Module, VarIdent' (VarIdent), - parseModuleFile, printTree) + parseModuleFile, + parseModuleSafe, printTree) import Language.Rzk.VSCode.Config (ServerConfig (ServerConfig, formatEnabled)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Logging +import Language.Rzk.VSCode.Tokenize (tokenizeModule) import Rzk.Format (FormattingEdit (..), formatTextEdits) import Rzk.Project.Config (ProjectConfig (include)) @@ -94,7 +103,8 @@ typecheckFromConfigFile = do rawPaths <- liftIO $ globDir (map compile (include config)) rootPath let paths = concatMap sort rawPaths - cachedModules <- getCachedTypecheckedModules + typecheckedCachedModules <- getCachedTypecheckedModules + let cachedModules = map (\(path, RzkCachedModule{..}) -> (path, cachedModuleDecls)) typecheckedCachedModules let cachedPaths = map fst cachedModules modifiedFiles = paths \\ cachedPaths @@ -118,13 +128,14 @@ typecheckFromConfigFile = do -- cache well-typed modules logInfo (show (length checkedModules) ++ " modules successfully typechecked") logInfo (show (length errors) ++ " errors found") - cacheTypecheckedModules checkedModules + let checkedModules' = map (\(path, decls) -> (path, RzkCachedModule decls (filter ((== path) . filepathOfTypeError) errors))) checkedModules + cacheTypecheckedModules checkedModules' return (errors, checkedModules) -- Reset all published diags -- TODO: remove this after properly grouping by path below, after which there can be an empty list of errors -- TODO: handle clearing diagnostics for files that got removed from the project (rzk.yaml) - forM_ paths $ \path -> do + forM_ modifiedFiles $ \path -> do publishDiagnostics 0 (filePathToNormalizedUri path) Nothing (partitionBySource []) -- Report parse errors to the client @@ -194,8 +205,9 @@ provideCompletions req res = do logDebug ("Found " ++ show (length cachedModules) ++ " modules in the cache") let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri -- Take all the modules up to and including the currently open one - let modules = takeWhileInc ((/= currentFile) . fst) cachedModules + let modules = map ignoreErrors $ takeWhileInc ((/= currentFile) . fst) cachedModules where + ignoreErrors (path, RzkCachedModule{..}) = (path, cachedModuleDecls) takeWhileInc _ [] = [] takeWhileInc p (x:xs) | p x = x : takeWhileInc p xs @@ -249,3 +261,80 @@ formatDocument req res = do else do logDebug "Formatting is disabled in config" res $ Right $ InR Null + +provideSemanticTokens :: Handler LSP 'Method_TextDocumentSemanticTokensFull +provideSemanticTokens req responder = do + let doc = req ^. params . textDocument . uri . to toNormalizedUri + mdoc <- getVirtualFile doc + possibleTokens <- case virtualFileText <$> mdoc of + Nothing -> return (Left "Failed to get file content") + Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ + parseModuleSafe (filter (/= '\r') $ T.unpack sourceCode) + case possibleTokens of + Left err -> do + -- Exception occurred when parsing the module + logWarning ("Failed to tokenize file: " ++ err) + Right tokens -> do + let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens + case encoded of + Left _err -> do + -- Failed to encode the tokens + return () + Right list -> + responder (Right (InL (SemanticTokens Nothing list))) + + +data IsChanged + = HasChanged + | NotChanged + +-- | Detects if the given path has changes in its declaration compared to what's in the cache +isChanged :: RzkTypecheckCache -> FilePath -> LSP IsChanged +isChanged cache path = toIsChanged $ do + let cacheWithoutErrors = map (fmap cachedModuleDecls) cache + errors <- maybeToEitherLSP $ cachedModuleErrors <$> lookup path cache + cachedDecls <- maybeToEitherLSP $ cachedModuleDecls <$> lookup path cache + module' <- toExceptTLifted $ parseModuleFile path + e <- toExceptTLifted $ try @SomeException $ evaluate $ + defaultTypeCheck (typecheckModulesWithLocationIncremental (takeWhile ((/= path) . fst) cacheWithoutErrors) [(path, module')]) + (checkedModules, errors') <- toExceptT $ return e + decls' <- maybeToEitherLSP $ lookup path checkedModules + return $ if null errors' && null errors && decls' == cachedDecls + then NotChanged + else HasChanged + where + toExceptT = modifyError (const ()) . ExceptT + toExceptTLifted = toExceptT . liftIO + maybeToEitherLSP = \case + Nothing -> throwError () + Just x -> return x + toIsChanged m = runExceptT m >>= \case + Left _ -> return HasChanged -- in case of error consider the file has changed + Right x -> return x + +hasNotChanged :: RzkTypecheckCache -> FilePath -> LSP Bool +hasNotChanged cache path = isChanged cache path >>= \case + HasChanged -> return False + NotChanged -> return True + +-- | Monadic 'dropWhile' +dropWhileM :: (Monad m) => (a -> m Bool) -> [a] -> m [a] +dropWhileM _ [] = return [] +dropWhileM p (x:xs) = do + q <- p x + if q + then dropWhileM p xs + else return (x:xs) + +handleFilesChanged :: Handler LSP 'Method_WorkspaceDidChangeWatchedFiles +handleFilesChanged msg = do + let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just + if any ("rzk.yaml" `isSuffixOf`) modifiedPaths + then do + logDebug "rzk.yaml modified. Clearing module cache" + resetCacheForAllFiles + else do + cache <- getCachedTypecheckedModules + actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths + resetCacheForFiles actualModified + typecheckFromConfigFile diff --git a/rzk/src/Language/Rzk/VSCode/Lsp.hs b/rzk/src/Language/Rzk/VSCode/Lsp.hs index 3f2ee860d..640e87f7d 100644 --- a/rzk/src/Language/Rzk/VSCode/Lsp.hs +++ b/rzk/src/Language/Rzk/VSCode/Lsp.hs @@ -1,84 +1,26 @@ {-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TypeApplications #-} module Language.Rzk.VSCode.Lsp where -import Control.Lens (_Just, to, (^.), (^..)) import Control.Monad.IO.Class import Control.Monad.Reader import Data.Default.Class (Default (def)) -import Data.List (isSuffixOf) import qualified Data.Text as T -import Language.LSP.Protocol.Lens (HasParams (params), - HasTextDocument (textDocument), - HasUri (uri), changes, uri) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server -import Language.LSP.VFS (virtualFileText) -import Control.Exception (SomeException, evaluate, try) -import Control.Monad.Except (ExceptT (ExceptT), - MonadError (throwError), - modifyError, runExceptT) import Data.Aeson (Result (Error, Success), fromJSON) -import Language.Rzk.Syntax (parseModuleFile, - parseModuleSafe) import Language.Rzk.VSCode.Config (ServerConfig (..)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Handlers -import Language.Rzk.VSCode.Logging -import Language.Rzk.VSCode.Tokenize (tokenizeModule) -import Rzk.TypeCheck (defaultTypeCheck, - typecheckModulesWithLocationIncremental) -- | The maximum number of diagnostic messages to send to the client maxDiagnosticCount :: Int maxDiagnosticCount = 100 -data IsChanged - = HasChanged - | NotChanged - --- | Detects if the given path has changes in its declaration compared to what's in the cache -isChanged :: RzkTypecheckCache -> FilePath -> LSP IsChanged -isChanged cache path = toIsChanged $ do - cachedDecls <- maybeToEitherLSP $ lookup path cache - module' <- toExceptTLifted $ parseModuleFile path - e <- toExceptTLifted $ try @SomeException $ evaluate $ - defaultTypeCheck (typecheckModulesWithLocationIncremental (takeWhile ((/= path) . fst) cache) [(path, module')]) - (checkedModules, _errors) <- toExceptT $ return e - decls' <- maybeToEitherLSP $ lookup path checkedModules - return $ if decls' == cachedDecls - then NotChanged - else HasChanged - where - toExceptT = modifyError (const ()) . ExceptT - toExceptTLifted = toExceptT . liftIO - maybeToEitherLSP = \case - Nothing -> throwError () - Just x -> return x - toIsChanged m = runExceptT m >>= \case - Left _ -> return HasChanged -- in case of error consider the file has changed - Right x -> return x - -hasNotChanged :: RzkTypecheckCache -> FilePath -> LSP Bool -hasNotChanged cache path = isChanged cache path >>= \case - HasChanged -> return False - NotChanged -> return True - --- | Monadic 'dropWhile' -dropWhileM :: (Monad m) => (a -> m Bool) -> [a] -> m [a] -dropWhileM _ [] = return [] -dropWhileM p (x:xs) = do - q <- p x - if q - then dropWhileM p xs - else return (x:xs) - handlers :: Handlers LSP handlers = mconcat @@ -86,20 +28,9 @@ handlers = -- TODO: add logging -- Empty handlers to silence the errors , notificationHandler SMethod_TextDocumentDidOpen $ \_msg -> pure () - -- , requestHandler SMethod_TextDocumentFormatting $ \_req _res -> pure () , notificationHandler SMethod_TextDocumentDidChange $ \_msg -> pure () , notificationHandler SMethod_TextDocumentDidClose $ \_msg -> pure () - , notificationHandler SMethod_WorkspaceDidChangeWatchedFiles $ \msg -> do - let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just - if any ("rzk.yaml" `isSuffixOf`) modifiedPaths - then do - logDebug "rzk.yaml modified. Clearing module cache" - resetCacheForAllFiles - else do - cache <- getCachedTypecheckedModules - actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths - resetCacheForFiles actualModified - typecheckFromConfigFile + , notificationHandler SMethod_WorkspaceDidChangeWatchedFiles handleFilesChanged , notificationHandler SMethod_TextDocumentDidSave $ \_msg -> do -- TODO: check if the file is included in the config's `include` list. -- If not (and not in `exclude`) either, issue a warning. @@ -115,25 +46,7 @@ handlers = -- range' = Range pos pos -- responder (Right $ InL rsp) , requestHandler SMethod_TextDocumentCompletion provideCompletions - , requestHandler SMethod_TextDocumentSemanticTokensFull $ \req responder -> do - let doc = req ^. params . textDocument . uri . to toNormalizedUri - mdoc <- getVirtualFile doc - possibleTokens <- case virtualFileText <$> mdoc of - Nothing -> return (Left "Failed to get file content") - Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ - parseModuleSafe (filter (/= '\r') $ T.unpack sourceCode) - case possibleTokens of - Left err -> do - -- Exception occurred when parsing the module - logWarning ("Failed to tokenize file: " ++ err) - Right tokens -> do - let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens - case encoded of - Left _err -> do - -- Failed to encode the tokens - return () - Right list -> - responder (Right (InL SemanticTokens { _resultId = Nothing, _data_ = list })) + , requestHandler SMethod_TextDocumentSemanticTokensFull provideSemanticTokens , requestHandler SMethod_TextDocumentFormatting formatDocument ] diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index c5a307e12..027c1acd7 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -5,8 +5,6 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeSynonymInstances #-} module Rzk.TypeCheck where import Control.Applicative ((<|>))