Roger, 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: >> >> http://www.lemma-one.com/ProofPower/getting/experimental/ > > 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. > VERY MINOR COMMENT > > 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. Regards, Rob. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
