path: root/todo

-*- mode:outline -*-

$Id$

* Priorities
============
A (High)   to be fixed before release (Version 2.0)
B          would be nice to fix before release of 2.0; but not crucial
D (Medium) desirable to fix at some point
X (Low)    probably not worth wasting time on

* This is a list of things which need doing in the generic interface
====================================================================

A Change mail address to proofgen@dcs.ed.ac.uk everywhere.

B Cleanup handling of proof-terminal-string.  At the moment some
  commands need to have the terminal string, some don't.
  da: I suggest removing proof-terminal-string altogether and
  adding back the semi-colons or fullstops at the specific level.
  It's not a big deal and would support other provers which
  may use a mixture of terminators, or no terminators at all.

B Investigate and improve indentation/font-locking code.
  At the moment editing .ML files in Isabelle Proof General is
  *very* slow.  Moreover the indentation is screwy.  Also
  seems screwy in LEGO/Coq PG.  (da, 2hr)

A Add support for people typing directly into the inferior process.
  The error messages are going to drive experienced Isabelle users
  mad otherwise!  Fair enough to hide the buffer from those
  dumb users "not authorized for this information", but lets not
  get in the way of experienced users.
  (da, 1hr: I'm not sure of the best way of doing this)

A proof-toolbar:  Fixup movement of point (choice of
  up and down functions).  Add toolbar to response mode too.  
  (30mins, da)

A toolbar icons: Fixup for low-colour modes again.  Improve restart
  and qed icon (30mins, da).

B toolbar icons: Automatically generate reduced and
  pressed/greyed-out versions from gimp xcf files.  Keep the
  xcf files under CVS rather than xpm files.  (2h, da)

B Better support for adding a new prover: give error messages which
  hint at what variable to set (see proof-issue-goal for example).

B Functions for next,previous input a la shell mode, but in proof
  script buffer (3h, da).

X Read-only mode of extents sometimes gets in the way: for example,
  if file changes on disk, can't reload it via usual functions.
  Can this be improved?  Always have to retract first, and that
  always leaves stuff around.

B User-level functions: 
  1. add new version of undo-until-point which behaves analogously to 
  proof-assert-next-command.
  2. make version of proof-restart-script which will start or
  restart the proof assistant as appropriate.  (It's handy to have
  a direct function to start the proof assistant).
  (1hr, da)

B Write test schedule for things to try out with a new instantiation
  of Proof General.

B Add skeleton instantiation files for a dummy prover "myassistant" to
  make it easier to add support for new assistants -- looking at
  any of the existing modes is confusing because of the
  prover-specific stuff.  Ideally it should work for one of
  the default provers as an impoverished example mode.  (2h)

X Add support for putting a locked region in processed files.

X Make process handling smarter: because Emacs is single-threaded,
  no process output can be dealt with when we are running some
  command.  This means that it would be safe to extend the 
  red region, by putting more commands on the queue.  Also it would
  be safe to implement a clever undo command which worked on the
  red region: if there are commands waiting to be processed, we
  could remove them from the queue.  If there are no commands waiting,
  we have to wait until something becomes blue to undo it by sending
  a command to the process.

A Clean up proof-assert-until-point behaviour.  At the moment we
  get an odd error if it is run in the locked region.  If point
  is on the start of a command it says "nothing to do", but if
  it is one character into the command, it asserts the whole command!
  I propose the new function proof-assert-next-command as a 
  possible alternative/additional behaviour, bound to  C-c C-RET.
  Another question is whether the point is moved afterwards or not.
  I suspect it is useful to leave point where it is, so we can
  easily edit one step in a proof, try the next few steps, then
  undo them, try a variation, etc.  As an experiment, 
  proof-assert-next-command does not advance point. 
  (da, tms/others to assess)
  
A A less drastic version of proof-restart-script would be useful:
  one that doesn't involve killing off the proof assistant process
  and restarting that -- it can take ages!  (da, 20mins)

D Code in proof.el assumes all characters with top bit set are special
  instructions to Emacs.  This is rather arrogant, and precludes proof
  systems which utilize 8-bit character sets!  Needs repair.  (3h)

D Prune dead code.  (1h)

D Add support to proof.el for *not* setting variables for
  commands which aren't supported by a prover.  For example,
  in Isabelle there is no such thing as killing a goal.
  For the minimum set of variables to cover, see FIXME's in isa.el
  (da, 1.5hrs)						   
				    
D Outsource script management features from proof.el to
  proof-script.el 		(1h)

A Write function proof-retract-file. (30min tms)
  Currently, the command ForgetMark (for LEGO) is hardwired in
  proof-steal-process.

D Improve documentation in proof.el to help porting/understanding 
  Also add notes into proof.texinfo.
  (ongoing, da).

B Fixup sources to follow Elisp conventions better.
  1. The first line of documentation of functions and
     variables should be a whole sentence.  Subsequent lines should
     *not* be indented.  See output of hyper-apropos and
     poor formatting of current comments.   (1hr)
  2. Replace defvar's by defconst's where appropriate.
     Introduce new defconsts.

A Update source documentation and manual, in particular document bugs
  and workarounds
  (4h hhg & tms & da) 

D Technical documentation to record expertise and allow users of other
  proof systems to adopt generic package (40h h)

A Implement more generic mechanism for large undos (2h tms)

    COQ: C-c u inside a Section should reset the whole section, then
         redo defns 

    LEGO: consider Discharge; perhaps unrol to the beginning of the
          module?

A Multiple files are sometimes handled incorrectly, because the
  function `proof-steal-process' cannot figure out that some files have
  already been processed. This is most likely caused by the ad-hoc
  equality test on file names. Instead, one could employ
  the built-in `file-truename' to trigger *canonical* file names.
  (1h tms)

D Implement proof-find-previous-terminator and bind it to C-c C-a
  (45min)

X Support for x-symbols package.
  Provers with sophisticated/configurable syntax should tell Emacs
  about their syntax somehow, rather than trying to duplicate
  specifications inside Emacs.

A file handling could be more robust; perhaps one should always cd to
  the directory corresponding to the script buffer (currently only
  done for the buffer which starts up the proof system). This could be 
  achieved with a hook which is not set by default. [Remember to add
  user documentation] (30min tms)

A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
  where ever possible (30 min tms)

A Reengineer *-count-undos and *-find-and-forget at generic level
  (3h)

D Allow bib-cite style clicking on Load/Import commands to go to file.

D support font-lock in goal buffer

X We need to go over to piped communication rather than ptys to fix
  the (Solaris) ^G bug. In this circumstance there's a bug in the
  eager annotation code. Document this problem so that it can be
  tested for future versions. [Currently the problem is documented in
  Email messages sent to lego]

B Introduce keybinding to save the proof e.g., in LEGO, this should
  insert "Save id" or "$Save id" depending on the name of the theorem. 
  Do the same thing for Goal, to add as a toolbar function.

B Unify toolbar and menu functions.

A use proof buffer instead of response buffer and leave non-proof
  state output in the process buffer (2h tms)

D Remove duplication of variables e.g., proof-prog-name and
  lego-prog-name for Coq and Lego. (1h)

D Fixup implementation of "spans":  Add documentation!
  (30 mins)

X Comment support is not very generic: we don't support end-of-line
  terminated comments.  Is there any case where this might be
  worthwhile?  (2h to add it).

B Make completion more generic.  For Isabelle we can build a
  completion table by querying the process, which is better than
  messing with tags.

X Write a Makefile for the distribution.  It can do things like
  install the info file properly.  The work is at the moment done
  in the RPM spec file instead.

X Ideas for efficiency improvements.  Rather than repeatedly
  re-parsing the buffer, we could parse the whole buffer *once*
  and make adjustments after edits, like font-lock.  We could
  make an extent for every command, and set it to "blue", "red"
  or "clear" as appropriate.  (This would allow proofs to be
  sent out-of-order to the proof process too, although perhaps
  that's not so nice).
  The function proof-segment-up-to could be made to cache its
  result.


* Proof-by-Pointing
===================

A Change proof by pointing (pbp) stuff into proofstate buffer stuff.

A Fixing up errors caused by pbp-generated commands; currently, script
  management unwisely assumes that pbp commands cannot fail (2h)

A Rename pbp-mode to response-mode or goals-mode (which doesn't
  support any actual proof-by-pointing) (30min) 

A Outsource actual pbp/goals functionality (30min)
  (separate pbp annotations from other annotations).
  Make a file proof-goals.el.

X pbp code doesn't quite accord with the tech report; in particular it
  decodes annotations eagerly. Lazily would be faster, and it's what
  the tech report claims
  --- djs: probably not much faster, actually.


* Here are things to be done to Lego mode
=========================================

A fix Pbp implementation (10h)

A release new version of the LEGO proof engine (4h tms)

B Equiv, Next,... aren't handled properly, because LEGO does not
  refresh the proof state. Perhaps it would be easiest to get LEGO to
  output more information in proof script mode (2h)

B LEGO should not issue warning messages triggered by the interactive
  use of the Module command when invoked by the interface e.g.,

    Lego> Module nstderror Import stderror;
    Including module nstderror
    Warning: module name "nstderror" does not equal filename ""!

  (15min)

X Mechanism to save object file

B Improve legotags. I cannot handle lists e.g., with 	

    [x,y:nat];

  it only tags x but not y. [The same problem exists for coqtags]

* Here are things to be done to Coq mode
========================================

D set proof-commands-regexp to support indentation for commands
						    (10min hhg)

D Add Patrick Loiseleur's commands to search for vernac or ml files.

X Sections and files are handled incorrectly.

A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
  correct command if I undo up to the lower lemma, but the buffer
  undoes to the upper lemma.  I.e., if I start Lemma x, then prove
  Lemma y, then finish x, and undo lemma x, then lemma y gets undone
  in the buffer as well. (45min hhg)
  [ This seems to have corrected itself... hhg ]

D Proof-by-Pointing (10h hhg)

A Add coq-add-tactic with a tactic name, which adds that tactic to the 
  undoable tactics and to the font-lock. (2h hhg)

B Improve coqtags. I cannot handle lists e.g., with 	

	Parameter x,y:nat

  it only tags x but not y. [The same problem exists for legotags]

* Here are things to be done to Isabelle Mode
=============================================

A Get basic features working:
    proof state extraction  -- okay.
    undo		    -- needs work (undoes to much).
    error detection	    -- seems okay.
    
    what else?

    Check these things:

    abort-goal-regexp

  Still get non-sequitur errors, why?

  BUG: undo after last step undoes till top of proof in
  process buffer, not in script!  

A CRUCIAL: Do something to manage .thy and .ML files coherently.
  At the moment loading one into Isabelle will force the
  processing of the other.  We could ask that users develop
  proof scripts in another kind of file entirely, or a file
  with a different name.  But that's an ugly hack.
  But what else can we do??
  (Probably answer: Isabelle needs to support non-automatic
  reading of ML file: a function "use_thy_only" ).

X Write perl scripts to generate TAGS file for ML and thy files.
  (6h, I've completely forgotten perl), or better:

D Implement completion for Isabelle using tables generated by
  the running process.

D Add useful specific commands for Isabelle.  Many could
  be added.  Would be better to merge in Isamode's menus.
  (probably a week's work to bring together Isamode and proof.el,
   making some of Isamode generic)

D Add ability to choose logic.  Maybe not necessary: can use default
  set in Isabelle settings nowadays, in the premise that most people
  stick to a particular logic?   But then no support for loading
  user-saved databases.
  (ponder this)

X New features ideas:
   1. Manage multiple proofs (markers in possibly different buffers)
	 

* Emacs19
=========

D The proof-locked-span isn't set to read-only, because overlays don't 
  have that capability.  This needs to be done with text-regions.
  (2hr hhg)

* Release
=========

A validate/fix web pages.

A remove CVS history in all files  (replace with idents $Id)

A extend Copyright to 1998

A fix INSTALL file, add COPYING note

A fix branches after renames

A write Makefile targets to build documentation formats, .elc

A write release message