-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add support for WebAssembly target (#4)
[This pull request against MLton](MLton/mlton#550) enables compiling to WebAssembly, so that twelf can be run from, e.g. inside a web browser. A demo can be seen at: https://jcreedcmu.github.io/twelf-wasm/ Test plan: - ensure that the make target `twelf-server-mlton` still produces a twelf-server binary - ensure that the make target `wasi` produces `bin/twelf.wasm`, when an appropriate version of `mlton` is installed. Detailed instructions for building follow. Comments on the above pull request have more details pertaining to build and install of GMP. Checked out https://github.com/agoode/mlton/tree/wasm2 at commit MLton/mlton@d2b9e5d put into `$BUILD/dev-mlton` and then did the following: ``` MLTON=$BUILD/mlton-wasm2-INSTALL cd $BUILD/dev-mlton make clean make CC=$WASISDK/bin/clang \ AR=$WASISDK/bin/ar \ RANLIB=$WASISDK/bin/ranlib \ TARGET_OS=wasi \ TARGET_ARCH=wasm32 \ TARGET=wasm32-unknown-wasi \ WITH_GMP_DIR=$BUILD/gmp-wasi-INSTALL \ PREFIX=$MLTON \ dirs runtime install-runtime cd $BUILD/dev-mlton make clean make all make PREFIX=$MLTON install cd $BUILD/twelf mlton=$BUILD/mlton-wasm2-INSTALL/bin/mlton make wasi ``` Co-authored-by: Jason Reed <[email protected]>
- Loading branch information
Showing
6 changed files
with
64 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
|
||
twelf-core-mlton.mlb | ||
twelf-wasi.sml |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,6 @@ | ||
|
||
twelf-core-mlton.mlb | ||
../src/server/sigint.sig | ||
../src/server/sigint-mlton.sml | ||
../src/server/server.sml | ||
twelf-server-mlton.sml | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
(* | ||
* | ||
* This file makes twelf into a library that can be called directly from WASI Preview 1, | ||
* which specifies an API by which WebAssembly programs can interact with the outside world. | ||
* It is somewhat like POSIX. | ||
* | ||
* https://github.com/WebAssembly/WASI/blob/main/legacy/preview1/docs.md | ||
* | ||
* It provides two entry points: | ||
* | ||
* allocate : int -> CharArray.array | ||
* expects to be called with the length of the twelf source string | ||
* we want to evaluate, so that the sml side can allocate a buffer. | ||
* The caller is then expected to write the twelf source into the | ||
* buffer returned. | ||
* | ||
* execute : unit -> unit | ||
* has the side effect of loading the string found in the allocated | ||
* buffer, which will result in various print statements. The caller | ||
* is expected to implement the WASI fd_write endpoint so that they | ||
* can see the output so printed. | ||
*) | ||
|
||
val bref: CharArray.array option ref = ref NONE | ||
|
||
val e = _export "allocate": (int -> CharArray.array) -> unit; | ||
val _ = e (fn size => | ||
let | ||
val b = CharArray.tabulate (size, fn _ => Char.chr 0) | ||
in | ||
bref := SOME b; b | ||
end) | ||
|
||
val e = _export "execute": (unit -> unit) -> unit; | ||
val _ = e (fn () => (case !bref of | ||
NONE => print "No input buffer allocated" | ||
| SOME b => (Twelf.loadString (CharArray.vector b); ()))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
structure SigINT :> SIGINT = | ||
struct | ||
|
||
fun interruptLoop (loop:unit -> unit) = | ||
let | ||
in | ||
loop () | ||
end | ||
|
||
end; |