Custom Query (361 matches)
Results (79 - 81 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #198 | fixed | Prover executable not found when running without interface script | ||
| Description |
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:
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 |
|||
| #199 | fixed | Allow use of Isabelle.command to wrap commands singly | ||
| Description |
Isabelle.command allows additional "properties" to be attached to individual commands when they are processed by Isar. Example properties are file name and line number (Isabelle Position type), which are not maintained by the top-level loop, but would be useful to get error messages to include this information when processing interactively. |
|||
| #200 | fixed | Sledgehammer output broken | ||
| Description |
Output appears in Waiting for further information. |
|||
