On 13 Aug 2012, at 02:15, Roger Bishop Jones wrote:

> On Monday 13 Aug 2012 03:24, Jon Lockhart wrote:
> 
>> I have already written the specifications in Word using Z
>> Word Tools, and they are already saved in a variety of
>> formats. I have them transferred over to my linux image.
>> What format do they need to be in for me to get to
>> import them into XPP so I can begin the proof
>> development.
> 
> ProofPower and Word don't really go together.
> ProofPower works with LaTeX documents using a special 
> encoding for non-ascii characters

> ....
> It is possible to cut out the LaTeX, but without the LaTeX 
> your ProofPower-Z source files would not be printable 
> documents and you would be maintaining two parallel sets of 
> documents, a printable set in Word and sources for 
> ProofPower in a different set of documents.

Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to 
bridging this gap. Z Word Tools allows you to prepare a Z specification inside 
a Word document and project out the Z in a format suitable for processing by 
other tools such as Fuzz or CZT.  Anthony and I have talked about adding 
ProofPower as a list of targets, but it got deferred pending some work I was 
doing on getting ProofPower to support UTF-8. I have a prototype converter from 
a UTF-8 format to the ProofPower formats, but it would require a bit of 
handcranking to get it to convert CZT input into ProofPower input. I don't know 
how much work would be involved in getting Z Word Tools to output something 
that ProofPower can eat (e.g., my UTF-8 format).

Regards,

Rob.


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

Reply via email to