#!/bin/sh

# tested in a debian VM
# packages installed by root: build-essential zstd

# warnings:
# * holtrace-verify could easily have bugs that allow false statements to be proven
# * many such bugs have been found in other proof-checking systems
# * HOL Light has been carefully audited but those are not audits of holtrace-verify
# * even when a trace is correct, maybe it isn't proving what you expect

# recommendations:
# * take the time to run traces through authentic HOL Light
# * also audit what a trace is proving (using, e.g., holtrace2tex)
# * see https://github.com/hol-light-family/Navier_Stokes/blob/main/doc/REPORT.md

set -e
version=20250714
curl -O https://holtrace.cr.yp.to/holtrace-$version.tar.gz
tar -xzf holtrace-$version.tar.gz
cd holtrace-$version
make holtrace-verify
curl -O https://holtrace.cr.yp.to/navierstokes.50.zst
unzstd < navierstokes.50.zst | ./holtrace-verify