On Saturday 22 November 2008 09:20:56 Rob Arthan wrote:
(me)
> > Can't find anything which suggests that these
> > are configurable, any hints?
(rob)
> 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
PPHOME=/usr/local/src/pp/pp
(which is a softlink to: /usr/local/src/pp/pp2.8.1a10)
PPCOMPILER=POLYML
PPTARGETS=all
PPDOCFORMAT=PDF
So to build proofpower I just unpack the source and in the home directory do:
./configure
./install
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
expected.
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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
