script to compile F* code to binary

fstar-compile.sh

#!/bin/bash
set -o noclobber  # (-C) Don\'t overwrite existing files with ">".
set -o errexit    # (-e) If not interactive, exit immediately if any untested command fails.
set -o nounset    # (-u) Write a message to standard error when attempting to expand a variable that is not set, and if the shell is not interactive, exit immediately.

# parse options
usage() {
    echo "Usage: [FSTAR_HOME=...] $0 [Module.fst ...] [Module.fst.hints ...] Main.fst"
}
OPT="$(getopt --options h\? --longoptions help -- "$@")"
eval set "$OPT"
for OPT in "$@" ; do
    case $OPT in
        -h | --help | -\? ) usage ; exit ;;
        -- ) shift ; break ;;
    esac
done
if [ $# -eq 0 ] ; then
    usage 1>&2
    exit 1
fi
FSTAR_HOME="${FSTAR_HOME:-"$(dirname "$(dirname "$(realpath "$(which fstar.exe)")")")"}"

# make a temp dir
TEMPDIR="$(mktemp -d)"
atexit() {
    rm -rf "$TEMPDIR"
}
trap atexit EXIT
trap 'trap - EXIT; atexit; exit -1' INT PIPE TERM

# copy files
cp "$@" "$TEMPDIR"

# move to the temp dir
OLDPWD="$PWD"
cd "$TEMPDIR"

# see https://github.com/FStarLang/FStar/blob/master/examples/hello/Makefile
cat <<'EOF' > Makefile
include $(FSTAR_HOME)/src/gmake/z3.mk
include $(FSTAR_HOME)/src/gmake/fstar.mk
include $(FSTAR_HOME)/ulib/ml/Makefile.include

ulib: $(FSTAR_HOME)/bin/fstarlib/fstarlib.cmxa

$(FSTAR_HOME)/bin/fstarlib/fstarlib.cmxa:
	$(MAKE) -C $(ULIB_ML)

build: ulib
	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --codegen OCaml *.fst
	ls -l
	$(OCAMLOPT) -o $(NAME) $(MODULES)
EOF
NAME="$(basename "${*: -1}" .fst)".exe
make FSTAR_HOME="$FSTAR_HOME" NAME="$NAME" MODULES="$(echo "$@" | tr ' ' '\n' | sed 's/\.fst$/.ml/ ; t ; d' | tr '\n' ' ')" build

# copy the result
cp "$NAME" "$OLDPWD"

$ fstar.exe --version
F* 0.9.5.0
platform=Linux_x86_64
compiler=OCaml 4.05.0
date=2018-04-10T14:18:35+09:00
commit=cc8247b

https://github.com/FStarLang/FStar/wiki/Executing-F*-code