[ProofPower] PP on windows

[Gregg Reynolds]

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.  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.
 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.

I also happen to have a copy of FontLab and an aging project to make a
pair (serif and sans) of usable monospaced TT fonts with complete math
and Z support.  But that'll be a while.

 > You've got much further than I did with building the ML-based stuff.
I didn't
> know how to run the Windows implementation of Poly/ML from Cygwin, and so I 
> got bogged down trying to work with SML/NJ. Unfortunately, at that time, 
> ProofPower required version 1.54 or later of SML/NJ and these didn't work on 
> Cygwin. I suspect the current version 1.57 might be better.

Haven't tried SML/NJ yet.  I hadn't even heard of Poly/ML until I found
PP, and it turns out they have a nice windows installer.

 > 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.
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.  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.  And
if I need to do some mucking around with the build process, it's hard to
see where the parts are and do different things for different parts.
BTW I realize that sieving is partially intended to deal with some of
these issues.

	So the trick is to split out the code into normal source files while
preserving lp capabilities.  Fortunately sieve provides =INCLUDE, so we
can do this.  For example, imp100.doc is "Implementation of Document
Handling Commands for Solaris 2" and it contains about a dozen shell
scripts.  Since sieving them out doesn't transform them in any way, I've
created .sh files for each, and in "utils.cvl" (renamed from
"imp100.doc" =INCLUDEd each.  Now the build process will be much simpler
and more amenable to the automation provided by GNU autotools.
	
	-Sieve view files.  For maintainability and understandability, I
recommend grouping all view specs for a category in a separate file with
a .v suffix; e.g. sml.v, tex.v.  Such files can then be included in a
master "civl.v" or the like.  I have some other ideas on cat/view as
well, but I'll save them for another post.

	-Cross-references.  The .doc files contain hardcoded cross-references
like "\cite{DS/FMU/IED/USR001}".  Ideally we would want to use URNs,
something like "urn:lemma-1:pp:intro" or the like, and then have
something like an XML catalog to resolve the URN into a file name.  I
think this would probably be pretty easy to do with a sh script.

	-Directory structure.  Breaking logical groupings out into distinct
subdirs.  For example, the shell scripts in "utils", the lp source for
e.g. sieve and findfiles into "civl", latex style files in "sty" or
"latex", etc.

I'm using the Standard GNU autotools for all this.  See my bibsonomy
page at http://www.bibsonomy.org/user/mobileink and filter on
"autotools" to get links to the docs.  Start with the Goat Book (in the
BibTeX column).  I've got a first cut working already; it wasn't nearly
as painful as I had expected.  I haven't yet audited the code for
non-portable stuff, though.

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.

-gregg