You are right that Rob is the man to answer your technical
problem, but in the meantime I might be able to help you 
round it.

"save_and_quit();" is something that I never use.

If your system otherwise seems OK then you should go right 
ahead and work through the tutorial.

Why don't I use it?

Well, whenever I am working interactively with ProofPower I 
just don't save the database.
I always have a make system in the background ready to build 
in batch mode, and this uses proofpower with the "-f" option 
to run a script and then save it.
So when I have a working script I create a new database 
using "make".
This must be possible with your system otherwise you would 
not have completed the build of ProofPower.

When I resume work on an incomplete development I will enter 
the current document with xpp picking the database with all 
prior documents loaded, and then I use "use_file" to run the 
current script through to the point of failure where I was 
last working (and I force failure by just putting "stop;" in 
the script at the point I am working).
Then I continue my interactive work.
When I have a clean document I save it and then do a make to 
create a new database.

You probably don't want to set up a makefile for working 
through the tutorial, but you can still work in a similar 
manner, i.e. instead of saving the database when you pause 
in the tutorial, just put "stop here;" in your script, save 
it, and quit xpp.
When you come back use "use_file" to run your script through 
to your current position in the tutorial.
(you will need to use docsml on the file first if it is not 
pure SML, but for the tutorial you can just work with an SML 

I presume you are looking at usr004, which is the gentlest 
introduction to ProofPower-HOL.
Alternatively you could work through the ProofPower HOL 
course usr022 with its accompanying tutorial notes usr013, 
which is less gentle but I think, more systematic and has 
greater coverage (but doesn't actually mention 

Roger Jones

Proofpower mailing list

Reply via email to