(I replied from the wrong email address which silently fails, trying again...)

-------- Forwarded Message --------
Subject: Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24
Date: Thu, 15 Jun 2017 16:31:29 +0100
From: Phil Clayton <phil.clay...@lineone.net>
To: proofpower@lemma-one.com

Hi Mark,

On 15/06/17 10:29, Mark Adams wrote:
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 \

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

I think the system requirements just say that TeX/LaTeX is required and suggest Tex-Live or teTeX installations. The issue here is that TeX-Live is provided by several Fedora packages, presumably because it is so large, that are not all installed by default. If every Tex-Live package was installed, this wouldn't be an issue. There should have been an error message saying "can't find espf.sty" or similar in the log file for dtd017.

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?

The one with the output from processing imp002.doc, which will probably be called imp002.ldd (as this is the target mentioned in the Make error above) but could be called imp002.err. It should be the last modified file in the list given by
  ls -ltr src/*/* | tail



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/


On 15/06/17 00:39, Mark Adams wrote:

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.

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:

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.


Proofpower mailing list

Proofpower mailing list

Proofpower mailing list

Reply via email to