verify

#!/bin/sh

# Verify mmfile $1 (default "set.mm")

set -eu

extra=''
top_date_skip=''
verify_markup=true

# NL = newline
NL="$(printf '\nX')"
NL="${NL%X}"

inner_commands='verify proof *'

while [ $# -gt 0 ] ; do
  case "$1" in
    --top_date_skip) shift ; top_date_skip=' /top_date_skip' ;; # Extra command
    --no-verify-markup) verify_markup=false ; shift ;;
    --extra) shift ; extra="$1"; shift ;; # Extra command
    --*) echo "Error, unknown option $1" ; exit 1 ;;
    *) break ;;
  esac
done

mmfile="${1:-'set.mm'}"

if [ "$verify_markup" = true ] ; then
  inner_commands="${inner_commands}${NL}verify markup *${top_date_skip}"
fi

if [ -n "$extra" ] ; then
  inner_commands="${inner_commands}${NL}${extra}"
fi

# Run metamath's "verify" program.  This uses a here-document to handle
# "extra" commands (since they can be blank).
run_verify () {
  metamath << COMMANDS
set echo on
set scroll continuous
read ${mmfile}
${inner_commands}
quit
COMMANDS
}

# Run verify command, tee results to a separate file so we can examine it.
run_verify | tee mm$$.log

# Get status, which is false (nonzero) if an error or warning was found.
! grep -E -q '[?]Error|[?]Warning' < mm$$.log > /dev/null
result=$?

# Remove the log, or we'll have lots of useless logs
rm mm$$.log

# Return result, which is false (nonzero) if there was a problem.
exit "$result"