Skip to content

Commit 0c418fa

Browse files
banacornbanacorn
authored
[ git ] Merge pull request #32 from agda-web/wasm
Build WASM modules via cabal
2 parents 046e02b + cec3d3d commit 0c418fa

File tree

14 files changed

+219
-12
lines changed

14 files changed

+219
-12
lines changed

‎.github/workflows/wasm.yaml‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
name: Compile WASM
2+
3+
on: [push, pull_request, workflow_dispatch]
4+
5+
env:
6+
GHC_WASM_META_FLAVOUR: '9.10'
7+
GHC_WASM_META_COMMIT_HASH: '7927129e42bcd6a54b9e06e26455803fa4878261'
8+
9+
jobs:
10+
build:
11+
name: Build
12+
runs-on: ubuntu-22.04
13+
14+
steps:
15+
- uses: actions/checkout@v4
16+
with:
17+
path: als
18+
submodules: recursive
19+
20+
- name: Compute cache key
21+
run: echo "CI_CACHE_KEY=${{ runner.os }}-${{ runner.arch }}-${{ env.GHC_WASM_META_COMMIT_HASH }}-flavor-${{ env.GHC_WASM_META_FLAVOUR }}" >> "$GITHUB_ENV"
22+
23+
- name: Try to restore cached .ghc-wasm
24+
id: ghc-wasm-cache-restore
25+
uses: actions/cache/restore@v4
26+
with:
27+
path: ~/.ghc-wasm
28+
key: ghc-wasm-${{ env.CI_CACHE_KEY }}
29+
30+
- name: Try to restore cached native cabal
31+
id: native-cabal-cache-restore
32+
uses: actions/cache/restore@v4
33+
with:
34+
path: |
35+
~/.config/cabal
36+
~/.cache/cabal
37+
key: native-cabal-${{ env.CI_CACHE_KEY }}
38+
39+
- name: Try to restore cached dist-newstyle
40+
id: dist-newstyle-cache-restore
41+
uses: actions/cache/restore@v4
42+
with:
43+
path: als/dist-newstyle
44+
key: dist-newstyle-${{ env.CI_CACHE_KEY }}-${{ hashFiles('als/dist-newstyle/**') }}
45+
restore-keys: |
46+
dist-newstyle-${{ env.CI_CACHE_KEY }}-
47+
48+
- name: Clone and setup ghc-wasm-meta
49+
id: ghc-wasm-setup
50+
if: steps.ghc-wasm-cache-restore.outputs.cache-matched-key == ''
51+
run: |
52+
mkdir ghc-wasm-meta
53+
cd ghc-wasm-meta
54+
git config --global init.defaultBranch dontcare
55+
git config --global advice.detachedHead false
56+
git init
57+
git remote add origin https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta.git
58+
git fetch origin ${{ env.GHC_WASM_META_COMMIT_HASH }} --depth=1
59+
git checkout FETCH_HEAD
60+
FLAVOUR=${{ env.GHC_WASM_META_FLAVOUR }} ./setup.sh
61+
62+
- name: Add ghc-wasm-meta to PATH
63+
run: ~/.ghc-wasm/add_to_github_path.sh
64+
65+
# setup script also updates package store near the end
66+
- name: Update wasm32 cabal
67+
if: steps.ghc-wasm-setup.outcome == 'success' || steps.ghc-wasm-setup.outcome == 'skipped'
68+
run: wasm32-wasi-cabal update
69+
70+
- name: Install native utilities
71+
run: |
72+
echo ">>> Update cabal"
73+
~/.ghc-wasm/cabal/bin/cabal update
74+
echo ">>> Install alex and happy"
75+
~/.ghc-wasm/cabal/bin/cabal install alex-3.5.0.0 happy-1.20.1.1
76+
77+
- name: Run cabal configure
78+
working-directory: './als'
79+
run: wasm32-wasi-cabal configure --flag=Agda-2-7-0-1
80+
81+
- name: 'Build dep: lsp-types'
82+
uses: nick-fields/retry@v3
83+
id: build-dep-lsp-types
84+
with:
85+
timeout_minutes: 10
86+
max_attempts: 2
87+
command: cd als && wasm32-wasi-cabal build lib:lsp-types
88+
89+
- name: 'Build dep: agda'
90+
id: build-dep-agda
91+
working-directory: './als'
92+
run: wasm32-wasi-cabal build lib:agda
93+
94+
- name: Cache dist-newstyle
95+
uses: actions/cache/save@v4
96+
if: steps.build-dep-lsp-types.outcome == 'success' && steps.build-dep-agda.outcome == 'success'
97+
with:
98+
path: als/dist-newstyle
99+
key: dist-newstyle-${{ env.CI_CACHE_KEY }}-${{ hashFiles('als/dist-newstyle/**') }}
100+
101+
- name: Build every dependency else
102+
working-directory: './als'
103+
run: |
104+
cd wasm-submodules/network
105+
autoreconf -i
106+
cd ../..
107+
wasm32-wasi-cabal build --dependencies-only
108+
109+
- name: Build als
110+
working-directory: './als'
111+
run: |
112+
mkdir ~/out
113+
wasm32-wasi-cabal build
114+
cp $(wasm32-wasi-cabal list-bin als) ~/out
115+
116+
- name: Clean up native/wasm cabal logs
117+
run: rm -rf ~/.cache/cabal/logs ~/.ghc-wasm/.cabal/logs
118+
119+
- name: Cache native cabal
120+
uses: actions/cache/save@v4
121+
if: steps.ghc-wasm-setup.outcome == 'success'
122+
with:
123+
path: |
124+
~/.config/cabal
125+
~/.cache/cabal
126+
key: ${{ steps.native-cabal-cache-restore.outputs.cache-primary-key }}
127+
128+
- name: Cache ghc-wasm-meta
129+
uses: actions/cache/save@v4
130+
if: steps.ghc-wasm-setup.outcome == 'success'
131+
with:
132+
path: ~/.ghc-wasm
133+
key: ${{ steps.ghc-wasm-cache-restore.outputs.cache-primary-key }}
134+
135+
- name: Upload artifact
136+
uses: actions/upload-artifact@v4
137+
with:
138+
name: als
139+
path: ~/out
140+
include-hidden-files: true

