-
Notifications
You must be signed in to change notification settings - Fork 5
/
install_MizAR_WS.sh
executable file
·183 lines (152 loc) · 6.26 KB
/
install_MizAR_WS.sh
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
#!/bin/bash
# $1= 7.8.10 $2=4.99.1005 $3=http://mws.cs.ru.nl/~mptp
# script installing MizAR for particular version of library and sources
# assumes we are in some mizwrk directory
# old copied info:
# script creating the mizar html from a mizar distro
# current dir should contain the Makefile for doing this,
# and all prerequisities required by the Makefile have to be present
ver="$1_$2"
myurl=$3
cvsver=`echo -n $1| sed -e 's/\./_/g'`
root=`pwd`
ph=/home/mptp/public_html
cgi=$ph/cgi-bin
bindir=bin$2
mycgi=$cgi/bin$2
mymml=$ph/mml$2
jobs=8
#wget ftp://mizar.uwb.edu.pl/pub/system/i386-linux/mizar-$ver-i386-linux.tar
wget ftp://mizar.uwb.edu.pl/pub/system/i386-win32/mizar-$ver-i386-win32.exe
if [ "$?" != "0" ]; then exit 1; fi
mkdir $ver
unzip mizar-$1-i386-win32.exe -d $ver
#tar xf mizar-$ver-i386-linux.tar -C$ver
cd $ver
cvs -d:pserver:[email protected]:2401/srv/cvsroot co -rver_$cvsver kernel libtools base
cd kernel
fpc -Sd -dCH_REPORT -dSCH_REPORT -Fu../base verifier.dpr
fpc -Sd -dCH_REPORT -dSCH_REPORT -Fu../base nverifier.dpr
fpc -Sd -dCH_REPORT -dSCH_REPORT -Fu../base accom.dpr
fpc -Sd -dCH_REPORT -dSCH_REPORT -Fu../base transfer.dpr
fpc -Sd -dCH_REPORT -dSCH_REPORT -Fu../base nexporter.dpr
cd ../libtools
fpc -Sd -Fu../base -Fu../kernel envget.dpr
cd ..
### TODO: fix mizf!!
### TODO: make this conditional instead of commented, compile all binaries in that case
# doing it with the windows version (not working yet):
unzip -a -o mmlfull -d mml
unzip -a -o mizdoc -d doc
unzip -a -o mizbib -d doc
unzip -a -o mizxml -d doc/xml
unzip -a -o prel -d prel
unzip -a -o abstr -d abstr
unzip -a -o mizdb1
#tar xzf mizshare.tar.gz
#tar xzf mizdoc.tar.gz
mkdir bin
#tar xzf mizbin.tar.gz -Cbin
# TODO: need addfmsg and errflag
# TODO: nverifier will disappear
cp kernel/verifier bin/verifier.bfex
cp kernel/verifier bin/verifier.std
cp kernel/nverifier bin/nverifier.std
cp kernel/accom bin/accom
cp kernel/nexporter bin/nexporter
cp kernel/nexporter bin/exporter
cp kernel/transfer bin/transfer
cp libtools/envget bin/envget
#mv bin/verifier bin/verifier.std
cd bin && ln -s verifier.bfex verifier && cd ..
mkdir $mycgi
ln -s $root/$ver/bin $mycgi/mizar
# tar xzf mizbin.tar.gz -C$mycgi
pushd /home/mptp/gitrepo/MPTP2/
git pull; if [ $? != 0 ]; then echo "fix MPTP2 repo first, exiting"; exit 1; fi
cd ../xsl4mizar
git pull; if [ $? != 0 ]; then echo "fix xsl4mizar repo first, exiting"; exit 1; fi
popd
mkdir html
sed -e 's/urban/mptp/' /home/mptp/gitrepo/MPTP2/mizsys/Makefile.4.145 > Makefile
cp -a mml miztmp
cp Makefile miztmp
export MIZFILES=`pwd`
cd miztmp
make -j $jobs allacc | tee 00acc.log
make -j $jobs allhdr | tee 00hdr.log
make -j $jobs allcmt | tee 00cmt.log
make -j $jobs allxml | tee 00xml.log
if [ "$?" != "0" ]; then exit 1; fi
make -j $jobs allxml1 | tee 00xml1.log
make -j $jobs allhtmla1 | tee 00htmla1.log
make -j $jobs allxml2 | tee 00xml2.log
if [ "$?" != "0" ]; then exit 1; fi
make -j $jobs allevl1 | tee 00evl1.log
make -j $jobs allevl2 | tee 00evl2.log
if [ "$?" != "0" ]; then exit 1; fi
make hidden.acc
make hidden.hdr
make hidden.cmt
make hidden.xml
make hidden.xml1
make hidden.htmla1
make tarski.acc
make tarski.hdr
make tarski.cmt
make tarski.xml
make tarski.xml1
make tarski.htmla1
make tarski.xml2
make -j $jobs alldco2
make tarski.dco2
for j in `ls *.htmla1| sed -e 's/.htmla1//'`; do mv $j.htmla1 ../html/$j.html; done
cd ..
mv miztmp/refs html
tar czf html_abstr.$ver.noproofs.tar.gz html
mv miztmp/proofs html
tar czf html_abstr.$ver.tar.gz html
git clone [email protected]:JUrban/MPTP2.git
# git branch --track MizAR1096 origin/MizAR1096
# git checkout MizAR1096
ln -s MPTP2 mptp
cd mptp
mkdir pl
mkdir Axioms
mkdir problems
for i in dcl2 dco2 evl2 lem2 sch2 the2 xml2; do mv ../miztmp/*.$i pl; done
cp hidden.dco2 pl/hidden.dco2
ln -s ../mml.lar mml.lar
ln -s $root/$ver $ph/$ver
ln -s $root/$ver $mymml
ln -s /home/mptp/gitrepo/xsl4mizar $ph/xsl4mizar
cp /home/mptp/gitrepo/MPTP2/MizAR/cgi-bin/bin/* $mycgi
ln -s /home/mptp/gitrepo/MPTP2/MizAR/cgi-bin/showby.cgi $mycgi/showby.cgi
ln -s /home/mptp/gitrepo/MPTP2/MizAR/cgi-bin/showtmpfile.cgi $mycgi/showtmpfile.cgi
ln -s /home/mptp/bin/vampire_1.8 $mycgi/vampire_rel2
ln -s $mymml/mptp/utils.pl $mycgi/utils.pl
sed -ie "s/^mml_dir(.*/mml_dir(\"\/home\/mptp\/mizwrk\/$ver\/MPTP2\/pl\/\")./" utils.pl
sed -ie "s/^bindir=.*/bindir=$bindir/" $mycgi/mizf
sed -ie "s/^\(.*MyUrl.*\)http:..mws.cs.ru.nl.~mptp.*/\1$myurl\2/" $mycgi/MizARconfig.pl
## this is needed in the showby.cgi, however showby now seems symlinked to the main dir??
# sed -ie "s/^\(my .MyUrl = \).http:..mws.cs.ru.nl.~mptp.;/\1'$myurl';/" $mycgi/showby.cgi
## this will fail in suse, forcing us to create a symlink to "pl" from ~mptp/bin/swipl
which swipl > /dev/null ; if [ $? != 0 ]; then echo "swipl not executable, exiting"; exit 1; fi
swipl -nodebug -A0 -L0 -G0 -T0 -q -t "[utils], mml2tptp_includes('Axioms/'), halt."
cat Axioms/*.ax > 00allmmlax
# make problems, this could use a makefile instead of parallel
cat ../mml.lar | sort -R | time nice parallel -j $jobs time "swipl -nodebug -A0 -L0 -G0 -T0 -t \"[utils], declare_mptp_predicates,load_mml_for_article({}, 'pl', []),install_index,time(mk_article_problems({},[[mizar_by,mizar_from,mizar_proof],[theorem, top_level_lemma] ],[opt_REM_SCH_CONSTS,opt_TPTP_SHORT])),halt.\""
# sublemmas with proof, now commented, about 20 minutes and 156k probs
# cat ../mml.lar | sort -R | time nice parallel -j $jobs time "swipl -nodebug -A0 -L0 -G0 -T0 -t \"[utils], declare_mptp_predicates,load_mml_for_article({}, 'pl', []),install_index,time(mk_article_problems({},[[mizar_proof],[sublemma] ],[opt_REM_SCH_CONSTS,opt_TPTP_SHORT])),halt.\""
mv problems problems_small
mkdir problems
tar czf mptp_problems_small.$ver.tar.gz problems_small
# fix bindir in mizf - done
# upon first install, files in cgi-bin need to be symlinked to MizAR/cgi-bin files
# the same for the main html file
# xsl4mizar expected in public_html - done
# ERROR: script_file `/home/mptp/public_html/cgi-bin/bin4.160.1126/utils.pl' does not exist - DONE
# Not Found: The requested URL /~mptp/cgi-bin/bin4.160.1126/showby.cgi was not found on this server. - DONE
# The requested URL /~mptp/cgi-bin/tptp/RemoteSOT1.cgi was not found on this server.
# - one-time symlink from ~/gr/MPTP2/MizAR/cgi-bin/tptp needed in ~ph/cgi-bin/tptp
# - one-time: icons in ~/ph