scripts/runidris-node · Idris-dev

git.iko.soy/Idris-dev

on master help sign in

Idris-dev/scripts/runidris-node

25 lines 773 B history raw

1#!/bin/sh

3# This is a script that runs an idris program, suitable for use

4# in a shebang line. We cache the executables by naming them after

5# the SHA hash of the idris source and looking for it before

6# compiling. This is the node version.

7RUNIDRIS_DIR="${TEMP:-/tmp}/runidris-node"

8if [ ! -d $RUNIDRIS_DIR ]; then

9 mkdir $RUNIDRIS_DIR

10 chmod 700 $RUNIDRIS_DIR

13OS=`uname -s`

14case $OS in

15 OpenBSD ) TEMP_NAME="runidris-`sha1 -q $1`" ;;

16 * ) TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`" ;;

17esac

19FP="$RUNIDRIS_DIR/$TEMP_NAME"

20cp "$1" "$FP.idr" # idris won't compile the script unless it ends in .idr

21if [ ! -e "$FP.js" ]; then

22 "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." "$FP.idr" -o "$FP.js"

24shift

25node "$FP.js" "$@"