Prover executable not found when running without interface script

[Makarius]

Using Carbon Emacs 1.6.0 without the isar/interface script, but loading .../PG/generic/proof-site.el manually, results in a non-functional environment.

When enabling PG by vising a thy file, the location of isatool is queried as expected. Nevertheless, trying to start the prover produces this error: Searching for program: no such file or directory, isabelle

A brief look at the elisp sources reveals a slightly untidy situation: isatool and isabelle executable locations are not really corellated. With isatool available one could just do isatool getenv -b ISABELLE to get the proper isabelle executable as well, instead there are funny attempts to guess at the PATH etc.

[David Aspinall]

Works for me, but maybe because of where I've installed Isabelle, 8-).

But we want to support remote connection too, when isatool may not be found. At the moment there is only provision for running the main <PROVER>-prog-name executable remotely. And the case that some brave souls try to use an executable alone without scripts.

IMO it's useful to support PATH guessing attempts to help default installations work out-of-the-box, including ones which may be packaged according to distribution standards rather than (admittedly saner) unpack in a single location method.

As the code comments suggests, needs tidying up, but we should add the recommended call to isatool as the first and default option.

[David Aspinall]

Fixed. The choice of program name is now based on isatool by default, with an Elisp override available in isabelle-program-name-override. Only one hardwired default location for isatool is tried, $HOME/Isabelle/bin/isatool. No defaults are tried for the isabelle command.