Hi Phil,
On 15/06/2017 10:24, Phil Clayton wrote:
...
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.
It all works now. I was missing texlive-epsf. I wonder whether/where
it is documented anywhere that this is needed..
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?
Which log file?
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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
