Hi Mark,
On 15/06/17 07:05, Mark Adams wrote:
Thanks very much for that Phil.
This definitely helps but I still get failure for Poly/ML 5.6..
Installing openmotif-devel clears up the Motif problem.
Regarding Poly/ML, yes when I look closer, the failure recorded in
build.log is indeed different for Poly/ML 5.5:
echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
polyc -o slrp-bin slrp-bin.o
make: polyc: Command not found
dev.mkf:174: recipe for target 'slrp-bin' failed
make: *** [slrp-bin] Error 127
So for 5.5 it's Error 127, but for 5.7 it's Error 1.
So Poly/ML 5.5 fails as expected: polyc not found. That error code is
probably from the shell.
For Poly/ML 5.7, polyc can't find the file slrp-bin.o specified as a
argument. That error code is probably from polyc.
There error codes aren't particularly useful. There is usually an error
message in the log file for the failing source file that gives more
details about what went wrong. This is usually the last file written,
which you can find with
ls -ltr src/*/* | tail
Anyway, Poly/ML 5.6 gets further in processing dev.mkf but still fails,
this time with:
doctex dtd017.doc
texdvi -b dtd017 > dtd017.dvi.ldd1 </dev/null
dev.mkf:327: recipe for target 'dtd017.dvi' failed
make: *** [dtd017.dvi] Error 1
rm dtd017.tex
I haven't yet applied the patch for ProofPower 3.1.w7 (which shouldn't
be necessary because I'm using Poly/ML 5.6).
Correct, Poly/ML 5.6 should work fine. It looks like 5.6 is failing
whilst building the documentation. Can you try the following to make
sure you have the required packages installed:
dnf install \
gcc-c++ \
texlive-latex texlive-epsf \
ed \
motif motif-devel \
libXp-devel.x86_64 \
libXext-devel.x86_64 \
libXmu-devel.x86_64 \
libXt-devel.x86_64 \
xorg-x11-fonts-misc
and see how it goes with 3.1w7.
Incidentally, if I try building ProofPower 3.1w6 with Poly/ML 5.6, I get
further still in processing dev.mkf, but it fails this time with:
Compiling (code) imp002.sml
dev.mkf:349: recipe for target 'imp002.ldd' failed
make: *** [imp002.ldd] Error 1
I don't know why 3.1w6 doesn't build with Poly/ML 5.6. What does the
log file for imp002 say?
Phil
Cheers,
Mark.
On 15/06/2017 02:27, Phil Clayton wrote:
Hi Mark,
You probably need to do
yum install openmotif-devel
to ensure that the Motif C header files are also installed.
ProofPower 3.1w7 doesn't build with Poly/ML 5.7 due to a change in the
integer types described here:
http://lemma-one.com/pipermail/proofpower_lemma-one.com/2017-May/001178.html
You would need to apply the patch in that message.
Poly/ML 5.6 should work though.
Poly/ML 5.5 is quite old and doesn't have polyc so I can't see how
ProofPower 3.1w7 can build with that version, even though the website
say that it does. There are also versions 5.5.1 and 5.5.2 which do
provide polyc.
Poly/ML release dates are as follows:
5.7 2017-05-12
5.6 2016-01-25
5.5.2 2014-05-13
5.5.1 2013-11-18
5.5 2012-09-14
See https://sourceforge.net/projects/polyml/files/polyml/
Phil
On 15/06/17 00:39, Mark Adams wrote:
Hi,
I'm getting problems installing ProofPower 3.1w7 on Fedora 24 with
Poly/ML 5.7.
The first thing that looks wrong is that, even though I have
OpenMotif installed, running ./configure complains that it can't find
it.
yum install openmotif
...
Package motif-2.3.4-11.fc24.x86_64 is already installed, skipping.
Dependencies resolved.
Nothing to do.
Complete!
./distclean
PPHOME=`pwd` PPPOLYHOME=/usr/programs/polyml/polyml-5.7 ./configure
Using /usr/programs/pp/pp-3.1w7 as the installation target directory
Using Poly/ML from /usr/programs/polyml/polyml-5.7
Using dynamic linking for Motif
WARNING: Motif installation not found
Using 50 for the size of the labelled product cache
Generating code to install the following packages: pptex dev xpp hol
zed daz
If you are happy with these settings, now run ./install to install
ProofPower.
But ./install seems to fail for another reason:
./install
OpenProofPower installation begins [Wed Jun 14 21:41:19 2017] ...
Moving to build directory /usr/programs/pp/pp-3.1w7/src
Building pptex dev xpp hol zed daz
See /usr/programs/pp/pp-3.1w7/build.log for messages
install: installation failed; see /usr/programs/pp/pp-3.1w7/build.log
for more details
Last few lines of build.log:
echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
polyc -o slrp-bin slrp-bin.o
Error: slrp-bin.o: No such file
Usage: polyc [OPTION]... [SOURCEFILE]
dev.mkf:174: recipe for target 'slrp-bin' failed
make: *** [slrp-bin] Error 1
I get the same problem if I use Poly/ML 5.5.
Regards,
Mark.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
