path: root/todo

-*- mode:outline -*-

$Id$

* Priorities
============
A (High)   to be fixed before release (Version 2.0)
B (Medium) desirable to fix at some point
C (Low)    probably not worth wasting time on

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

A Remove defunct "isabelle" directory.  All collbarators must
  synchronize and remove their working directories to do this,
  because we need to operate on the repository directly.
  (da, 5min).

A Documentation for proof-mode and its derived modes.  (5min)

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)
  
B 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)

B 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)

A Add a small script "example.l" etc to each of the prover subdirectories,
  for testing/example purposes.  (Perhaps proving the same thing?
  commutativity of conjunction?) 
  Only needed for Coq now.
  (10min, tms)

B Prune dead code.  (1h)

B 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)						   
				    
B 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.

B 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.
  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)

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

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

    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)

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

B Technical documentation to record expertise and allow users of other
  proof systems to adopt generic package (40h hhg & tms)

B Support for x-symbols package 

C XEmacs sessions seem to grow excessively in terms of memory
  allocation. Perhaps some of the spans aren't removed properly?
  Setting a limit on the size of the process buffer doesn't seem to
  help. 

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) (30min tms)

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

A Replace "You are not authorised for this information." by a proper
  documentation (2h)

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

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

C LEGO and Coq modes overwrite each other.

C 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

C Outline-mode does not work due to read-only restrictions of
  protected region

B Remove LEGO-specific code in proof.el: for example,
  proof-shell-eager-annotation-end, proof-included-files-list.
  (added by hhg)

B support font-lock in response buffer

B Response buffer: after an error message has been displayed; ensure
  that the error message is visible

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. 

B use proof buffer instead of response buffer and leave non-proof
  state output in the process buffer (1h)

B Remove duplication of variables e.g., proof-prog-name and
  lego-prog-name . (1h)

B As well as duplicated variables, we also have duplicated modes,
  which could be removed.  We never use proof-shell-mode, proof-mode,
  pbp-mode, only the derived instances.
  Shouldn't the generic interface directly *define* the derived
  version required?   (1h to fix)

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

C 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).



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

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

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

A Outsource actual pbp functionality (30min)
    (separate pbp annotations from other annotations)

C 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; tms)

C Mechanism to save object file

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 tms)

A Error messages need to be revised e.g., if an import fails, LEGO
  outputs

    Error in file: search: undefined or out of context: should
   (* closing file ./blah.l; time= 0.010000  gc= 0.0  sys= 0.0 *)
   Error: Unwinding to top-level

  but script management only prints the last line. (5h tms)

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

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

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

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

C 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 ]

B 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)


* 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

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

B 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)

B 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)

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

* Emacs19
=========

B 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 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
  and generate distributable tar.gz file, tag sources,
  compile .elc, web page (?), with release version.