From 54cda98f6a7ae2b04d6c2f020db6d18641181b2a Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sun, 3 Aug 2025 00:58:26 +0800 Subject: [PATCH 01/15] Add RTS option -V1 for wasm32 build --- agda-language-server.cabal | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/agda-language-server.cabal b/agda-language-server.cabal index cf56e92..509c83a 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -145,11 +145,12 @@ executable als if flag(Agda-2-7-0-1) build-depends: Agda ==2.7.0.1 - if arch(wasm32) - build-depends: - unix >=2.8.0.0 && <2.9 if !arch(wasm32) ghc-options: -threaded -with-rtsopts=-N + else + build-depends: + unix >=2.8.0.0 && <2.9 + ghc-options: -with-rtsopts=-V1 test-suite als-test type: exitcode-stdio-1.0 @@ -223,8 +224,9 @@ test-suite als-test if flag(Agda-2-7-0-1) build-depends: Agda ==2.7.0.1 - if arch(wasm32) - build-depends: - unix >=2.8.0.0 && <2.9 if !arch(wasm32) ghc-options: -threaded -with-rtsopts=-N + else + build-depends: + unix >=2.8.0.0 && <2.9 + ghc-options: -with-rtsopts=-V1 From 95c2dd24f6f7a9185ef439fa8adc0462a1ffcfdc Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Tue, 16 Sep 2025 02:28:46 +0800 Subject: [PATCH 02/15] Update doc reflecting that the out-of-bound issue was fixed --- BUILDING_WASM.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/BUILDING_WASM.md b/BUILDING_WASM.md index b5e250f..f2fed31 100644 --- a/BUILDING_WASM.md +++ b/BUILDING_WASM.md @@ -24,6 +24,7 @@ Node.js v22.14.0 ``` At this moment, you should terminate the process and run it again. -This is a known issue ([ghc#26106](https://gitlab.haskell.org/ghc/ghc/-/issues/26106)). If this does *not* occur to you or you can fix it, please report to that issue. + +This was a known issue ([ghc#26106](https://gitlab.haskell.org/ghc/ghc/-/issues/26106)) and was fixed in the [GHC upstream](https://gitlab.haskell.org/ghc/ghc/-/commit/3e4a456801ba6aab5d8a6c0ae5a4ba8ab99b9d25). If everything works properly, it should build a binary `als.wasm`. From 224967677003d9e1346950c942b7cb59961b77b7 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sat, 20 Sep 2025 02:23:35 +0800 Subject: [PATCH 03/15] Try to build ALS with 2.8.0 (correctly) --- .github/workflows/wasm.yaml | 4 ++-- .gitmodules | 3 +++ cabal.project | 6 +----- wasm-submodules/agda | 1 + 4 files changed, 7 insertions(+), 7 deletions(-) create mode 160000 wasm-submodules/agda diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 231eb1d..c356dc4 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -2,11 +2,11 @@ name: Compile WASM on: push: - branches: [wasm] + branches: [wasm, wasm-*] tags: - 'v*' # Push events to matching v*, i.e. v1.0, v20.15.10 pull_request: - branches: [wasm] + branches: [wasm, wasm-*] env: GHC_WASM_META_FLAVOUR: '9.10' diff --git a/.gitmodules b/.gitmodules index edc646d..dc10f3e 100644 --- a/.gitmodules +++ b/.gitmodules @@ -2,3 +2,6 @@ path = wasm-submodules/network url = https://github.com/haskell-wasm/network +[submodule "wasm-submodules/agda"] + path = wasm-submodules/agda + url = git@github.com:agda-web/agda.git diff --git a/cabal.project b/cabal.project index f2c211d..dc7a89f 100644 --- a/cabal.project +++ b/cabal.project @@ -1,12 +1,8 @@ packages: . + wasm-submodules/agda wasm-submodules/network -source-repository-package - type: git - location: https://github.com/agda-web/agda.git - tag: 87cac9ce17932321dc1a0fdaed83436de22fa0aa - source-repository-package type: git location: https://github.com/haskell-wasm/foundation.git diff --git a/wasm-submodules/agda b/wasm-submodules/agda new file mode 160000 index 0000000..e2f8c69 --- /dev/null +++ b/wasm-submodules/agda @@ -0,0 +1 @@ +Subproject commit e2f8c69414fa115328280ecc4de1d2b7a23be7fa From cc3b9f5a5eca386319b42b8cd237bd0bca96f7f0 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sat, 20 Sep 2025 02:25:23 +0800 Subject: [PATCH 04/15] Bump ghc-wasm-meta --- .github/workflows/wasm.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index c356dc4..4bac2f6 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -10,7 +10,7 @@ on: env: GHC_WASM_META_FLAVOUR: '9.10' - GHC_WASM_META_COMMIT_HASH: '7927129e42bcd6a54b9e06e26455803fa4878261' + GHC_WASM_META_COMMIT_HASH: '78c87e9236a547fcb439db6927391df625af16fb' jobs: build: From 78b9e47c209616b114293d00d96f39480e3fac51 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sat, 20 Sep 2025 02:36:38 +0800 Subject: [PATCH 05/15] Update cabal.project.wasm32 --- cabal.project.wasm32 | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/cabal.project.wasm32 b/cabal.project.wasm32 index f2c211d..dc7a89f 100644 --- a/cabal.project.wasm32 +++ b/cabal.project.wasm32 @@ -1,12 +1,8 @@ packages: . + wasm-submodules/agda wasm-submodules/network -source-repository-package - type: git - location: https://github.com/agda-web/agda.git - tag: 87cac9ce17932321dc1a0fdaed83436de22fa0aa - source-repository-package type: git location: https://github.com/haskell-wasm/foundation.git From 9fd38afd85cdc687bad28a9a0a7db5197d7e8e38 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sat, 20 Sep 2025 03:15:45 +0800 Subject: [PATCH 06/15] Add type annotation to catchIO argument --- src/Server.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Server.hs b/src/Server.hs index b7c2b54..05aa218 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -52,7 +52,7 @@ run options = do Nothing -> do #if defined(wasm32_HOST_ARCH) liftIO $ setFdOption stdInput NonBlockingRead True - `catchIO` (\ e -> hPutStrLn stderr $ "Failed to enable nonblocking on stdin: " ++ (show e) ++ "\nThe WASM module might not behave correctly.") + `catchIO` (\ (e :: IOError) -> hPutStrLn stderr $ "Failed to enable nonblocking on stdin: " ++ (show e) ++ "\nThe WASM module might not behave correctly.") #endif runServer (serverDefn options) where From 7ab67c7c21297543cda18d26f080f2c43943aadf Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sat, 20 Sep 2025 04:12:22 +0800 Subject: [PATCH 07/15] Enable ScopedTypeVariables in server entry --- src/Server.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Server.hs b/src/Server.hs index 05aa218..df833f4 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE ScopedTypeVariables #-} -- entry point of the LSP server From 742e3098e319fadf3846d0d8438d5d6df286687a Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Sat, 20 Sep 2025 14:46:01 +0800 Subject: [PATCH 08/15] Use wasm-opt to reduce file size --- .github/workflows/wasm.yaml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 4bac2f6..e7a6d46 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -121,7 +121,10 @@ jobs: run: | mkdir ~/out wasm32-wasi-cabal build - cp $(wasm32-wasi-cabal list-bin als) ~/out + ALS_PATH=$(wasm32-wasi-cabal list-bin als) + stat --format="%s" "$ALS_PATH" + time wasm-opt "$ALS_PATH" -Oz -o ~/out/als.wasm + stat --format="%s" ~/out/als.wasm - name: Clean up native/wasm cabal logs run: rm -rf ~/.cache/cabal/logs ~/.ghc-wasm/.cabal/logs From 8a00fcce9540aa6df5555ac7f6481bc0638e87f5 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 01:02:14 +0800 Subject: [PATCH 09/15] Bump ghc-wasm-meta, fixing random build failures of lsp-types --- .github/workflows/wasm.yaml | 12 ++---------- BUILDING_WASM.md | 23 ----------------------- 2 files changed, 2 insertions(+), 33 deletions(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index e7a6d46..1e62c46 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -10,7 +10,7 @@ on: env: GHC_WASM_META_FLAVOUR: '9.10' - GHC_WASM_META_COMMIT_HASH: '78c87e9236a547fcb439db6927391df625af16fb' + GHC_WASM_META_COMMIT_HASH: 'c3f44696d29aaeadd755d69c51735954bfcd59db' jobs: build: @@ -86,15 +86,7 @@ jobs: mv cabal.project.wasm32 cabal.project wasm32-wasi-cabal configure --flag=Agda-2-8-0 - - name: 'Build dep: lsp-types' - uses: nick-fields/retry@v3 - id: build-dep-lsp-types - with: - timeout_minutes: 10 - max_attempts: 2 - command: cd als && wasm32-wasi-cabal build lib:lsp-types - - - name: 'Build dep: agda' + - name: Build Agda as dependency id: build-dep-agda working-directory: './als' run: wasm32-wasi-cabal build lib:agda diff --git a/BUILDING_WASM.md b/BUILDING_WASM.md index f2fed31..f7bebaa 100644 --- a/BUILDING_WASM.md +++ b/BUILDING_WASM.md @@ -5,26 +5,3 @@ 3. In the project root, run `cp cabal.project{.wasm32,}`, and then `wasm32-wasi-cabal build`. Note: This project uses a hybrid approach - most dependencies use cabal's git handling, but the network package remains as a git submodule due to autotools requirements. - -The process might output the following: - -``` -[442 of 452] Compiling Language.LSP.Protocol.Message.Types ( src/Language/LSP/Protocol/Message/Types.hs, /home/qbane/agda-project/haskell-lsp-wasm/dist-newstyle/build/wasm32-wasi/ghc-9.10.1.20250207/lsp-types-2.3.0.1/build/Language/LSP/Protocol/Message/Types.o, /home/qbane/agda-project/haskell-lsp-wasm/dist-newstyle/build/wasm32-wasi/ghc-9.10.1.20250207/lsp-types-2.3.0.1/build/Language/LSP/Protocol/Message/Types.dyn_o ) - -wasm://wasm/001e3c92:1 - - -RuntimeError: table index is out of bounds - at wasm://wasm/001e3c92:wasm-function[586]:0x45e40 - at wasm://wasm/001e3c92:wasm-function[365]:0x286e1 - at wasm://wasm/001e3c92:wasm-function[595]:0x46135 - at process.processImmediate (node:internal/timers:491:21) - -Node.js v22.14.0 -``` - -At this moment, you should terminate the process and run it again. - -This was a known issue ([ghc#26106](https://gitlab.haskell.org/ghc/ghc/-/issues/26106)) and was fixed in the [GHC upstream](https://gitlab.haskell.org/ghc/ghc/-/commit/3e4a456801ba6aab5d8a6c0ae5a4ba8ab99b9d25). - -If everything works properly, it should build a binary `als.wasm`. From 0adfe486da3040a185b8ae6e5a7a726a1c92ec86 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 01:58:31 +0800 Subject: [PATCH 10/15] Use lsp-types from upstream --- cabal.project | 6 ------ 1 file changed, 6 deletions(-) diff --git a/cabal.project b/cabal.project index dc7a89f..008d1c3 100644 --- a/cabal.project +++ b/cabal.project @@ -14,11 +14,5 @@ source-repository-package location: https://github.com/k0001/network-simple.git tag: 2c3ab6e7aa2a86be692c55bf6081161d83d50c34 -source-repository-package - type: git - location: https://github.com/agda-web/lsp.git - tag: 9baf76e6d9965a3b6e8b3ecfcdf33c62b5628fd8 - subdir: lsp-types - package Agda flags: +optimise-heavily From 7dfb578b3968ed8b1680f5660dc4c76e33912efe Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 02:07:05 +0800 Subject: [PATCH 11/15] Add strategy matrix in CI to build with multiple Agda versions --- .github/workflows/wasm.yaml | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 1e62c46..5e369bf 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -16,12 +16,26 @@ jobs: build: name: Build runs-on: ubuntu-22.04 + strategy: + matrix: + agda: + # undocumented usage; see https://stackoverflow.com/q/66025220 + - { name: '2.8.0', flag: '2-8-0', commit: 'e2f8c69414fa115328280ecc4de1d2b7a23be7fa' } + - { name: '2.7.0', flag: '2-7-0', commit: '702c924fdab93aa8992adca84e72a91c490f7b1b' } + - { name: '2.6.4.3', flag: '2-6-4', commit: '8f35851954c39dc3849095bfd018bed9bd1b32ad' } + fail-fast: false steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 with: path: als - submodules: true + submodules: recursive + + - name: Checkout Agda submodule at v${{ matrix.agda.name }} + run: | + cd als/wasm-submodules/agda + git fetch --depth 1 origin "${{ matrix.agda.commit }}" + git checkout FETCH_HEAD - name: Compute cache key run: echo "CI_CACHE_KEY=${{ runner.os }}-${{ runner.arch }}-${{ env.GHC_WASM_META_COMMIT_HASH }}-flavor-${{ env.GHC_WASM_META_FLAVOUR }}" >> "$GITHUB_ENV" @@ -84,7 +98,7 @@ jobs: working-directory: './als' run: | mv cabal.project.wasm32 cabal.project - wasm32-wasi-cabal configure --flag=Agda-2-8-0 + wasm32-wasi-cabal configure --flag=Agda-${{ matrix.agda.flag }} - name: Build Agda as dependency id: build-dep-agda @@ -93,12 +107,12 @@ jobs: - name: Cache dist-newstyle uses: actions/cache/save@v4 - if: steps.build-dep-lsp-types.outcome == 'success' && steps.build-dep-agda.outcome == 'success' + if: steps.build-dep-agda.outcome == 'success' with: path: als/dist-newstyle key: dist-newstyle-${{ env.CI_CACHE_KEY }}-${{ hashFiles('als/dist-newstyle/**') }} - - name: Build dependencies + - name: Build dependencies other than Agda working-directory: './als' run: | # Setup network submodule autotools From a28b0f225004a861a2d938939d42b81b0fbf7fb8 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 02:12:24 +0800 Subject: [PATCH 12/15] Fix using lsp not taking effect in CI --- cabal.project | 18 ------------------ cabal.project.wasm32 | 6 ------ 2 files changed, 24 deletions(-) delete mode 100644 cabal.project diff --git a/cabal.project b/cabal.project deleted file mode 100644 index 008d1c3..0000000 --- a/cabal.project +++ /dev/null @@ -1,18 +0,0 @@ -packages: - . - wasm-submodules/agda - wasm-submodules/network - -source-repository-package - type: git - location: https://github.com/haskell-wasm/foundation.git - tag: 8e6dd48527fb429c1922083a5030ef88e3d58dd3 - subdir: basement - -source-repository-package - type: git - location: https://github.com/k0001/network-simple.git - tag: 2c3ab6e7aa2a86be692c55bf6081161d83d50c34 - -package Agda - flags: +optimise-heavily diff --git a/cabal.project.wasm32 b/cabal.project.wasm32 index dc7a89f..008d1c3 100644 --- a/cabal.project.wasm32 +++ b/cabal.project.wasm32 @@ -14,11 +14,5 @@ source-repository-package location: https://github.com/k0001/network-simple.git tag: 2c3ab6e7aa2a86be692c55bf6081161d83d50c34 -source-repository-package - type: git - location: https://github.com/agda-web/lsp.git - tag: 9baf76e6d9965a3b6e8b3ecfcdf33c62b5628fd8 - subdir: lsp-types - package Agda flags: +optimise-heavily From 925e5bd95bb6ea1a4f5ce2bbcf60188cd54b86d2 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 02:23:42 +0800 Subject: [PATCH 13/15] Add version suffix to artifact names --- .github/workflows/wasm.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 5e369bf..721d02f 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -38,7 +38,7 @@ jobs: git checkout FETCH_HEAD - name: Compute cache key - run: echo "CI_CACHE_KEY=${{ runner.os }}-${{ runner.arch }}-${{ env.GHC_WASM_META_COMMIT_HASH }}-flavor-${{ env.GHC_WASM_META_FLAVOUR }}" >> "$GITHUB_ENV" + run: echo "CI_CACHE_KEY=${{ runner.os }}-${{ runner.arch }}-${{ env.GHC_WASM_META_COMMIT_HASH }}-flavor-${{ env.GHC_WASM_META_FLAVOUR }}-${{ matrix.agda.name }}" >> "$GITHUB_ENV" - name: Try to restore cached .ghc-wasm id: ghc-wasm-cache-restore @@ -154,6 +154,6 @@ jobs: - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: als + name: als-wasm-${{ matrix.agda.name }} path: ~/out include-hidden-files: true From 1e87f06d232b9b484c56c2e9e243c2693017cd73 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 14:20:31 +0800 Subject: [PATCH 14/15] Unify version string with a suffix for WASM builds --- src/Options.hs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/Options.hs b/src/Options.hs index a2c0ce3..585a0d7 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -77,17 +77,21 @@ versionNumber = 6 versionString :: String versionString = -#ifdef wasm32_HOST_ARCH - "Agda v2.7.0.1 Language Server v" <> show versionNumber <> " (WebAssembly build)" -#elif MIN_VERSION_Agda(2,8,0) - "Agda v2.8.0 Language Server v" <> show versionNumber +#if MIN_VERSION_Agda(2,8,0) + "Agda v2.8.0 Language Server v" <> show versionNumber <> suffix #elif MIN_VERSION_Agda(2,7,0) - "Agda v2.7.0.1 Language Server v" <> show versionNumber + "Agda v2.7.0.1 Language Server v" <> show versionNumber <> suffix #elif MIN_VERSION_Agda(2,6,4) - "Agda v2.6.4.3 Language Server v" <> show versionNumber + "Agda v2.6.4.3 Language Server v" <> show versionNumber <> suffix #else error "Unsupported Agda version" #endif + where +#ifdef wasm32_HOST_ARCH + suffix = " (WebAssembly build)" +#else + suffix = "" +#endif usage :: String usage = versionString <> "\nUsage: als [Options...]\n" From 7c8e67b9edc03397188326e472266a9ea637f582 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Mon, 29 Sep 2025 18:39:17 +0800 Subject: [PATCH 15/15] Fix version name typo --- .github/workflows/wasm.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 721d02f..411a312 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -21,7 +21,7 @@ jobs: agda: # undocumented usage; see https://stackoverflow.com/q/66025220 - { name: '2.8.0', flag: '2-8-0', commit: 'e2f8c69414fa115328280ecc4de1d2b7a23be7fa' } - - { name: '2.7.0', flag: '2-7-0', commit: '702c924fdab93aa8992adca84e72a91c490f7b1b' } + - { name: '2.7.0.1', flag: '2-7-0', commit: '702c924fdab93aa8992adca84e72a91c490f7b1b' } - { name: '2.6.4.3', flag: '2-6-4', commit: '8f35851954c39dc3849095bfd018bed9bd1b32ad' } fail-fast: false