Hi there,
I'm trying to install the latest of ProofPower 2.8.1a10, but I got some
problems.
The last lines of build.log that I got is:
cat install_holdemo.sh >install_holdemo
chmod a+x install_holdemo
[ -d "/usr/local/pp"/man ] || mkdir "/usr/local/pp"/man
[ -d "/usr/local/pp"/man/man1 ] || mkdir "/usr/local/pp"/man/man1
cp usr004.doc usr004.dvi usr005.dvi usr029.dvi usr013.doc usr013A.doc
usr013B.doc usr013C.doc usr013D.doc usr013E.doc usr013F.doc usr013G.doc
usr013H.doc usr013S.doc usr013X.doc usr013.dvi usr022.doc usr022.dvi
usr022S.doc usr022_slides.doc int002.doc int008.doc spc001.doc spc001.dvi
spc002.doc spc002.dvi spc003.doc spc003.dvi spc004.doc spc004.dvi spc005.doc
spc005.dvi wrk022.doc wrk022.dvi wrk043.doc wrk043.dvi wrk044.doc wrk044.dvi
wrk046.doc wrk046.dvi wrk051.doc wrk051.dvi "/usr/local/pp"/doc
cp install_holdemo "/usr/local/pp"
chmod -R a-w "/usr/local/pp"
chmod -R g-w "/usr/local/pp"
chmod -R u+w "/usr/local/pp"
cp pp_make_database.1 pp_list.1 pp.1 hol_list.1 "/usr/local/pp"/man/man1
make[1]: Leaving directory
`/home/artur/Proofpower/OpenProofPower-2.8.1a10/src'
make -f zed.mkf build </dev/null
make[1]: Entering directory
`/home/artur/Proofpower/OpenProofPower-2.8.1a10/src'
rm -f zed.polydb
cp "`findfile hol.polydb
"/home/artur/Proofpower/OpenProofPower-2.8.1a10/src"`" zed.polydb
chmod u+wr zed.polydb
echo "PPBuild.pp'save_name := \"zed\"; save_and_quit();" | pp -d zed.polydb
val it = () : unit
val it = () : unit
=== ProofPower 2.8.1a10 [HOL Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2008
Database name:
:) val it = () : unit
val it = () : unit
echo " open_theory \"fin_set\"; new_theory \"z_language\";
set_cache_theories [\"z_language\",\"hol\", \"basic_hol\"]; save_and_quit
(); " | \
PPDATABASENAME=zed "pp-ml" ""zed.polydb
val it = () : unit
val it = () : unit
=== ProofPower 2.8.1a10 [HOL Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2008
Database name: zed
:) val it = () : unit
val it = () : unit
val it = ["basic_hol"] : string list
val it = () : unit
docsml -f hol.svf dtd048
Compiling (code) dtd048.sml
docsml -f hol.svf imp048
Compiling (code) imp048.sml
pp: "pp-ml /home/artur/Proofpower/OpenProofPower-2.8.1a10/src/zed.polydb"
exited with status 1
make[1]: *** [imp048.ldd] Error 1
make[1]: Leaving directory
`/home/artur/Proofpower/OpenProofPower-2.8.1a10/src'
make: *** [zed_build] Error 2
Is this extract enough to see what is going on?
Regards,
--
Artur Oliveira Gomes
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
