On 9 Aug 2012, at 12:07, Roger Bishop Jones wrote:

> Rob,
> On Thursday 09 Aug 2012 10:26, Rob Arthan wrote:
>> I plan to make a new ProofPower release shortly. In the
>> meantime, if you want the state of the art, I uploaded
>> an experimental version built from the latest source.
>> You can find this here:
> It that any different from what you get building from the RCS 
> archive in your dropbox?

Not today, but that's just because I haven't done any new development.

> Can I build MathsEgs from that RCS?
> [actually, I just tried but I see that the makefile for 
> maths_egs isn't compliant with the pattern used in that 
> system (no inst target, and the bld target fails).

The bld target works for me, but you are certainly right that the makefiles for 
the examples don't thing into the pattern.  It would be nice to make them 
(including fef) more uniform with the main packages. If you want to look into 
that please do. It might give us some more ideas about how a ProofPower contrib 
might work. if you use RCS for your version control, I have shell scripts that 
do a repository/file level merge of one RCS repository into another.

> Seems odd that the directory in which one builds is called 
> pp and the one in which one installs is ppdev.
> Shouldn't it be the other way round?

Maybe. The names are the result of a fairly random choice of mine. I type ~/pp 
much more often than ~/ppdev, so the choice does save keyboard and finger wear 
and tear, but that is a complete accident. I should have explained that they 
are both part of the development process: specifically, when you build zed, the 
starting point is an unfrozen hol database, so things would go wrong if you 
were just picking things up from a standard installation with frozen databases.



Proofpower mailing list

Reply via email to