set -euo pipefail

# Deermine shared library extension
if [ "${OS:-}" = Windows_NT ]; then
LIB_PREFIX=
SHLIB_EXT=dll
elif [ "`uname`" = Darwin ]; then
LIB_PREFIX=lib
SHLIB_EXT=dylib
else
LIB_PREFIX=lib
SHLIB_EXT=so
fi

# Reset test
./clean.sh
lake update -q

# Build plugins
lake build
PKG=user__plugin # mangled
LIB_DIR=.lake/build/lib
check_plugin () {
  plugin=$1
  shlib=$LIB_DIR/${LIB_PREFIX}${PKG}_$plugin.$SHLIB_EXT
  test -f $shlib || {
    echo "$plugin library not found; $LIB_DIR contains:"
    ls $LIB_DIR
    exit 1
  }
}
check_plugin UserPlugin
check_plugin UserEnvPlugin
PLUGIN=$LIB_DIR/${LIB_PREFIX}${PKG}_UserPlugin.$SHLIB_EXT
ENV_PLUGIN=$LIB_DIR/${LIB_PREFIX}${PKG}_UserEnvPlugin.$SHLIB_EXT

# Expected test output
EXPECTED_OUT="Ran builtin initializer"
ENV_EXPECTED_OUT="Builtin value"

# Test plugins at elaboration-time via `lean` CLI
echo "Testing plugin load with lean CLI ..."
echo | lean --plugin=$PLUGIN --stdin 2>&1 | diff <(echo "$EXPECTED_OUT") -
lake env lean --plugin=$ENV_PLUGIN testEnvUse.lean 2>&1 | diff <(echo "$ENV_EXPECTED_OUT") -

# Test plugins at runtime via `Lean.loadPlugin`
echo "Testing plugin load with Lean.loadPlugin ..."
lean --run test.lean $PLUGIN 2>&1 | diff <(echo "$EXPECTED_OUT") -
lake env lean --run testEnv.lean $ENV_PLUGIN 2>&1 | diff <(echo "$ENV_EXPECTED_OUT") -

# Test failure to load environment plugin without `withImporting`
lean --run test.lean $ENV_PLUGIN >/dev/null 2>&1 && {
  fail "Loading environment plugin without importing succeeded unexpectedly."
} || true

# Test loading plugin with a provided initialization function
echo "Testing plugin load with a provided initialization function ..."
INIT_PLUGIN=.lake/libUserPlugin.$SHLIB_EXT
INIT_PLUGIN_FN=initialize_${PKG}_UserPlugin
cp $PLUGIN $INIT_PLUGIN
echo | lean --plugin=$INIT_PLUGIN=$INIT_PLUGIN_FN --stdin 2>&1 | diff <(echo "$EXPECTED_OUT") -

# Print success
echo "Tests completed successfully."