Re: [CZT-Devel] Problem installing jEdit plugin

[Anthony H. <an...@an...>]

Dear Leo

 

Nice to hear from you --- and apologies for the delay. I was away in Brazil
on holiday in the middle of nowhere :-).

Thanks for this and several other messages - I'll consolidate replies into
one.

 

I've picked up on CZT again because of a possible need to use it. I'm also
very encouraged that there is going to be a new release and that prompts me
to try and find some time to look at the memory usage problem again. 

 

And of course trying to get back into it I've been hitting some problems
because of unfamiliarity and not having kept up with the changes - sorry to
have burdened the list with these troubles and I'm grateful for all the help
from Andrius.

 

 

--- git

 

I had a similar feeling when I started using it (through Andrius diligent
suggestion for my doing so). 

It is away better than SVN in various respects and not that difficult in
itself. A few new concepts like

push/pull/fetch, but they are natural (distributed) counterparts for
commit/update/check.

 

As I said, I don't object and haven't had any problem yet - just need to
learn it.

 

--- IDEs and CZT.jar

 

the jEdit development was meant as a testbed for how a CZT GUI would look
like / need --- if I recall correctly.

In itself jEdit came a long way since then and improved in various respects.
We keep it alive to make allow for

a light-weight IDE usage, but not all recent features have been implemented
for it.

 

Andrius is an Eclipse wizard, having worked in industry building
Eclipse-based plugins and systems. This made

the transition to Eclipse (and update over the original development by Mark
and his students) possible. 

 

Again, I insisted to keep the IDE separate (and a reflection of) the
CZT.jar, which does contain access to all

recent/new features. Eclipse has extra bells and whistles, though. They make
specification and cross referencing

much easier / smoother than in jEdit or other editor.

 

The Eclipse plugin seemed pretty nice - I'm still interested in the answer
to my question to Andrius about incremental checking and big specs in
multiple files.

 

---- release

 

Andrius recently added nightly builds, which means you can get newest
(stable) features without much fuss

(i.e. no need for long builds and/or GIT). 

 

We make a point about only pushing (new repository versions) stable versions
of features (i.e. those that passed

tests and that we have worked with in some model in practice). This way
nightly builds are reliable.

 

We plan to have a release over the summer, and Andrius is launching soon
(coming week) a new website / doc site too !

 

Yes - I think these are all really good developments and will make it a lot
better.

 

My two pence on the OZ discussion. On jEdit, you need to choose the ZCharmap
accordingly so that oz symbols are used.

You also need to change on the ZSidekick the default parser for .tex (or
.utf8) files (which is Z-Latex/Unicode) to OZ, unless

you add files with the right extension (I think .oz).  A similar story
occurs in Eclipse: you need to choose the "default compiler"

in the preferences for CZT as Z, OZ, Circus, ZEves. 

 

The only problem I had with Eclipse was the one about creating an oz8 file -
I didn't try oz I must admit as I wasn't keen on latex. I'm putting this one
on the back burner for now unless the need for it arises in which case I'll
look into it further. 

 

On the font issue, yes there was a problem with Visual Studio and the TTF
generated by font forge (which was the tool we used

to create the CZT font for Z, OZ and Circus). As Mark said I think this has
been resolved, but tests on Windows are due on our side.

In any case, installing/uninstalling it is just a matter of copying/deleting
a file from c:\windows\fonts, so shouldn't be too troublesome.

Let us know otherwise.

 

I've installed it and will let you know if I have any trouble

 

On OZ, I tried extending Andrius' Eclipse development for OZ and Circus and
got as far as having the type checker working

with the ZCharmap support under Eclipse. Missing features I know off are
syntax highlighting for example.

 

I may be interested in pursuing this but it depends on a potential customer
- I'll let you know if I really need to go forward with this.

 

On ZEves, I did try with Mark Saaltink to "revive" it, but the trouble was
change in the Canadian government civil service leading

to a "freeze" in "what to do". The bits owned by ORA canada are somewhat
available to tweak (i.e. the Z-TO-EVES and EVES-TO-Z)

and use, yet the underlying EVES prover isn't (and is unlikely to become).

 

Having said that, Mark and I started (on and off since 2008) to "redevelop"
EVES (i.e. Mark redoes it and I use/test/suggest), and we

got a version called "Z/P" (P=prover). Given EVES is close to ACL2 (with
Quantifiers), I also tried to link the Z translations back and 

forth to LISP as ACL2 but that's not as simple as I hoped.

 

I think the *key* to ZEves was its ability to turn LISP/ML-like Z
representation of the schema calculus back to a Z-LaTex/Unicode view.

I mean, it's relatively easy to go from Z to say Isabelle/HOL (i..e. see
Z/HOL, ISabelle/Z, Proof-Power-Z). The difficulty comes in bringing

back whatever the prover's result / intermediate proof is as a Z construct!
That part from ZEves is available and is what we are (Slowly)

working with. 

In practical terms, I think for now I should just assume it's dead. On
Proofpower, I am discussing with Rob Arthan the idea of a Z Word
Tools/Proofpower integration. As part of this, Rob is I think working on
making PP use Unicode - but there are as you say still issues with the fact
that you are really working in HOL all the time.

 

Many thanks for all your feedback.

 

On the memory usage question, I was thinking of starting by investigating
just what does get put on the AST. Is there an AST pretty printer or similar
that I could modify to do this?

 

Thanks

 

Anthony