[ProofPower] PP on windows

[Gregg Reynolds]

Hello,

I just discovered PP last week, and I'm enamoured.  Many thanks to M.
Arthan et al.  Fantastic work.

Believe it or not, I got the go-ahead to use Z for a minor project at
work, in a standard IT department setting.  ;)  So I'm trying to get PP
to compile and run on windows with from the Cygwin CLI with PolyML and
MkTex, in order to use it mainly as a technical documentation system
with Z support.  Has anybody built it this way?  I got through most of
the build, and then came across a problem that seems to be connected to
"docsml imp113" (.sml file empty), and then "pp_list -d polydb...etc"
resulting in

	pp:  "PolyML -r hol.polydb" exited with status 1

I'll figure it out eventually; the real reason I'm writing is because
I'm messing around with the build design.  I assume you'd like to see PP
more widely used and ported to more platforms.  If so, IMO it would be a
good thing to GNU-ize the build structure, so it looks like the kind of
package techies are accustomed to work with.  I'm doing this on my
windows machine, mainly because its a good way to learn the structure of
the system, but also because I think it would make it easier to learn
and maintain.  If you'd like to have a look at the results just let me know.

I've also found a few places where the build system can be fixed as is.
 For example, the Poly/ML command is hard-coded in various places.

I'm also keeping track of other stuff, e.g. the default directory for
Poly/ML is "Poly ML"; the spaces cause trouble in some cygwin shell
commands, so you want to remove the spaces on install.  And, the tex
installation you get from Cygwin won't work, at least not out of the
box.  But miktex (http://www.miktex.org) seems to work fine.

Let me know if you think any of this would be useful.

Thanks

-gregg