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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
