[ProofPower] Problems with XPP!

[Rob Arthan]

On 1 Sep 2004, at 21:11, Thiago Carvalho de Sousa wrote:

>
> Hi friends,
>
> I've just installed ProofPower 2.7.3 in the Fedora
> Core 2 (successor of Red Hat). The installation
> process worked fine, but I'm getting the follow error
> when trying to run XPP:
>
> xpp: warning:  could not use the ProofPower font
> directory
> Warning: Cannot convert string "holnormal" to type
> FontStruct
> xpp: system error: no pseudo-terminal devices
> available
> xpp: No such device or address
>
> PP at command line works good! I'm running as root, so
> I have full rights to access ProofPower font
> directory! Has someone else experienced this issue? Or
> is it an OS  incompatible issue?
>

I think two different problems are showing up here. The first one is to 
do with fonts : xpp has tried to add the ProofPower fonts directory to 
the X Windows font path but then still cannot find the ProofPower 
fonts. If you run xpp with the PPENVDEBUG environment variable set to Y 
that may give you some clues;

PPENVDEBUG=Y xpp

The second problem about pseudo-devices is more likely to be an OS 
issue. I haven't had a go at installing ProofPower on Fedora yet. If 
you (or a friend) are good on UNIX system issues, the comments at the 
head of the file src/pterm.c may help you understand whether Fedora 
differs in any significant way from the models for setting up 
pseudo-devices that xpp knows about.

Regards,

Rob.


> By the way, for historical record, does someone knows
> what the biggest Z specification tested in the
> ProofPower?
>

I don't have any definite answers on this one. There was a verification 
condition generated by the Compliance Tool that occupied 16Mb reducing 
to a few Kb after some rewriting. ClawZ has been used to generate some 
very large specifications.

Regards,

Rob.