diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 231eb1d..411a312 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -2,29 +2,43 @@ 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' - GHC_WASM_META_COMMIT_HASH: '7927129e42bcd6a54b9e06e26455803fa4878261' + GHC_WASM_META_COMMIT_HASH: 'c3f44696d29aaeadd755d69c51735954bfcd59db' 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.1', 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" + 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 @@ -84,29 +98,21 @@ jobs: working-directory: './als' run: | 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 + wasm32-wasi-cabal configure --flag=Agda-${{ matrix.agda.flag }} - - name: 'Build dep: agda' + - name: Build Agda as dependency id: build-dep-agda working-directory: './als' run: wasm32-wasi-cabal build lib:agda - 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 @@ -121,7 +127,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 @@ -145,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 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/BUILDING_WASM.md b/BUILDING_WASM.md index b5e250f..f7bebaa 100644 --- a/BUILDING_WASM.md +++ b/BUILDING_WASM.md @@ -5,25 +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 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. - -If everything works properly, it should build a binary `als.wasm`. diff --git a/agda-language-server.cabal b/agda-language-server.cabal index dc4bca2..378b857 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -160,7 +160,8 @@ executable als if arch(wasm32) build-depends: unix >=2.8.0.0 && <2.9 - if !arch(wasm32) + ghc-options: -with-rtsopts=-V1 + else ghc-options: -threaded -with-rtsopts=-N test-suite als-test @@ -241,5 +242,6 @@ test-suite als-test if arch(wasm32) build-depends: unix >=2.8.0.0 && <2.9 - if !arch(wasm32) + ghc-options: -with-rtsopts=-V1 + else ghc-options: -threaded -with-rtsopts=-N diff --git a/cabal.project b/cabal.project deleted file mode 100644 index f2c211d..0000000 --- a/cabal.project +++ /dev/null @@ -1,28 +0,0 @@ -packages: - . - 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 - tag: 8e6dd48527fb429c1922083a5030ef88e3d58dd3 - subdir: basement - -source-repository-package - type: git - 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 diff --git a/cabal.project.wasm32 b/cabal.project.wasm32 index f2c211d..008d1c3 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 @@ -18,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 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" diff --git a/src/Server.hs b/src/Server.hs index b7c2b54..df833f4 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE ScopedTypeVariables #-} -- entry point of the LSP server @@ -52,7 +53,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 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