[ProofPower] PP on windows

[Rob Arthan]

Gregg,

On Saturday 21 Jan 2006 9:45 pm, Gregg Reynolds wrote:
> Hello,
>
> I just discovered PP last week, and I'm enamoured.  Many thanks to M.
> Arthan et al.  Fantastic work.

Thank you!

>
> Believe it or not, I got the go-ahead to use Z for a minor project at
> work, in a standard IT department setting.

Well done indeed!

!  ;)  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 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 got through most of
> the build,

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.

> and then came across a problem that seems to be connected to
> "docsml imp113" (.sml file empty),

That warning is what I'd expect (imp113.doc is just a container for lots of 
little scripts, the command "docsml imp113" unpacks these and happens to give 
this warning because imp113.doc doesn't actually contain any ML code or HOL 
or Z paragraphs).

> and then "pp_list -d polydb...etc"
> resulting in
>
> 	pp:  "PolyML -r hol.polydb" exited with status 1
>
> I'll figure it out eventually; 

pp_list has a -v option which makes it put the log of the ML session onto 
standard output. That should give you more to go on.

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

Yes, indeed.

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

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

I am sure it could turn out to be very useful. Just having a working port to 
Cygwin would be great.

Regards,

Rob.