diff --git a/.github/workflows/wasm.yaml b/.github/workflows/wasm.yaml new file mode 100644 index 0000000..125eee2 --- /dev/null +++ b/.github/workflows/wasm.yaml @@ -0,0 +1,140 @@ +name: Compile WASM + +on: [push, pull_request, workflow_dispatch] + +env: + GHC_WASM_META_FLAVOUR: '9.10' + GHC_WASM_META_COMMIT_HASH: '7927129e42bcd6a54b9e06e26455803fa4878261' + +jobs: + build: + name: Build + runs-on: ubuntu-22.04 + + steps: + - uses: actions/checkout@v4 + with: + path: als + submodules: recursive + + - 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" + + - name: Try to restore cached .ghc-wasm + id: ghc-wasm-cache-restore + uses: actions/cache/restore@v4 + with: + path: ~/.ghc-wasm + key: ghc-wasm-${{ env.CI_CACHE_KEY }} + + - name: Try to restore cached native cabal + id: native-cabal-cache-restore + uses: actions/cache/restore@v4 + with: + path: | + ~/.config/cabal + ~/.cache/cabal + key: native-cabal-${{ env.CI_CACHE_KEY }} + + - name: Try to restore cached dist-newstyle + id: dist-newstyle-cache-restore + uses: actions/cache/restore@v4 + with: + path: als/dist-newstyle + key: dist-newstyle-${{ env.CI_CACHE_KEY }}-${{ hashFiles('als/dist-newstyle/**') }} + restore-keys: | + dist-newstyle-${{ env.CI_CACHE_KEY }}- + + - name: Clone and setup ghc-wasm-meta + id: ghc-wasm-setup + if: steps.ghc-wasm-cache-restore.outputs.cache-matched-key == '' + run: | + mkdir ghc-wasm-meta + cd ghc-wasm-meta + git config --global init.defaultBranch dontcare + git config --global advice.detachedHead false + git init + git remote add origin https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta.git + git fetch origin ${{ env.GHC_WASM_META_COMMIT_HASH }} --depth=1 + git checkout FETCH_HEAD + FLAVOUR=${{ env.GHC_WASM_META_FLAVOUR }} ./setup.sh + + - name: Add ghc-wasm-meta to PATH + run: ~/.ghc-wasm/add_to_github_path.sh + + # setup script also updates package store near the end + - name: Update wasm32 cabal + if: steps.ghc-wasm-setup.outcome == 'success' || steps.ghc-wasm-setup.outcome == 'skipped' + run: wasm32-wasi-cabal update + + - name: Install native utilities + run: | + echo ">>> Update cabal" + ~/.ghc-wasm/cabal/bin/cabal update + 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 + working-directory: './als' + run: wasm32-wasi-cabal configure --flag=Agda-2-7-0-1 + + - 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' + 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' + with: + path: als/dist-newstyle + key: dist-newstyle-${{ env.CI_CACHE_KEY }}-${{ hashFiles('als/dist-newstyle/**') }} + + - name: Build every dependency else + working-directory: './als' + run: | + cd wasm-submodules/network + autoreconf -i + cd ../.. + wasm32-wasi-cabal build --dependencies-only + + - name: Build als + working-directory: './als' + run: | + mkdir ~/out + wasm32-wasi-cabal build + cp $(wasm32-wasi-cabal list-bin als) ~/out + + - name: Clean up native/wasm cabal logs + run: rm -rf ~/.cache/cabal/logs ~/.ghc-wasm/.cabal/logs + + - name: Cache native cabal + uses: actions/cache/save@v4 + if: steps.ghc-wasm-setup.outcome == 'success' + with: + path: | + ~/.config/cabal + ~/.cache/cabal + key: ${{ steps.native-cabal-cache-restore.outputs.cache-primary-key }} + + - name: Cache ghc-wasm-meta + uses: actions/cache/save@v4 + if: steps.ghc-wasm-setup.outcome == 'success' + with: + path: ~/.ghc-wasm + key: ${{ steps.ghc-wasm-cache-restore.outputs.cache-primary-key }} + + - name: Upload artifact + uses: actions/upload-artifact@v4 + with: + name: als + path: ~/out + include-hidden-files: true diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..c80f1dd --- /dev/null +++ b/.gitmodules @@ -0,0 +1,16 @@ +[submodule "wasm-submodules/agda"] + path = wasm-submodules/agda + url = git@github.com:agda-web/agda.git +[submodule "wasm-submodules/foundation"] + path = wasm-submodules/foundation + url = git@github.com:haskell-wasm/foundation.git +[submodule "wasm-submodules/network"] + path = wasm-submodules/network + url = https://github.com/haskell-wasm/network +[submodule "wasm-submodules/network-simple-0.4.2"] + path = wasm-submodules/network-simple-0.4.2 + url = https://github.com/k0001/network-simple +[submodule "wasm-submodules/lsp"] + path = wasm-submodules/lsp + url = git@github.com:agda-web/lsp.git + diff --git a/BUILDING_WASM.md b/BUILDING_WASM.md new file mode 100644 index 0000000..6b76b2b --- /dev/null +++ b/BUILDING_WASM.md @@ -0,0 +1,27 @@ +# How to build for WASM + +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`. + +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 `als.wasm`. diff --git a/agda-language-server.cabal b/agda-language-server.cabal index d970f61..a4865f7 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -5,7 +5,7 @@ cabal-version: 1.12 -- see: https://github.com/sol/hpack name: agda-language-server -version: 0.2.7.0.1.4 +version: 0.2.7.0.1.5 synopsis: An implementation of language server protocal (LSP) for Agda 2. description: Please see the README on GitHub at category: Development @@ -94,13 +94,12 @@ library , lsp-types >=2 , mtl , network - , network-simple + , network-simple == 0.4.2 , prettyprinter , process , stm , strict , text - , text-icu default-language: Haskell2010 if flag(Agda-2-6-3) build-depends: @@ -111,6 +110,9 @@ library 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 executable als main-is: Main.hs @@ -123,7 +125,7 @@ executable als OverloadedStrings 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 -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans + 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 build-depends: Agda , aeson @@ -137,13 +139,12 @@ executable als , lsp-types >=2 , mtl , network - , network-simple + , network-simple == 0.4.2 , prettyprinter , process , stm , strict , text - , text-icu default-language: Haskell2010 if flag(Agda-2-6-3) build-depends: @@ -195,7 +196,7 @@ test-suite als-test OverloadedStrings 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 -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans + 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 build-depends: Agda , aeson @@ -209,7 +210,7 @@ test-suite als-test , lsp-types >=2 , mtl , network - , network-simple + , network-simple == 0.4.2 , prettyprinter , process , stm @@ -219,7 +220,6 @@ test-suite als-test , tasty-hunit , tasty-quickcheck , text - , text-icu default-language: Haskell2010 if flag(Agda-2-6-3) build-depends: diff --git a/app/Main.hs b/app/Main.hs index ba3291d..dd22719 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -38,4 +38,4 @@ main = do else do _ <- run options -- _ <- run - return () \ No newline at end of file + return () diff --git a/cabal.project b/cabal.project new file mode 100644 index 0000000..78a8cd0 --- /dev/null +++ b/cabal.project @@ -0,0 +1,8 @@ +packages: + . + wasm-submodules/agda + wasm-submodules/foundation/basement + wasm-submodules/network + wasm-submodules/network-simple-0.4.2 + wasm-submodules/lsp/lsp-types + diff --git a/package.yaml b/package.yaml index 5bc37cc..63e85e4 100644 --- a/package.yaml +++ b/package.yaml @@ -68,7 +68,6 @@ dependencies: - strict - stm - text - - text-icu - process - prettyprinter diff --git a/src/Options.hs b/src/Options.hs index b0b700e..e77a432 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -76,7 +76,9 @@ versionNumber = 5 versionString :: String versionString = -#if MIN_VERSION_Agda(2,7,0) +#ifdef wasm32_HOST_ARCH + "Agda v2.7.0.1 Language Server (WebAssembly build) v" <> show versionNumber +#elif MIN_VERSION_Agda(2,7,0) "Agda v2.7.0.1 Language Server v" <> show versionNumber #elif MIN_VERSION_Agda(2,6,4) "Agda v2.6.4.3 Language Server v" <> show versionNumber diff --git a/src/Server.hs b/src/Server.hs index c9b1ffc..e92225e 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -28,6 +28,12 @@ import qualified Server.Handler as Handler import Switchboard (Switchboard, agdaCustomMethod) import qualified Switchboard +#if defined(wasm32_HOST_ARCH) +import Agda.Utils.IO (catchIO) +import System.IO (hPutStrLn, stderr) +import System.Posix.IO (stdInput, setFdOption, FdOption (..)) +#endif + -------------------------------------------------------------------------------- run :: Options -> IO Int @@ -44,6 +50,10 @@ run options = do -- Switchboard.destroy switchboard return 0 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.") + #endif runServer (serverDefn options) where serverDefn :: Options -> ServerDefinition Config diff --git a/wasm-submodules/agda b/wasm-submodules/agda new file mode 160000 index 0000000..87cac9c --- /dev/null +++ b/wasm-submodules/agda @@ -0,0 +1 @@ +Subproject commit 87cac9ce17932321dc1a0fdaed83436de22fa0aa diff --git a/wasm-submodules/foundation b/wasm-submodules/foundation new file mode 160000 index 0000000..8e6dd48 --- /dev/null +++ b/wasm-submodules/foundation @@ -0,0 +1 @@ +Subproject commit 8e6dd48527fb429c1922083a5030ef88e3d58dd3 diff --git a/wasm-submodules/lsp b/wasm-submodules/lsp new file mode 160000 index 0000000..9baf76e --- /dev/null +++ b/wasm-submodules/lsp @@ -0,0 +1 @@ +Subproject commit 9baf76e6d9965a3b6e8b3ecfcdf33c62b5628fd8 diff --git a/wasm-submodules/network b/wasm-submodules/network new file mode 160000 index 0000000..1dc8708 --- /dev/null +++ b/wasm-submodules/network @@ -0,0 +1 @@ +Subproject commit 1dc870889eee4ac733335ced4e274b4dfe8ed369 diff --git a/wasm-submodules/network-simple-0.4.2 b/wasm-submodules/network-simple-0.4.2 new file mode 160000 index 0000000..2c3ab6e --- /dev/null +++ b/wasm-submodules/network-simple-0.4.2 @@ -0,0 +1 @@ +Subproject commit 2c3ab6e7aa2a86be692c55bf6081161d83d50c34