agda · andy0130tw · Aug 2, 2025 · Sep 15, 2025 · Sep 19, 2025 · Sep 19, 2025
diff --git 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
@@ -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
@@ -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
@@ -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
diff --git 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
@@ -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
@@ -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