pg


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

#!/bin/sh
# Start Proof General with the right -I options
# Use the Makefile to rebuild dependencies if needed
# Recompile the modified file after coqide editing

PWD=`pwd`
INCLUDES=`make print-includes`

make -q ${1}o || {
  make -n ${1}o | grep -v "\\b${1}\\b" | \
  (while read cmd; do
    sh -c "$cmd" || exit 2
   done)
}

COQPROGNAME="${COQBIN}coqtop"

COQPROGARGS=""
for arg in $INCLUDES; do
  case "$arg" in
    -I|-R|-as|compcert*)
      COQPROGARGS="$COQPROGARGS \"$arg\"";;
    *)
      COQPROGARGS="$COQPROGARGS \"$PWD/$arg\"";;
  esac
done

emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \
 --eval "(setq coq-prog-args '($COQPROGARGS))" $1 \
&& make ${1}o