Gentlemen,

I apologize I should of been more specific at the tasks that I was trying
to accomplish and in describing where I am at so far.

It seems the first point of business though from what Rob is saying is
actually getting the specifications into the ProofPower environment, which
at this point sounds like it needs to be done by hand, but I will explain
it more closely Rob. That way you can tell me if I got a shot of importing
them or if I am going to have to do a hand rewrite.

So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I
have written all my specifications in there so far. It is a fabulous
writing tool, interfacing so well with Word, and providing all the
structure I need to write the specifications I am working on. Now, I am not
sure if you are aware of this, but the latest version of the Z Word Tools
no longer requires an export of the specification to be used with FUZZ or
CZT, those checkers are built right into the tool now and allow for
typechecking of the specification as you are writing it, using either
checker. Now of course, neither of these checkers run on .doc / .docx
format files, and there are a whole host of other files generated when you
save or run a check, including a LaTeX file of the specification. I was
wondering if you thought this LaTeX file would be possible to import into
the ProofPower system, or does it have to be in a special format of .tex to
be of any use?

I have attached one of the specifications I was originally using to learn Z
Word Tools, and it has passed all the typecheckers. This is the LaTeX file
that is generated for the specification.

Thanks,
Jon


On Mon, Aug 13, 2012 at 10:59 AM, Roger Bishop Jones <r...@rbjones.com>wrote:

> On Monday 13 Aug 2012 13:12, Rob Arthan wrote:
>
> > 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).
>
> That's all very interesting, and it would be good to get
> ProofPower into a less eccentric position on document
> formats.
>
> I have myself recently found myself using utf8 in LaTeX
> documents (when I wanted to get some Greek in), and may find
> myself wanting to prepare documents which have both Greek
> and ProofPower as a result of furthering my modelling of
> aspects of Aristotle's Organon and Metaphysics.
>
> I see from reading a little about this in either or both of
> emacs and PERL that the support of arbitary encodings rather
> than specifically of one or more of the UTF variants seems to
> be thought desirable (and is realised I think in emacs).
> From this point of view one might consider making the
> ProofPower encoding "respectable" by doing whatever is
> needed for it to be supported by such generic software.
> It might then be possible to convert between ProofPower's
> encoding and others using some standard generic utility
> (perhaps emacs does this).
> [On further grubbing around I think the "generic" facilities
> support a fixed, if perhaps long, list of encodings.
> I haven't found anything which appears to work from a soft
> definition of an encoding.]
>
> Somewhere in this maze I think there are ways of telling
> that the greek alphabet does consist of alphabetic
> characters and hence perhaps should be admitted in
> ProofPower identifiers.
>
> When you speak of "my UTF8 format", presumably you are
> talking about the mapping between the ProofPower extended
> characters and the unicode character codes (which wouldn't
> be specific to UTF8).
>
> Incidentally, my hacks for making HTML from ProofPower
> sources, though they once translated into image references,
> were switched a while back to use unicode entities (not UTF
> but ascii things like &#xxxx;) so I do have a mapping
> between the two (though incomplete).
> Not good enough to be of any help to you, but I would fall
> in line with whatever mapping you have come up with if I
> ever find myself augmenting or fixing it.
>
> Roger
>
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>

Attachment: Elevator_Zed_Tools_V1.tex
Description: TeX document

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

Reply via email to