There was some discussion a while back about how to package offerings for a 
“contrib”
repository of ProofPower specification and proof scripts. I had a proposal that
tried to mimic how this kind of thing is done in HOL4 where you pull in theories
and supporting code by running ML commands. I now think it is better
to have a process that is closer to the way ProofPower itself
and the ProofPower case studies are packaged.

My current proposal is based on a convention for makefiles that extends
the way the makefiles for the ProofPower case studies work. Previously these
makefiles loaded the scripts into a new database made specially for the purpose.

With the new convention, you can specify a database of your own and the makefile
will load the scripts into that. I have implemented this convention in version 
3.1
of the three case studies. You can download these by following the links on:

        http://www.lemma-one.com/ProofPower/examples/

So, for example, assume you have an existing database, $HOME/wrk/mydb and
you want to load the maths case studies in it. To do this, you unpack the 
tarball
PPMathsEgs-3.1.tgz in a directory of your choice and then do:

        cd PPMathsEgs-3.1
        make -f maths_egs.mkf clean
        PPDB=$HOME/wrk/mydb make -f maths_egs.mkf load

If you wanted, you could then repeat the exercise to load one of the two Z case 
studies
into $HOME/wrk/mydb as well, provided mydb is descended from the ProofPower-Z
database, zed. Currently it is down to the user to understand this kind of 
dependency
(and to know to look in .err files to see what has gone wrong when a script has 
failed
to compile).

Any feedback and comments would be welcome. 

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to