bootstrap

#!/usr/bin/env bash

set -e

cd "$(dirname "$0")"

source setup

LEM_ZIP="lem-$LEM_COMMIT.zip"
CAKEML_ZIP="cakeml-$CAKEML_COMMIT.zip"

if [ ! -f "$LEM_ZIP" ]; then
  echo "Downloading Lem ..."
  curl -sLo "$LEM_ZIP" "$LEM_REPOSITORY/archive/$LEM_COMMIT.zip"
fi

if [ ! -f  "$CAKEML_ZIP" ]; then
  echo "Downloading CakeML ..."
  curl -sLo "$CAKEML_ZIP" "$CAKEML_REPOSITORY/archive/$CAKEML_COMMIT.zip"
fi

RAW_TARGET="download"
TARGET="thy"
GENERATED_TARGET="$TARGET/generated"

echo "Cleaning ..."
rm -rf "$RAW_TARGET"
mkdir -p "$RAW_TARGET"
rm -rf "$GENERATED_TARGET"
mkdir -p "$GENERATED_TARGET"

echo "Unpacking Lem ..."
unzip -oq "$LEM_ZIP" -d "$RAW_TARGET"

echo "Unpacking CakeML ..."
unzip -oq "$CAKEML_ZIP" -d "$RAW_TARGET"

LEM_RAW_TARGET="download/lem-$LEM_COMMIT"
CAKEML_RAW_TARGET="download/cakeml-$CAKEML_COMMIT"

echo "Checking download ..."
if [ ! -d "$LEM_RAW_TARGET" ] || [ ! -d "$CAKEML_RAW_TARGET" ]; then
  echo "Malformed download"
  exit 1
fi

echo "Making Lem ..."
make -C "$LEM_RAW_TARGET" bin/lem

echo "Generating Lem/Isabelle libraries ..."
make -C "$LEM_RAW_TARGET/library"

echo "Checking Lem ..."
LEM_BINARY="$LEM_RAW_TARGET/bin/lem"
if [ ! -x "$LEM_BINARY" ]; then
  echo "Failed to produce Lem binary"
  exit 1
fi

echo "Copying Lem/Isabelle theories ..."
cp "$LEM_RAW_TARGET/isabelle-lib/"*.thy "$GENERATED_TARGET"

echo "Generating CakeML/Isabelle theories ..."
(
  LEM_LIBRARY="$(readlink -f "$LEM_RAW_TARGET/library")"
  LEM_BINARY="$(readlink -f "$LEM_BINARY")"
  GENERATED_TARGET="$(readlink -f "$GENERATED_TARGET")/CakeML"
  cd "$CAKEML_RAW_TARGET"
  mkdir -p "$GENERATED_TARGET"
  LEMLIB="$LEM_LIBRARY" "$LEM_BINARY" -isa -use_datatype_record -outdir "$GENERATED_TARGET" "${CAKEML_LEM_FILES[@]}"
)

echo "Patching theories ..."
for THEORY in "${CAKEML_IGNORE_THEORIES[@]}"; do
  rm "$GENERATED_TARGET/CakeML/$THEORY"
done

echo "Building theories ..."
"$ISABELLE_TOOL" build -c -o document=pdf -v "${AFP_STRING[@]}" -D "$TARGET"

echo "Success."