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
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

Reply via email to