‎.gitmodules‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
[submodule "wasm-submodules/agda"]
2+
path = wasm-submodules/agda
3+
url = [email protected]:agda-web/agda.git
4+
[submodule "wasm-submodules/foundation"]
5+
path = wasm-submodules/foundation
6+
url = [email protected]:haskell-wasm/foundation.git
7+
[submodule "wasm-submodules/network"]
8+
path = wasm-submodules/network
9+
url = https://github.com/haskell-wasm/network
10+
[submodule "wasm-submodules/network-simple-0.4.2"]
11+
path = wasm-submodules/network-simple-0.4.2
12+
url = https://github.com/k0001/network-simple
13+
[submodule "wasm-submodules/lsp"]
14+
path = wasm-submodules/lsp
15+
url = [email protected]:agda-web/lsp.git
16+

‎BUILDING_WASM.md‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
# How to build for WASM
2+
3+
1. Setup a working ghc (tested with v9.10) with WASM backend and wasm32-wasi-cabal.
4+
2. `cd` into `wasm-submodules/network` and run `autoreconf -i`.
5+
3. In the project root, run `wasm32-wasi-cabal build`.
6+
7+
The process might output the following:
8+
9+
```
10+
[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 )
11+
12+
wasm://wasm/001e3c92:1
13+
14+
15+
RuntimeError: table index is out of bounds
16+
at wasm://wasm/001e3c92:wasm-function[586]:0x45e40
17+
at wasm://wasm/001e3c92:wasm-function[365]:0x286e1
18+
at wasm://wasm/001e3c92:wasm-function[595]:0x46135
19+
at process.processImmediate (node:internal/timers:491:21)
20+
21+
Node.js v22.14.0
22+
```
23+
24+
At this moment, you should terminate the process and run it again.
25+
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.
26+
27+
If everything works properly, it should build a `als.wasm`.

‎agda-language-server.cabal‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ cabal-version: 1.12
55
-- see: https://github.com/sol/hpack
66

