begriffs open source - acsl-example/blob - scripts/coq_errors.sh

   1 #!/bin/bash
   2
   3 set -e
   4
   5 WHY3_LIB="/home/joe/.opam/4.14.1/lib/why3/coq"
   6
   7 if [ $# -eq 0 ]; then
   8     echo "Usage: $0 path/to/proof_file.v"
   9     exit 1
  10 fi
  11
  12 PROOF_FILE_PATH="$1"
  13
  14 if [ ! -f "$PROOF_FILE_PATH" ]; then
  15     echo "Error: Proof file '$PROOF_FILE_PATH' not found"
  16     exit 1
  17 fi
  18
  19 PROOF_DIR=$(dirname "$PROOF_FILE_PATH")
  20 PROOF_FILE=$(basename "$PROOF_FILE_PATH")
  21
  22 echo "Debugging Coq proof: $PROOF_FILE_PATH"
  23 echo "Using Why3 library: $WHY3_LIB"
  24 echo "----------------------------------------"
  25
  26 cd "$PROOF_DIR"
  27
  28 # Run coqtop with the same arguments that frama-c uses
  29 coqtop -batch -R "$WHY3_LIB" Why3 -l "$PROOF_FILE"