summaryrefslogtreecommitdiff
path: root/pg
blob: 924230380472d1dfbaf37d6d103b855bf4f57e99 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
#!/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`
ARCH=$PWD/`sed -n -e 's/^ARCH=//p' Makefile.config`
VARIANT=$ARCH/`sed -n -e 's/^VARIANT=//p' Makefile.config`


make -q ${1}o || {
  make -n ${1}o | grep -v "\\b${1}\\b" | \
  (while read cmd; do
    sh -c "$cmd" || exit 2
   done)
}
COQPROGNAME="coqtop"
COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\" \"-I\" \"$PWD/flocq\" \"-I\" \"$PWD/flocq/Appli\" \"-I\" \"$PWD/flocq/Calc\" \"-I\" \"$PWD/flocq/Core\" \"-I\" \"$PWD/flocq/Prop\""


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