path: root/todo

-*- mode:outline -*-

$Id$

* Priorities
============

A  (URGENT) to be fixed immediately for next pre-release 
B           to be fixed before next release (Version 2.1)
C          would be nice to fix before release of 2.1; 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
====================================================================

B Polish ProofGeneral.texi and publish LaTeX version as an LFCS
  Technical Report.  

   * Fix page rearrangement to insert a blank page
   * Fix typos/other stuff found by Dave
   * Improve trivial and uniformative docstrings.
   * Fixup markup mistakes by editing docstrings.
   * Fix docstring magic so PROOFGENERAL_HOME is not var'd.
   * New line after first sentence of docstrings.
   * Several env variables / LEGO name stuff:: make `STUFF' be literal.
   * Update menus in texi

A BUGS to investigate:
  - Is there a catch bug on Solaris when a process shell killed?
  - There is a bizarre process bug with "\"'s on 254th character.
    This now seems to be the root cause of the Solaris bug mentioned
    later, and might be XEmacs rather than Solaris.
  - Thomas has a bizarre .emacs file which causes Seg Faults with
    Proof General and FSF Emacs.  Doesn't happen with "emacs -q".
    Investigate which package/setting he adds is to blame.
  - outline mode when proof-strict-read-only is nil ought to
    work, but there may be problems.

A Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General 
  info file into a good place.

B QUESTION: why do we have proof-shell-proof-completed-regexp's
  perhaps objectionable behaviour of forcing the response buffer?
  Would it be safe just to set the proof-shell-proof-completed flag
  and output as usual?   (The effect would be to allow Isabelle's
  completed proof message to appear in the goals buffer since it's
  marked up as a proof state output)

B proof-shell-exit has a time delay of 10 secs built-in, 
  before which the process is killed off.  
  This should be configurable to allow for proof assistants 
  which really want to do some work before exiting, for
  example writing persistent databases out or the like.
  Also this fact should be documented.

B Is it possible to let C-c C-c (SIGINT) issue additional process input?
  Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or
  rather, to fail gracefully.

B Fixup display problems.
   The window dedicated stuff is a real pain and I've
   spent ages inserting workarounds.  Why do we want it??
   The latest problem is that with
    (setq special-display-regexps
	 (cons "\\*Inferior .*-\\(goals\\|response\\)\\*"
		     special-display-regexps))
   I get the script buffer made into a dedicated buffer,
   presumably because the wrong window is selected in
   proof-display-and-keep-buffer?

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

B outline configuration should be generic  (or else documented for
  each prover separately, since not guaranteed to work for all).

B Improve behaviour when switching active scripting buffer.
  Now kill buffer function retracts partially-processed files
  and removes them from proof-included-files-list, we could
  allow switching between scripting buffers automatically,
  (perhaps with an option akin to the old "steal scripting?" idea). 
  Also we 

C Improve handling of process exiting early (see note at
  end of proof-shell-mode).  (30mins)
  
C da: Suggested improvement to interface for included files:
  Currently have two cases: processing a single file, and
  retracting which updates the included file list arbitrarily
  (but assumes that only removals are made).  A simpler and
  more general interface would be to just have the second
  case, and automatically find removed files and added files
  between two versions of proof-included-files-list and
  unlock or lock buffers appropriately.  We could provide
  a useful default function based on three regexps:
  retract-file-regexp, add-file-regexp, clear-filelist-regexp.
  Master regexp process-file-regexp would match all of
  these cases.   Could be multiple matches of the three above
  within a single process-file-regexp to avoid processing
  lots of urgent messages.  (3h)

C da: goal-hyp: this should be more generic.  At the moment, there are
  generic variables which are only used in the specific code:
  proof-shell-goal-regexp and proof-shell-assumption-regexp.
  This is confusing.  I suggest making lego-goal-hyp the
  default behaviour for proof-goal-hyp-fn a hook function.
  That will work for Isabelle too.   (15 mins)


C Process handling output.
  Handling mixtures of urgent and non-urgent messages:
  at the moment any non-urgent output *before* an urgent
  message will not be displayed in the response buffer.
  Accept this as a feature for now.

C  proof-goal-command-regexp: add this setting to coq.el.
   Rationalize use of proof-goal-command-p
   (probably can be scrapped now).  

C Improve indentation code and see why it's so slow (at
  least for Isabelle).   Enable it for particular provers if
  it works okay  (but must test in on large files).

C Regions in script buffer have nice "name" property and configurers
  have to set regexps carefully so that it works, but is it actually
  used anywhere?   What's it good for?

C ROBUSTness: deal gracefully with possibility that goals buffer is
  killed during session.   (2h)

D Add support to filter out unwanted noise from the prover by setting
  up a regular expression  proof-shell-noise-regexp (1h)

C support for templates e.g., in LEGO it would be nice if, by default, 
  fresh buffers corrsponding to file foo.l would automatically insert
  "Module foo;" (1h)

C  Remove "FIXME notes" which are just notes I've put in about old
   code in case something breaks   (da, 10mins).

C  Check on all FIXME notes.

C  automise testing procedures in etc/

C  Write proof-define-derived-mode which automatically adds a 
   call back hook somehow.  Propose this to maintainer of derived.el.
   (1.5hrs)

C  Toolbar icon for `proof-execute-minibuffer-cmd'  (1.5hrs)

