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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
