forked from np/crypto-agda
-
Notifications
You must be signed in to change notification settings - Fork 5
/
runjs.sh
executable file
·46 lines (39 loc) · 992 Bytes
/
runjs.sh
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
#!/bin/bash
set -eu
HERE="$PWD"
GITHUB="$HOME"/.agda-pkg/github
INCL=(-i. -i"$HERE" -ilib)
STDLIB="$GITHUB"/agda/agda-stdlib
INCL=("${INCL[@]}" -i"$STDLIB"/src)
LIBJS="$GITHUB"/crypto-agda/agda-libjs
INCL=("${INCL[@]}" -i"$LIBJS"/lib)
NPLIB="$GITHUB"/crypto-agda/agda-nplib
INCL=("${INCL[@]}" -i"$NPLIB"/lib)
ORIG_DIR=`pwd`
BUILD=_build
mkdir -p "$BUILD"
for m in run libagda proc; do
coffee -b -c "$LIBJS/$m".coffee
cp "$LIBJS/$m".js "$BUILD"
done
main="${1:-ZK/PartialHeliosVerifier}"
if [ ! -e "$main".agda ]; then
echo "$main.agda does not exists." >>/dev/stderr
exit 1
fi
shift || :
mainmodule="${main/\//.}"
cd "$BUILD"
cat >main.agda <<EOF
module main where
open import FFI.JS using (JS!)
import $mainmodule as M using (main)
main : JS!
main = M.main
EOF
agda --js "${INCL[@]}" main.agda
echo "Running: node run.js jAgda.main $*"
#echo NODE_PATH="$HOME/node_modules:.:$LIBJS"
BUILD_DIR=`pwd`
cd "$ORIG_DIR"
NODE_PATH=":$BUILD_DIR" node $BUILD_DIR/run.js jAgda.main "$@"