On Saturday 22 November 2008 09:20:56 Rob Arthan wrote:

> >  Can't find anything which suggests that these
> > are configurable, any hints?

> They are configured by the settings of Xpp.textTranslations and by the
> settings of the acceleratorText resources for the menu entries in
> whichever of XppKeyboard3 or XppKeyboard4 you are using.

I guess it doesn't get more obvious than that!
The non-obvious bit is how it could possibly fail to pick up the shortcuts, 
given that I don't actually touch any of the keyboard files.

Anyway the problem did go away when I edited the app-defaults directory in the 
installation to link to Keyboard4 instead of 3, even though I thought it 
should pick it up from the app-defaults in my home directory, and in any case 
they all have the accelerators in them.

Notwithstanding that I don;t know *how*, I did get the installation on my 
desktop working, and with it rebuilt MathsEgs and all my own proofs.

Then I put it on my laptop and find that I can't get MathsEgs to work (and my 
attempt to revert to 2,7 failed because I can't easily revert to the right 
version of PolyML, so my ProofPower work has now ground to a halt.)

The setup on my laptop is as follows.

Poyml 5,2,1 was installed from source and comes up with the right version when 
I type "poly",

I have the following environment variables set by my .bash_profile

        (which is a softlink to: /usr/local/src/pp/pp2.8.1a10)

So to build proofpower I just unpack the source and in the home directory do:


This seems to work OK.

Then I unpack PPMathsEgs1211.tgz in directory /usr/local/src/pp/maths_egs and 
do a make bld in the src directory.
This fails in the proof of l'hostpitals_thm1 with the message:

Exception * no rewriting occurred [rewrite_tac.26001] * raised abandoning file
 wrk066.sml at line 7856

possibly because of algebraic normalisation over the reals not behaving as 

At the head of wrk066.err it is confirmed that we are running the right 
version of ProofPower.

=== ProofPower 2.8.1a10 [HOL Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2008
Database name: /usr/local/src/pp/maths_egs/src/maths_egs

I deleted the ProofPower directory and started afresh to make sure nothing 
funny had happened but it made no difference.

the full log from the maths_egs build was:

pp_make_database -f -p hol maths_egs
pp_make_database: parent database /usr/local/src/pp/pp2.8.1a10/db/hol.polydb 
now has a frozen theory hierarchy
pp_make_database: child database maths_egs.polydb created and initialised
touch db.ldd
docsml wrk066
Compiling (code) wrk066.sml
pp: "pp-ml /usr/local/src/pp/maths_egs/src/maths_egs.polydb" exited with 
status 1
make: *** [wrk066.ldd] Error 1

Any idea what's going wrong here?

Roger Jones

Proofpower mailing list

Reply via email to