forked from T-Brick/lean2wasm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMain.lean
30 lines (23 loc) · 1.03 KB
/
Main.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
import Std
def using_std_test : Std.HashMap Nat String :=
Std.HashMap.empty |>.insert 5 "this was compiled into WASM!"
def msg := using_std_test.find! 5
def main (args : List String) : IO UInt32 := do
IO.println s!"Hello, {msg}!"
IO.println s!"{args}"
/- Compiling with and without `-sNODERAWFS` changes behaviour here. With it,
the current directory should be the directory that the calling shell is
in but `home/web_user` will not exist (unless you have that directory
on your system). Without that flag, the current directory should be `/`
and `/home/web_user` should exist.
Relevant emscripten docs:
- https://emscripten.org/docs/porting/files/file_systems_overview.html
- https://emscripten.org/docs/api_reference/Filesystem-API.html
-/
IO.println s!"current directory: {← IO.currentDir}"
let webuser : System.FilePath := "" / "home" / "web_user"
if ←(webuser.pathExists) then
IO.println s!"{webuser} does exist"
else
IO.println s!"{webuser} doesn't exist"
return 0