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.

Also, I think the full Tex-Live installation is huge, so would be good to mention somewhere the two bits that are required, for those that don't have the full installation.

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

Here it is:

Poly/ML 5.6 Release
val it = (): unit
imp002.sml:155: error: Value or constructor (install_pp) has not been declared i
n structure PolyML
Found near
  (
let fun error_pp (...) ... = (let datatype ...; ... in ... ...; ... end) in (PolyML.install_pp) (PPCompiler.make_pp ["BasicError", ...] error_pp)
     end)
*** Fail: Fail "Static Errors" ***

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

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to