#!/bin/sh
# Run from a directory containing the downloaded manifest, .elf and .lean files.
# Requires git, Python 3 and elan (https://github.com/leanprover/elan).
# Full replay can take substantial time and RAM; it is separate from the web check.
set -eu
revision=a6c827c0171acf1c284e604870933501079bcdd2
artifacts=$(pwd)
python3 - <<'PY'
import hashlib, json
from pathlib import Path
manifest = json.loads(Path('manifest.json').read_text())
assert manifest['revision'] == 'a6c827c0171acf1c284e604870933501079bcdd2'
for name, record in manifest['examples'].items():
    for suffix, key in [('elf', 'sha256'), ('lean', 'proofSha256')]:
        path = Path(f'{name}.{suffix}')
        if path.exists():
            assert hashlib.sha256(path.read_bytes()).hexdigest() == record[key], path
print('Downloaded artifact fingerprints match the manifest.')
PY
git clone https://github.com/hiloopai/silmaril-lean.git silmaril-public
cd silmaril-public
git checkout --detach "$revision"
lake exe cache get
lake --wfail build Silmaril.Process.LPS.Problems.GnuSha256sum.Close Silmaril.Process.LPS.Problems.CoreutilsLite.TrueFalse
for name in sha256 true wrong-exit wrong-output; do
    if [ -f "$artifacts/$name.lean" ]; then
        cp "$artifacts/$name.lean" Example.lean
        lake env lean -DwarningAsError=true -o Example.olean Example.lean
        # leanchecker rechecks the theorem and its imported dependency closure.
        lake env leanchecker Example
    fi
done