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
