Isamode was developed partly as a proof of concept: that writing a front end inside a new-generation Emacs is a viable way of attaining a powerful user-interface for Isabelle and similar systems. I believe this has been demonstrated by now. But improvements in the interface are certainly still possible.
Several ideas for future improvement of Isamode are included below.
Please feel free to send me comments on this list, more ideas to add, or --- even better -- offers to implement something from it!
More flexible ways of using isa-thy-use-line would be nice.
Presently it works best inside ML files: it could be linked in with
the listener or *proof* buffer (see below) in a function
isa-replay-proof which grabs a proof (interactive or
non-interactive) from an ML file into a fresh proof buffer and begins
replaying it. Ways of moving through interactive lines would be
useful (they should really be part of sml-mode).
We perhaps need logic.el and even theory.el
files for customization per-logic and per-theory. At present too much
is hard coded inside Isamode -- it would be good to have ways of
generating (at least first attempts at) rule tables from the theorem
databases, or from the HTML that is automatically generated by
Isabelle during building logics. As an alternative to introducing
more files, a special emacs section could be added to theory
files. We'd like ways of controlling and customizing the tactics that
appear in the menus and the completion table in
isa-completion-list.
We really need both logic-name and root-logic-name, the
latter used for rule tables, provers, etc. This is because people may
save logic images that are extensions of built-in logics. Also, user
logics should be provided for in a better way. Perhaps Emacs should
attempt to understand or communicate with Isabelle about the theory
tree structure and make system? Browsing of theories?
It should listen actively! A complete history of commands is a bit
too general really, particularly when it is available in the
interaction buffer, by paging backwards or using the comint history
mechanism. A better idea would be to have multiple listeners or
*proof* buffers which accumulates commands since the most
recent "goal". The push_proof commands could be interpreted to
manage several such buffers. Commands issued to Isabelle which don't
affect/reference the proofstate could be appended to a "proof
preamble" (e.g. making lists of rules, simpsets, etc). With a little
bit of help from Isabelle (see below), undo(); can be correctly
interpreted and lines deleted from the transcript as needed. Lines
might be annotated with the corresponding proof level. It can't be
perfectly robust, of course, but we should be able to do pretty well.
Suggested functions: extract-interactive-proof,
extract-batch-proof to create *proof* buffers from regions of
ML files, and a command replay-proof-step to step through each
command in an interactive proof.
Stepping backward and forward through proof levels is slow, probably
mostly due to Isabelle's pretty printer. Emacs could cache them in an
internal buffer, given an understanding of undo, etc, (or at
least, a conservative cache-flushing when the proof level is seen to
go down).
This scheme might be improved by making use of ML's type information to
help infer the rule category. Type information could prevent Emacs from
constructing an ill-typed tactic, for example, by showing the difference
between subgoal indexed tactics (int->tactic) and tactics the
apply to the whole proofstate (tactic).
Type information isn't fine enough to distinguish between the different kinds of rules, however, so a better solution would be to add the rule categories to the rule tables themselves, at the expense of added complexity in emacs lisp. This may be implemented in some future version of Isamode. (In the meantime, and at any rate, following the naming convention above for your own logics is probably a good idea). Then general ways of handling things such as LK's `pack' type may be integrated.
A different problem is the choice of the default tactic itself, given
the category of the identifier. Often you won't want to apply
fast_tac to everything of type claset! There needs to be
a more flexible way of specifying what the default tactic is (for
example, based on the last menu action).
isa-batchify could do with improving: it should be a bit more
flexible, permitting proofs starting with goal ..., and even
not ending with result (it might prompt for a rule name).
(Also, we shouldn't use replace-regexp in the function -- it
means undo doesn't work properly.)
Should probably appear a temporary buffer or the proof state window. Prompting might be in the minibuffer (or dialogue boxes?).
Is the behaviour of tactic, etc, shortcuts annoyingly inconsistent? -
should assume, resolve prems, etc, wait for RET to
submit input? Another possibility is to use the minibuffer for input
in tactic-entering functions: (or editing the current line of ML) if
the tactic menus become accessible from the Proof State buffer, the
Isabelle interaction buffer itself would become only of esoteric interest. (for
"advanced" use!).
In theory mode files; `hot spots' (that disappear when you type something into them) are nicer than minibuffer prompting, I think. But probably not worth the trouble.
Ruletable option for filtering of resolvable rules to highlight only those applicable in the current proofstate.
They're quicker to use than pull-down menus: we might have a special buffer of them (e.g. Tactics table), a special section in the ruletable buffer, or tool bars. In a tactics table we could have standard tactics, and then additional tactics on a per-logic basis. But we probably don't really want a proliferation of windows ...
We're on the way a completely mouse-driven interface. Whether you want to use a mouse or not, it should be possible to use the mouse most of the time, for simple proofs. More control keys for the interaction buffer would be useful (for example, completion on rule names after all).
Several of the improvements suggested so far would benefit from `behind the scenes' interaction with Isabelle. At the moment, the interface is fairly simple minded -- proof states are displayed in another buffer simply by removing anything from Isabelle's output that looks like a list of subgoals. It would probably be better to get Isabelle to participate actively in the interaction, writing some of the interface code in ML and sending special control sequences to Emacs. It would probably be more appropriate to site all of the rule table data, tactic names, etc, within Isabelle.
Icon bitmaps, colours, more fontification, etc, etc .... It might be good to highlight and tag completed proofs somehow, or annotate in some way. Also, implement "intelligent" filtering.
Isamode has rudimentary support for the special X fonts with symbols,
via the variable isa-use-special-font. The 8-bit input
functions provided in the Isabelle distribution are not yet integrated
(I tried them once and locked up my keyboard!). This is future work,
including automatic processing of theory files to convert between the
symbol format and the long-hand TeX-oriented names.
What ideas or improvements are missing from the above list?
What are the priorities?
What's the state of art in other theorem prover interfaces?
Which things can be done usefully and easily inside Emacs and which not?
Go to the first, previous, next, last section, table of contents.