Skip to content

Commit e48a2fc

Browse files
committed
[ git ] Merging from master with WASM stuff
2 parents 20c15ad + 9b7f1d0 commit e48a2fc

File tree

18 files changed

+310
-36
lines changed

18 files changed

+310
-36
lines changed

.github/workflows/test.yaml

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ jobs:
1919
runs-on: ${{ matrix.os }}
2020
strategy:
2121
matrix:
22-
os: [windows-latest]
23-
agda: ['Agda-2.7.0.1']
22+
os: [windows-latest, ubuntu-latest, macos-latest, macos-13]
23+
agda: ['Agda-2.7.0.1', 'Agda-2.6.4.3', 'Agda-2.6.3']
2424
fail-fast: false
2525
steps:
2626

@@ -289,10 +289,7 @@ jobs:
289289
cd zip
290290
Compress-Archive * "$($env:ARTEFACT).zip"
291291
cd ..
292-
ls zip
293292
mv zip/"$($env:ARTEFACT).zip" .
294-
ls
295-
296293
297294
- name: 🧪 Run tests
298295
run: stack test $STACK_YAML_ARG --ta --als-path=zip/als

.github/workflows/wasm.yaml

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

CHANGELOG.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,16 @@ All notable changes to this project will be documented in this file.
44

55
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
66

7+
## v0.2.7.0.1.5 - 2024-12-18
8+
9+
### Added
10+
- New command line option `--version` and `-V` for printing version information.
11+
12+
## v0.2.7.0.1.4 - 2024-12-6
13+
14+
### Changed
15+
- Target only 3 versions of Agda at a time: Agda-2.7.0.1, Agda-2.6.4.3, and Agda-2.6.3.
16+
717
## v0.2.7.0.1.3 - 2024-12-5
818

919
### Fixed

agda-language-server.cabal

Lines changed: 21 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,11 @@ 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
116+
if !arch(wasm32)
117+
ghc-options: -threaded -with-rtsopts=-N
114118

115119
executable als
116120
main-is: Main.hs
@@ -123,7 +127,7 @@ executable als
123127
OverloadedStrings
124128
PatternSynonyms
125129
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
130+
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
127131
build-depends:
128132
Agda
129133
, aeson
@@ -137,13 +141,12 @@ executable als
137141
, lsp-types >=2
138142
, mtl
139143
, network
140-
, network-simple
144+
, network-simple ==0.4.2
141145
, prettyprinter
142146
, process
143147
, stm
144148
, strict
145149
, text
146-
, text-icu
147150
default-language: Haskell2010
148151
if flag(Agda-2-6-3)
149152
build-depends:
@@ -154,6 +157,11 @@ executable als
154157
if flag(Agda-2-7-0-1)
155158
build-depends:
156159
Agda ==2.7.0.1
160+
if arch(wasm32)
161+
build-depends:
162+
unix >=2.8.0.0 && <2.9
163+
if !arch(wasm32)
164+
ghc-options: -threaded -with-rtsopts=-N
157165

158166
test-suite als-test
159167
type: exitcode-stdio-1.0
@@ -195,7 +203,7 @@ test-suite als-test
195203
OverloadedStrings
196204
PatternSynonyms
197205
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
206+
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
199207
build-depends:
200208
Agda
201209
, aeson
@@ -209,7 +217,7 @@ test-suite als-test
209217
, lsp-types >=2
210218
, mtl
211219
, network
212-
, network-simple
220+
, network-simple ==0.4.2
213221
, prettyprinter
214222
, process
215223
, stm
@@ -219,7 +227,6 @@ test-suite als-test
219227
, tasty-hunit
220228
, tasty-quickcheck
221229
, text
222-
, text-icu
223230
default-language: Haskell2010
224231
if flag(Agda-2-6-3)
225232
build-depends:
@@ -230,3 +237,8 @@ test-suite als-test
230237
if flag(Agda-2-7-0-1)
231238
build-depends:
232239
Agda ==2.7.0.1
240+
if arch(wasm32)
241+
build-depends:
242+
unix >=2.8.0.0 && <2.9
243+
if !arch(wasm32)
244+
ghc-options: -threaded -with-rtsopts=-N

app/Main.hs

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,10 @@ main = do
3232
options <- getOptionsFromArgv
3333
if optHelp options
3434
then putStrLn usageMessage
35-
else do
36-
_ <- run options
37-
-- _ <- run
38-
return ()
35+
else
36+
if optVersion options
37+
then putStrLn versionString
38+
else do
39+
_ <- run options
40+
-- _ <- run
41+
return ()

cabal.project.wasm32

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
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+
9+
package Agda
10+
flags: +optimise-heavily

0 commit comments

Comments
 (0)