gen_docs

#!/usr/bin/env bash
set -e
link=0
site_root='/'
while [ "$1" != "" ]; do
    case $1 in
        -t | --target )           shift
                                target=$1
                                ;;
        -r | --source )           shift
                                source=$1
                                ;;
        -w | --web )            shift
                                site_root=$1
                                ;;
        -l | --link )    link=1
                                ;;
        * )
                                exit 1
    esac
    shift
done
if [ -z "$source" ]; then
  source=_target/deps/mathlib/
fi

args=()
if [ -n "$target" ]; then
  args+=( '-t' )
  args+=( "$target" )
fi
if [ "$link" -eq "1" ]; then
  args+=('-l')
fi

# build the file lists for mathlib and the archives
(cd "$source" && leanproject mk-all)
(cd "$source/archive" && leanproject mk-all && mv all.lean archive_all.lean)
(cd "$source/counterexamples" && leanproject mk-all && mv all.lean counterexamples_all.lean)
echo "import counterexamples_all" >> "$source/src/all.lean"
echo "import archive_all" >> "$source/src/all.lean"

# ensure the archive is on the lean path
echo "path $source/archive" >> leanpkg.path
echo "path $source/counterexamples" >> leanpkg.path
lean --run src/entrypoint.lean >export.json

python3 print_docs.py -r "$source" -w "$site_root" "${args[@]}"