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.

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

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

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

Reply via email to