git.iko.soy/Idris-dev
on appveyor-fix help sign in
Idris-dev/scripts/runidris
25 lines 708 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
7RUNIDRIS_DIR="${TEMP:-/tmp}/runidris"
8if [ ! -d $RUNIDRIS_DIR ]; then
9 mkdir $RUNIDRIS_DIR
10 chmod 700 $RUNIDRIS_DIR
11fi
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 ]; then
22 "${IDRIS:-idris}" "$FP.idr" --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
23fi
24shift
25"$FP" "$@"