#!/bin/bash

set -e

WHY3_LIB="/home/joe/.opam/4.14.1/lib/why3/coq"

if [ $# -eq 0 ]; then
    echo "Usage: $0 path/to/proof_file.v"
    exit 1
fi

PROOF_FILE_PATH="$1"

if [ ! -f "$PROOF_FILE_PATH" ]; then
    echo "Error: Proof file '$PROOF_FILE_PATH' not found"
    exit 1
fi

PROOF_DIR=$(dirname "$PROOF_FILE_PATH")
PROOF_FILE=$(basename "$PROOF_FILE_PATH")

echo "Debugging Coq proof: $PROOF_FILE_PATH"
echo "Using Why3 library: $WHY3_LIB"
echo "----------------------------------------"

cd "$PROOF_DIR"

# Run coqtop with the same arguments that frama-c uses
coqtop -batch -R "$WHY3_LIB" Why3 -l "$PROOF_FILE"