[ProofPower] PP on windows

[Rob Arthan]

Gregg,

Thanks for all the info.

On Monday 23 Jan 2006 2:42 pm, Gregg Reynolds wrote:
> Rob Arthan wrote:
> > I have looked at building ProofPower on Cygwin, but my main concern at
> > that time was with the X Windows side of things. I did just about get xpp
> > working with the Lesstif libraries I seem to remember, but had some
> > problems with getting it to pick up the fonts.
>
> I haven't gotten that far yet; should be doable, but I rather dread it,
> since I've not done any X programming.  Naturally we would want to look
> at a native interface eventually.  Qt or something like that, maybe.
>
> On the subject of Xpp and extended chars.  I suspect Xpp predates the
> addition of Z chars to Unicode, no?  I see that PP supports a customized
> 8-bit encoding for specialized notation glyphs; obviously it would be
> good if PP understood utf-8 as well.

Yes, that is a long term goal and the ProofPower fonts do indeed go back long 
before the addition of the Z symbols to Unicode. A move to Unicode via UTF-8 
or whatever is one of my long term goals.


>  There's also Omega, although I
> haven't seen any dev activity on that project for years.  But it does
> support Unicode.  FYI Emacs handles unicode quite well, although I
> haven't found a font with the complete set of glyphs needed on Windows.

I think the same is true on Linux and Mac OS X. It would be nice (and not 
specific to ProofPower) if fonts supporting the Z requirements were widely 
available (currently there are quite a few gaps and Roger Jones' work on 
XML/ProofPower/HTML has to use GIFs rather than Unicode characters for a lot 
of the symbols).

>  MS Mincho has a lot of the math operators, although it's a bit ugly.
> Still I expect that once I get PP running on Windows I'll be able to use
> Emacs to write PP scripts.

Good luck ! And do let us know how you get on.

Ror ProofPower on the currently supported OSes, xpp is probably the best way 
for users who aren't utterly addicted to some other editor. As I said in an 
earlier posting, getting xpp going on Cygwin shouldn't be too hard.

>...
>
>  > Yes, please! It was simply ignorance and unfamiliarity on my part that
> >
> > resulted in the current build arrangements. What are the GNU tools for
> > building and maintaining the build environment that you use?
>
> I'm very glad to hear that, because I went slightly berzerk this weekend
> with PP.  First off, sieve is a wonderful little piece of work that
> stands on its own, so I've pulled it from the distrib and begun a
> separate project.  Since it needs a clever marketing name I'm going with
> "civl" until something better comes along.  (Aside from the puns on
> "civil" and "sieve", it has that necessary geek property of
> recursiveness:  "Civl Is Very Literate".)  You might want to pick a name
> that would send people to lemma-one, though.  Maybe "lemmaticus" or
> "lemmalit" or sth.
>
> Here are the things I'm working on:
>
> 	-Naming.  I hope you agree names like "imp096.doc" aren't optimal. I've
> split stuff out of the PPTex-related files (imp100, imp096, imp054,
> usr001, usr024, etc.) and given them readable names.
>
> 	Also, *.doc is probably not the best choice for lp texts.  Mainly
> because 99% of the world sees .doc and thinks MS Word, but also because
> an lp text isn't _a_ doc, it's a package of many docs.  So I'm using
> *.cvl for now.
> 	-Decomposition.  I think your LitProg approach is terrific, but in
> looking through the code I realized there's a problem with traditional
> "Knuthian" litprog.  That is, it works great for generating a lovely
> printed document, which is very useful for certain classes of reader -
> people new to the code, mainly. 
> But for people who want to work with
> the code - programmers, release engineers, etc - it's non-optimal.
>...

This is very interesting. I think you are actually using sieve etc. as the 
basis of something quite different from what it is actually intended for (not 
that there's anything wrong with that).

The PPTex package is atypical within the ProofPower suite in using sieve etc. 
to package up C programs and scripts and what have you. The primary purpose 
of all this stuff is for packaging formal material such as Z specs and proof 
scripts. For those it is not at all appropriate to split out the different 
kinds of source material into separate files.

If you are using the PPTex stuff to package source code, I agree with you 
about working with the code, but I only do that for PPTex (whose original 
author mainly used it to package itself as an entertaining challenge). For 
significant C programs like xpp, I just package the source in the traditional 
way.

Using code/numeric file names liek imp096.doc rather than mnemonic file names 
is actually quite convenient when you have several hundred source files, all 
of which can be thought of as items in a document library. And all of which 
have entries in a BibTex bibliography which you can quickly search to find 
out what's what (and there's a quick check list in comments in most of the 
make files).

> Refactoring, for example, is problematic.  My primary "view" of lp code
> as a programmer is through a text editor, in which case many of the lp
> appurtenances get in the way.  If I'm doing build/release engineering,
> my tools are shell stuff, editors, etc.  Files are useful as
> abstractions in both cases.

The problem is that if people don't think of the documents as documents, then 
they forget to maintain them as documents. For literate formal specification, 
having the narrative by the formalism at all times is a must.

>  IOW, there's a clash between tools:
> typesetter on one side, programming tools on the other.  A simple
> example:  if I'm working with an lp text that contains TeX, C code,
> shell code, etc. then all of the language-specific intelligence built
> into my editor - modes in the case of emacs - are pretty useless.

So maybe e-macs itself needs some improvement here if it can't support one 
file containing many kinds of stuff.

>...
> In short, I think sieve can form the basis of a superb suite of general
> LitProg tools.  I can think of some nice enhancements as well, which
> I'll outline in another post.
>
> Whaddya think?  I should have a tarball of civl/sieve by the end of the
> week.

Interesting. I think the docucentric approach has a lot going for it though.

I should also add that if I was thinking about designing anything like sieve 
today, I would find it difficult to justify not using XML and I'd hope that 
there'd be some usable XML technology out there to help. (See Roger's posting 
for more info on what he's been doing in that area).

Regards,

Rob.