From bc58354cd7a87e638d4516fbde67ce67e205297a Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Wed, 23 Jul 2025 12:32:11 +0800 Subject: [PATCH 1/3] Fix compatibility issues for both native and wasm32 targets --- .github/workflows/wasm.yaml | 6 ++++-- BUILDING_WASM.md | 4 ++-- agda-language-server.cabal | 6 ++++++ cabal.project => cabal.project.wasm32 | 0 src/Options.hs | 2 +- src/Server.hs | 4 ++-- 6 files changed, 15 insertions(+), 7 deletions(-) rename cabal.project => cabal.project.wasm32 (100%) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 125eee2..9b3495d 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -74,9 +74,11 @@ jobs: echo ">>> Install alex and happy" ~/.ghc-wasm/cabal/bin/cabal install alex-3.5.0.0 happy-1.20.1.1 - - name: Run cabal configure + - name: Cabal configure working-directory: './als' - run: wasm32-wasi-cabal configure --flag=Agda-2-7-0-1 + run: | + mv cabal.project.wasm32 cabal.project + wasm32-wasi-cabal configure --flag=Agda-2-7-0-1 - name: 'Build dep: lsp-types' uses: nick-fields/retry@v3 diff --git a/BUILDING_WASM.md b/BUILDING_WASM.md index 6b76b2b..29d8c54 100644 --- a/BUILDING_WASM.md +++ b/BUILDING_WASM.md @@ -2,7 +2,7 @@ 1. Setup a working ghc (tested with v9.10) with WASM backend and wasm32-wasi-cabal. 2. `cd` into `wasm-submodules/network` and run `autoreconf -i`. -3. In the project root, run `wasm32-wasi-cabal build`. +3. In the project root, run `cp cabal.project{.wasm32,}`, and then `wasm32-wasi-cabal build`. The process might output the following: @@ -24,4 +24,4 @@ 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 `als.wasm`. +If everything works properly, it should build a binary `als.wasm`. diff --git a/agda-language-server.cabal b/agda-language-server.cabal index a4865f7..6ae6362 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -82,6 +82,8 @@ library PatternSynonyms TypeOperators ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans + if !arch(wasm32) + ghc-options: -threaded -with-rtsopts=-N build-depends: Agda , aeson @@ -126,6 +128,8 @@ executable als PatternSynonyms TypeOperators ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans + if !arch(wasm32) + ghc-options: -threaded -with-rtsopts=-N build-depends: Agda , aeson @@ -197,6 +201,8 @@ test-suite als-test PatternSynonyms TypeOperators ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans + if !arch(wasm32) + ghc-options: -threaded -with-rtsopts=-N build-depends: Agda , aeson diff --git a/cabal.project b/cabal.project.wasm32 similarity index 100% rename from cabal.project rename to cabal.project.wasm32 diff --git a/src/Options.hs b/src/Options.hs index e77a432..27c0da3 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -77,7 +77,7 @@ versionNumber = 5 versionString :: String versionString = #ifdef wasm32_HOST_ARCH - "Agda v2.7.0.1 Language Server (WebAssembly build) v" <> show versionNumber + "Agda v2.7.0.1 Language Server v" <> show versionNumber <> " (WebAssembly build)" #elif MIN_VERSION_Agda(2,7,0) "Agda v2.7.0.1 Language Server v" <> show versionNumber #elif MIN_VERSION_Agda(2,6,4) diff --git a/src/Server.hs b/src/Server.hs index e92225e..b7c2b54 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -50,10 +50,10 @@ run options = do -- Switchboard.destroy switchboard return 0 Nothing -> do - #if defined(wasm32_HOST_ARCH) +#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.") - #endif +#endif runServer (serverDefn options) where serverDefn :: Options -> ServerDefinition Config From acc099355f9dee684dfa54da74946ef6fb454d23 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Wed, 23 Jul 2025 12:43:08 +0800 Subject: [PATCH 2/3] Set wasm workflow trigger condition --- .github/workflows/wasm.yaml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml index 9b3495d..f32f5e4 100644 --- a/.github/workflows/wasm.yaml +++ b/.github/workflows/wasm.yaml @@ -1,6 +1,12 @@ name: Compile WASM -on: [push, pull_request, workflow_dispatch] +on: + push: + branches: [master, ci-*, ci] + tags: + - 'v*' # Push events to matching v*, i.e. v1.0, v20.15.10 + pull_request: + branches: [master] env: GHC_WASM_META_FLAVOUR: '9.10' From 1c6425d30d0b1378a38e89d12ef9494fc051c634 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Wed, 23 Jul 2025 13:56:20 +0800 Subject: [PATCH 3/3] Add optimise-heavily flag to Agda for WASM --- cabal.project.wasm32 | 2 ++ 1 file changed, 2 insertions(+) diff --git a/cabal.project.wasm32 b/cabal.project.wasm32 index 78a8cd0..8e8c994 100644 --- a/cabal.project.wasm32 +++ b/cabal.project.wasm32 @@ -6,3 +6,5 @@ packages: wasm-submodules/network-simple-0.4.2 wasm-submodules/lsp/lsp-types +package Agda + flags: +optimise-heavily