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
31
32
33
34
35
36
37
38
39
40
41
|
#!/bin/sh
if [ -e v7 ]; then
echo "Warning: v7 directory found, the files are maybe already translated";
sleep 5;
fi
echo --------- Producing v8 files in the translation directory -------------
if [ -e v8 ]; then rm -r v8; fi
if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi
cp -pr . /tmp/v7.$$
cp -pr /tmp/v7.$$ v8
cd v8
rm description toto
make clean
make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
{ echo ---- Failed to translate; exit 1; }
echo --------- Upgrading files in the translation directory ----------------
v8files=`find . -name \*.v8`
for i in $v8files; do
j=`dirname $i`/`basename $i .v8`.v
echo Upgrading $j in the translation directory
mv -u -f $i $j
done
echo --------- Recompiling v8 files in the translation directory -----------
make clean
make || { echo ---- Failed to recompile; exit 1; }
echo --------- Saving v7 files in directory v7 -----------------------------
/bin/rm -r ../v7
mv /tmp/v7.$$ ../v7
echo Saving v7 files done
echo --------- Upgrading files in current directory ------------------------
vfiles=`find . -name \*.v`
cd ..
for i in $vfiles; do
echo Upgrading $i in current directory
mv -u -f v8/$i $i
done
echo --------- Translation completed ---------------------------------------
echo Old files are in directory '"v7"'
echo New files are in current directory
echo You can now remove the translation directory '"v8"'
|