77
name: agda-language-server
8-
version: 0.2.7.0.1.4
8+
version: 0.2.7.0.1.5
99
synopsis: An implementation of language server protocal (LSP) for Agda 2.
1010
description: Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme>
1111
category: Development
@@ -94,13 +94,12 @@ library
9494
, lsp-types >=2
9595
, mtl
9696
, network
97-
, network-simple
97+
, network-simple == 0.4.2
9898
, prettyprinter
9999
, process
100100
, stm
101101
, strict
102102
, text
103-
, text-icu
104103
default-language: Haskell2010
105104
if flag(Agda-2-6-3)
106105
build-depends:
@@ -111,6 +110,9 @@ library
111110
if flag(Agda-2-7-0-1)
112111
build-depends:
113112
Agda ==2.7.0.1
113+
if arch(wasm32)
114+
build-depends:
115+
unix >=2.8.0.0 && <2.9
114116

115117
executable als
116118
main-is: Main.hs
@@ -123,7 +125,7 @@ executable als
123125
OverloadedStrings
124126
PatternSynonyms
125127
TypeOperators
126-
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
128+
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
127129
build-depends:
128130
Agda
129131
, aeson
@@ -137,13 +139,12 @@ executable als
137139
, lsp-types >=2
138140
, mtl
139141
, network
140-
, network-simple
142+
, network-simple == 0.4.2
141143
, prettyprinter
142144
, process
143145
, stm
144146
, strict
145147
, text
146-
, text-icu
147148
default-language: Haskell2010
148149
if flag(Agda-2-6-3)
149150
build-depends:
@@ -195,7 +196,7 @@ test-suite als-test
195196
OverloadedStrings
196197
PatternSynonyms
197198
TypeOperators
198-
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
199+
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
199200
build-depends:
200201
Agda
201202
, aeson
@@ -209,7 +210,7 @@ test-suite als-test
209210
, lsp-types >=2
210211
, mtl
211212
, network
212-
, network-simple
213+
, network-simple == 0.4.2
213214
, prettyprinter
214215
, process
215216
, stm
@@ -219,7 +220,6 @@ test-suite als-test
219220
, tasty-hunit
220221
, tasty-quickcheck
221222
, text
222-
, text-icu
223223
default-language: Haskell2010
224224
if flag(Agda-2-6-3)
225225
build-depends:

‎app/Main.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,4 @@ main = do
3838
else do
3939
_ <- run options
4040
-- _ <- run
41-
return ()
41+
return ()

‎cabal.project‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
packages:
2+
.
3+
wasm-submodules/agda
4+
wasm-submodules/foundation/basement
5+
wasm-submodules/network
6+
wasm-submodules/network-simple-0.4.2
7+
wasm-submodules/lsp/lsp-types
8+

‎package.yaml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,6 @@ dependencies:
6868
- strict
6969
- stm
7070
- text
71-
- text-icu
7271
- process
7372
- prettyprinter
7473

‎src/Options.hs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,9 @@ versionNumber = 5
7676

7777
versionString :: String
7878
versionString =
79-
#if MIN_VERSION_Agda(2,7,0)
79+
#ifdef wasm32_HOST_ARCH
80+
"Agda v2.7.0.1 Language Server (WebAssembly build) v" <> show versionNumber
81+
#elif MIN_VERSION_Agda(2,7,0)
8082
"Agda v2.7.0.1 Language Server v" <> show versionNumber
8183
#elif MIN_VERSION_Agda(2,6,4)
8284
"Agda v2.6.4.3 Language Server v" <> show versionNumber

‎src/Server.hs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,12 @@ import qualified Server.Handler as Handler
2828
import Switchboard (Switchboard, agdaCustomMethod)
2929
import qualified Switchboard
3030

31+
#if defined(wasm32_HOST_ARCH)
32+
import Agda.Utils.IO (catchIO)
33+
import System.IO (hPutStrLn, stderr)
34+
import System.Posix.IO (stdInput, setFdOption, FdOption (..))
35+
#endif
36+
3137
--------------------------------------------------------------------------------
3238

3339
run :: Options -> IO Int
@@ -44,6 +50,10 @@ run options = do
4450
-- Switchboard.destroy switchboard
4551
return 0
4652
Nothing -> do
53+
#if defined(wasm32_HOST_ARCH)
54+
liftIO $ setFdOption stdInput NonBlockingRead True
55+
`catchIO` (\ e -> hPutStrLn stderr $ "Failed to enable nonblocking on stdin: " ++ (show e) ++ "\nThe WASM module might not behave correctly.")
56+
#endif
4757
runServer (serverDefn options)
4858
where
4959
serverDefn :: Options -> ServerDefinition Config

‎wasm-submodules/agda‎

Submodule agda added at 87cac9c

0 commit comments

Comments
 (0)