Mark,

> On 16 Jun 2017, at 10:52, Mark Adams <m...@proof-technologies.com> wrote:
> 
> 
> 
>> 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.

Unfortunately, I don’t how to describe that because I don’t think know of an 
agreed standard docomposition of TeX-Live into constituent parts.

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

The  interface PolyML.install_pp was withdrawn in Poly/ML version 5.6. 
This means that ProofPower versions 3.1w6 and earlier will not work
with Poly/ML versions 5.6 and later. No currently available version of
ProofPower will work with Poly/ML version 5.7 without some kind of
patch. I will shortly be issuing a new version of ProofPower that will
work with Poly/ML 5.7 (as well as earlier versions from 5.5.1 on).

Regards,

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

Reply via email to