C Improve web pages after suggestions in doc/notes.txt
  (da, 1.5hrs)

C proof-issue-goal should refuse to work when a proof is in progress.
  Similarly proof-issue-save should refuse to work when a proof
  hasn't been completed! Algorithm: Search the last goal and check
  length of span.  (45min)

C Bug in proof-retract-until-point when called twice in succession:
  calls backward-char at beginning of buffer.  (Should say no
  locked region, or "nothing to retract").  Problems is that
  there is a proof-locked-end, but it's at (point-min). (30min)

C Clean up proof-assert-until-point behaviour.  Discussion results:
    1.  At the moment we get an odd error if it is run in
    the locked region.    This is a bug.  Should behave same
    as proof-assert-next-command in this case (simpler) or
    give better error message.

    2.  At or before first character of proof command, "nothing to do"
    error message.  This is a bug.  Should behave same
    as proof-assert-next-command in this case.

    [1,2 have been "fixed" by rebinding C-c RET to 
     proof-assert-next-command for now, eventually 
     this may form a new version of proof-assert-until-point]

    3.  Movement and possible insertion of spaces/newlines for 
    when new commands are added to the buffer needs careful
    thought! (1h)

C Improve proof-goal-command and proof-save-command:
  `proof-goal-command' should be more flexible and support a
  placeholder for the name and the actual goal. In LEGO, we have
    Goal foo : absurd;
    ...
    Save foo;
  Perhaps functions at the generic level to make suitable
  values for the hook, e.g.,

     (setq proof-goal-command  (proof-prompt-named-goal "Goal %s :" "%s;"))

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

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

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

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

C 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, da will do for Isabelle)

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

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

C Unify toolbar and menu functions. (1h)

C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's.
  Generic problem, really: maybe CRs should be stripped, and just first
  line of multiline urgent message displayed in minibuffer.

D Perhaps goal..save sequences should be closed also by the appearance
  of a new goal, even though this may be a "broken" proof.  At the
  moment, undoing past the new goal causes errors:
  
     <goal>
     ...
     <new goal>
     ..

  Will ACS idea handle this?

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

D Multiple files: handle failures in reading ancestors.

D Provide a sensible default frame/buffer layout (4h)

D Implement mouse drag-and-drop support for selecting subterms in the
  goals buffer and copying them in a script buffer. This could be
  implemented by defining button2 in the response buffer and setting
  button2up in script buffers. (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.

D proof-find-next-terminator is too slow when it needs to parse
  a long buffer.   Generally a performance problem with
  proof-segment-up-to.
  				    
D Implement proof-find-previous-terminator and bind it to C-c C-a
  (45min)

D Implement a function to undo to the previous goal.

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

D Display management is much better than it was, but perhaps
  not quite as good as it could be.  It might be nice to
  display both the goals and response buffer occasionally
  (even with window-dedicated disabled).
  e.g. when proof-shell-erase-response-flag is non-nil
  and the goals buffer is updated: might like to still
  see what was in the response buffer.

  Oddities:  
    Response buffer doesn't get cleared after completion
    of a proof followed by retraction of whole file.
    On other cases of retraction, it does.
    Perhaps retraction should set the flag to ensure
    it's cleared.

D Fixup display of urgent messages in minibuffer: split at
  newlines so we don't get ^J's in FSF Emacs.

X Consider filtering out special annotations from shell buffer
  rather than merely making them invisible.

X Add ChangeLog to developers distribution to give them
  something more to look at.  (30mins).

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

X w3 manages to do toolbar enablers that work.  How?

X Images for splash screen: could add xpm files for logos 
  so that XEmacs displays transparent parts properly.
  (Probably not worth effort of distributing more files).

X  Customization mechanism: is there a way to make saved settings
   not be overwritten by setq's in the code?  Need to think how
   to do this, something like customize-set-variable-if-unchanged
   Otherwise no so useful for people to use customize for
   prover config settings (we'd need to shadow them all again for
   each assistant for this to work smoothly).
   Sure sign saving will fail is when you see "this option has
   been changed outside customization buffer"
   At the moment even setting config variables in a hook is tricky,
   because proof-config-done is called before the hook variables for the
   new mode are.  Our new version of define-derived-mode needs
   to address this.

X Proofs in Isabelle scripts can be non-interactive.  Non-interactive
  proofs have only one command, effectively.  It might be useful
  to find a way to integrate these into Proof General nicely.

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

X Span convenience functions for special 'type property.
  Could put these in proof.el or somewhere.

  (defsubst set-span-type-property (span val)
    "Set type property of SPAN to VAL"
    (set-span-property span 'type val))

  (defsubst span-type-property (span)
    "Get type property of SPAN"
    (span-property span 'type))

  etc.   (1hr)

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
  leaves stuff around.

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

X Remove .gif, .jpg, .xpm, .xbm files from the CVS repository.  Add 
  .cvsignore's for them instead.  Disadvantage: developers will need
  to have the Gimp installed to build them via 'make images'
  (or copy them from the latest download).   (da, 1hr)

X proof-site (da): I think it would be nice to change the architecture
  to make customization for new provers much easier.
  The standard use of 'define-derived-mode' could be invoked
  automatically in proof-site, and we could easily get away from the 
  kludge of proof-config-done and friends.
  (Compare this to the way font-lock works automatically for XEmacs
  when the right variable name is set, but for FSF Emacs you have
  to write something special).
  The objection to doing this is based on the idea that we should use
  an object-like inheritance mechanism to define the new modes.
  But if this is forgone, it might even be possible to add
  support for new assistants entirely via the customize mechanism,
  without any knowledge of elisp apart from regular expressions!

X Support a history of proof commands, with a "redo" command to
  redo undo-to-point or sequences of toolbar undo's.

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.

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

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.

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.

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]

X proof-mark-buffer-atomic marks the buffer as only containing
  comments if the first ACS is a goal-save span. This is however not a 
  problem for LEGO and Isabelle. (30 min)

X Idea for future re-engineering:
   Indirect Buffers seem to be a cunning way
   to implement the response buffer and goals buffer, since they're
   basically variants on displaying fragments of the shell buffer
   output. Unfortunately seems to be implemented only in FSFmacs at the
   moment.


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

B Change proof by pointing (pbp) stuff into proofstate buffer stuff.
  (1h tms)

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

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

B Outsource actual pbp/goals functionality (30min tmd)
  (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
=========================================

C In LEGO, apart from Goal...Save pairs, we have
  declaration...discharge pairs. See the section "Granularity of
  Atomic Commands" for a proposal on how to generalise the current
  implementation so that it can also deal with "Discharge".
  [See also the Coq problem with Sections] (6h)

C Inoking an "Expand" command produces a new proof state. But this is
  incorrectly displayed in the response buffer and not the goals
  buffer because special annotations are missing. Presumably, one
  ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the
  definition of "Expand" (see file newtop.sml [Version 1.4]). (30min)

C fix Pbp implementation (10h)

D Improve legotags. It cannot handle lists e.g., with 	

    [x,y:nat];

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

X Add support for changing directory when scripting buffer changes
  (see proof-activate-scripting-hook).  This would alleviate users
  from some messing with LEGOPATH.  (Possibly contentious).

X Mechanism to save object file


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

A* Implement multiple file handling.

C Retraction in a Section should retract to the beginning of the whole 
  section. See the section "Granularity of
  Atomic Commands" for a proposal on how to generalise the current
  implementation so that it can also deal with sections.
  [See also the LEGO problem with Discharge] (6h)

C derive a coq-response-mode from proof-response-mode; see lego.el (10min)

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

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

D Proof-by-Pointing (10h)

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

D Improve coqtags. It cannot handle lists e.g., with 	

	Parameter x,y:nat

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

X Sections and files are handled incorrectly.


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

A auto-adjust Pretty.setmargin when window is resized

A Multiple files needs careful testing.  There are cases when
  retracting asks for files to be removed which were never loaded.
  This might be harmless, but might be better cleaned up.

C derive an isa-response-mode from proof-response-mode;
  see lego.el (10min) 

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.
  (however, probably a month's work to bring together Isamode 
   and proof.el, making some of Isamode generic)

X 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 Write perl scripts to generate TAGS file for ML and thy files.
  (6h, I've completely forgotten perl), or better:

X Manage multiple proofs (markers in possibly different buffers)
	 
* FSF Emacs
===========

C `proof-zap-commas-region' does not work for Emacs 20.2 on
  lego/example.l . On *initially* fontifying the buffer,
  commas are not zapped. However, when entering text, commata are
  zapped correctly. (2h)

C proof-shell-dont-show-annotations doesn't seem to work.

* Bugs in other packages beyond our control
===========================================

. Odd behaviour of font-lock in elisp buffers when long strings
contain lines with stuff that looks lisp-ish.  e.g. "(asd . ads)"


* Release 
=========

A add links *from* Coq, Lego & Isabelle Web pages (da, tms 10 min)


* Stable version release checklist
==================================

1. Multiple file test suite for LEGO, Isabelle.  Coq example.
2. Check case with FSF Emacs
3. Check case with compiled code, for XEmacs only.
   (Wait for error reports for FSF Emacs)
4. Dates and versions updated in:
     README, doc/ProofGeneral.texi, html/download.html
5. ProofGeneral.texi docstring magic is up-to-date:
     cd doc; make magic
6. Update Emacs versions in texi, html/