path: root/TODO.developer

-*- mode:outline -*-
$Id$

This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.

=================================================================

3.7 TODOs
=========

Things to do for 3.7:

 -- move real todos onto Trac
 -- nuisance fix needed for docstring magic because of pruning of spaces 
    from empty lines in all docstrings by Stefan Monnier (argh!)
 -- merge/fix of patch by Claire Quigley (check status with Larry/Tom/whoever)
 -- Coq updates check: symbols, linewidth, file handling
 -- Complete generification of adjust-line-width function
      (currently separately in lego, isar,plastic)


=================================================================


* PGIP support
** Remove need for decorated output around PGIP responses.
** Support simplified (flat, non context-sensitive) completion for idtables
** URL parse: library from w3 is incomplete, also may clash with Emacs
   version.

* X-Symbol
** Unify versions with distributed XEmacs version
** Integrate large demo font

* Coq-8 fixup
** Fix display of sub/super scripts in Coq output
** Multiple file handling
** Automatic adjustment of line width

* Docstring magic fixups
** Some missing files
** Isabelle classic remove?

=================================================================

* Developers' Infeasibly Long Low-Level List of Things to Do


** 0. Contents

 1. Priorities
 2. Things to do in the generic interface
 3. Things to do for the documentation
 4. Emacs issues
 5. Things to do for Proof-by-Pointing
 6. Things to do for Web Pages, Distribution
 7. Future improvements to take advantage of newer Emacsen
 8. Bugs in other software beyond our control
 9. Stable version release checklist
 
    See <prover>/todo for things to do for each prover.

** 1. Priorities

A (High)	e.g. to be fixed ASAP for next pre-release 
B		e.g. to be fixed before next release
C (Medium)	e.g. would be nice to fix before next release; not crucial
D		e.g. desirable to fix at some point
X (Low)		e.g. probably not worth spending time on


** 2. Long list of things to do in the generic interface


*** B Fix-up show/hide for nested proofs.  
        (Wierdness with cursor jumping as well)

*** B Cleanup undo behaviour to cope with new Coq mechanism.

    Is the simplified mechanism better for other provers too, or does the
    split still apply?  Probably best to leave Isar as-is and have
    proof-nesting-depth left as experimental.

*** B proof-nesting-depth:
    This needs to be fixed up in count undos, find-and-forget.

*** C Add MMM for other provers where relevant/useful

*** C Further display management improvement (it's a nightmare)
    Glitches to resolve:
     -- suggestion to cache window height: could implement this
	by resize change functions (also doing the pretty-print hack?)
        which set a symbol property for associated buffer symbol
     -- longer term improvements: allow window preferences per 
	associated buffer.  Either separate frame or merged into
	switching mode.  Very messy to implement.
     -- Stuck-withs: XEmacs frames always have minibuffer.
		     GNU Emacs frames always have modelines.
     Other older comments:
      - 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.
      - check: does auto-delete-windows work with
      window-dedicated as it should? (I thought it would switch
      between 2/3 bufs as appropriate?).
      - Display buffer clearing: response buffer is cleared
      too often/eagerly, perhaps?  The output find-theorems or similar
      doesn't last beyond a single proof step.  The problem is that we
      want to erase irrelevant output from the response buffer for the
      previous proof step.  Consider making output from invisible
      command persistent.  See attempted patch in
      etc/patches/fix-attempt-for-eager-cleaning.txt


*** C Menu layout
    Would be good to try to make this uniform between version: 
    PG menu frist, then prover-specific menu.  Similarly for Imenu.

*** A PGIP SUPPORT (minimal for Isabelle patch):
      -- settings with categories

*** A Oddity: Weirdness with regions turning blue even though they
    haven't been processed.  Noticed with HOL/CCC experimental setups.
    Send a few regions queueing, no result from interpreter, yet sometimes
    turns blue.  Why???

*** C Allow empty retract action that doesn't produce new prompt
    (Noticed with HOL4).

*** unify format for syntax table entries with imenu (make alist);
    use config setting for syntax table entries everywhere rather than
    modify-syntax-entry.

*** C Implement optional arg to next/undo which doesn't update
      display (so user can retain something else on screen)

*** X Cleanup display during settings processing.

*** C Generic adjusting of pretty-printer line width 
  Make a generic hook (or hook-constructing macro) to adjust
  pretty printer line widths, a la LEGO.  Maybe find a better
  place to do this that in the proof-shell-insert-hook (should
  be triggered by resize events).

*** C document and simplify proof-script-span-context-menu-extensions

*** C generalize from Isabelle's "atomic scripting" theory file mode
      to allow other instances which do not allow incremental
      processing of files in major or auxiliary file types.
      E.g. twelf, ACL2, LambdaCLAM.
      Also, add the atomic scripting handling for Isabelle/Isar.

*** B Move over to new better designed parsing function mechanism.

*** B Generalize electric terminator mode for other parsing mechanisms.

*** B Add parameter for help function so HOL help works nicely

*** C Add output highlighting to minibuffer in proof-shell-message.
    (Quite tricky to get text properties onto text in minibuffer...)

*** B Extensions with semantic tokens
      Look at the Semantic Navigator package.  Implements persistent
      database of tokens.

*** D Bugs with extents: 
      Sometimes probs if try to assert a whole file while one is
      being processed:     (proof-set-queue-start end) call in
      proof-done-advancing finds that queue span is detached.
      Code is now robust for this.  But why detach anyway?

*** D ChangeLog generation still not right.  
      Probs: duplicated entries when runs several times in same day.
      Suggested fix: use rcs2log to generate the entire log, just take
      a sensible number of lines from it.
      (Ideal would be to get until a given date)

*** B proof-shell-restart should clear response buffer (only noticed with
  proof-tidy-response=nil)

*** B TESTING. 
    - Add automatic testing mechanism to test user-level functions PG
    - Test schedule for things to try with a new instantiation

*** B Add a new configuration setting for matching proof commands
  which have no undo effect --- should be treated like comments
  for undo.  Perhaps would be useful for Isabelle, HOL, at least,
  although it's tricky to see how it would be completely *safe*.
  [ See discussion with Pierre re Coq undo command categories ]

*** X Fix the doc makefiles to adapt the image flag in PG-adapting.tex
      properly, for dvi/ps targets

*** C Clean up assert-until-point stuff: should have just one
  function, as a subroutine of assert-next-command; and no bizarre
  never-used arguments!

*** C Improved configurability of command settings, etc.
  We should let command settings, etc, be a special type
  which can be one of three things:

    'string    -- send this as a command to assistant
    'function  -- call this interactively to return either
		   'string -- send this as a command
		    nil -- do nothing (function does work).
				   
  This way we cover commands which need prompting for extra
  args, as well as elisp functions which do whatever's necessary.
  Then use a generic function "proof-invoke-function" or similar.

  Used e.g. for proof-goal-command-regexp and proof-save-command-regexp.
  New names: proof-goal-command-match, proof-save-command-match.
  Then we can remove duplicity and simplify code.

*** C Usability enhancement:
   Movement of point after assert/retract commands
    - configure by default for one command/line.
    - Add option for many commands per line.
    - Maybe shell like behaviour with pressing return?

*** C Usability enhancement:
    - Fix proof-script-command-separator and
    proof-one-command-per-line flag, document them.

*** C Support an extended version of dynamic abbreviations, to work
  for commands rather than words.  Should behave a bit like a history
  mechanism in shell buffer: use M-n M-p to scroll up and down
  through previous and forthcoming (matching) commands.

*** C Consider supporting imenu instead, or as well as, func-menu.

*** C Improve proof-easy-config mechanism.   
      
  Let it be redoable by initializing some of the variables to 
  default values to begin with(?).  e.g. proof-script-next-entity-regexps.
  Convention is that everything must be set in proof-easy-config body.
  Use custom to set everything to its default value from proof-config,
  before invoking the body.

*** D Make tags support in lego.el and coq.el a bit more generic.
  Use customization option proof-tags-support.

*** D Continue programme of making adaptation easier.  

*** D Fix up sources to conform to library header conventions 
  see (lispref)Library Headers.

*** D Proof shell exit function -- could try sending an interrupt first
  if the process is busy, just to be polite (and avoid the 10 second
  wait before it gets killed).  

*** D X-Symbol: is there a function to input in the minibuffer using
  a token language?

*** X Investigate possible toolbar refresh problems.
  Sometimes extra clicks *are* needed.  Why?  (Gone in recent Emacsen?)

*** D Is there a way to make colours defined for x work in mswindows too?
  defface specs with (type x) seem to work fine with (type mswindows) too.
  Hassle to duplicate, is there an easy way to cover both?

*** C Implement proof-generic-find-and-forget
  <...>-count-undos, to simplify prover-specific code.  
  Complete reengineering of *-count-undos and 
  *-find-and-forget at generic level

*** C Add to proof-config those variables created in proof-easy-config for
  font lock and syntax entries.  Use these instead of primitive
  elisp in the other configs, too.

*** C Improvements to customization mechanism: watch the use
   of customize-set-variable, odd for users who think it
   means they've changed a setting!
   (currently: next-entity-regexps, proof-splash-settings for Isabelle).

*** C Add improvements to script movement in electric terminator mode.
  Some commented regions in code.  E.g. automatic newline/space after
  C-c C-BS.

*** C Make proof-{script,shell,goals,resp}-font-lock-keywords the
  default way of setting font-lock-keywords, removing from
  proof-easy-config and changing each supported prover instance.

*** D Settings mechanism could be generalised for non-persistent settings

   local settings:
    E.g. Coq has some settings which are local: "Focus" which
    it doesn't make sense to save between sessions or issue
    at the start of the session.
   
   Ideal would be to specify context when local settings are
   relevant, as a predicate.

*** D Modify response display routine a bit to center around recent output,
  or display top, for long output.    Makes better sense for big 
  screen-fulls, perhaps?  Or maybe display top with an itimer to
  move to the bottom after a couple of seconds delay, would be a
  nice effect.

*** D Scheme to detect type of buffer and choose between possible modes.
  Help select Isar over Isa, maybe sml over HOL etc?

*** D Fix the sentinel infinite loop bug which occurs in some cases
  when proof shell startup fails.  Same message is printed over
  and over.  Infinite in GNU Emacs.  Why?  See note at 
  end of proof-shell.  [2hrs]
  
*** D Quit timeout enhancement: instead of killing immediately after
  timeout, could give a message "not responding, kill immediately?"

*** D Consider proof-generic-goal-hyp function, for proof by
  pointing support.  Based on `proof-shell-goal-regexp' which
  I accidently introduced at one point.

*** D Make code robust against accidental deletion of response/goals
  buffer.  Add functions proof-get-or-create-{response,goals}-buffer.
  [1hr]

*** D proof-script-next-entity-regexps: 
  "However, it does not parse strings, comments, or parentheses."
  Actually we could improve the generic code to ignore
  headings which buffer-syntactic-context suggests are inside
  comments or strings.

*** X Change the name of "automatic multiple files" to something
  more comprehensible.

*** D Strange problem when running in tty mode: c-c c-RET seems to be
  impossible to type.  Consider binding C-c RET instead when
  running on a console.

*** D Tidy up library-loading and dependencies.  (Probably do
  this at the same time as organizing for the XEmacs
  packaging mechanism)

*** D Make compile should give error if any elisp compile fails.

*** D Check support for proof-guess-command-line, new generic setting
  added by Patrick.  Don't know if anyone can use it, actually.

*** D Usability enhancement:
    - Fix asymmetry between "doing" and "undoing": doing will skip comments,
      undoing will not.  e.g. test case: (* tester *) intros; 

*** D BUGLETS:
  - Response buffer doesn't scroll to display o/p (it does for debug msgs,
    oddly).  This might have been a 1998 design decision.
    Maybe it should be a user option?
  - XEmacs pg forces on font-lock, should it?

*** D SMALL DELTAS:
  - Consider setting proof-mode-for-script automatically?
  Is it ever needed in the shell before the script mode has
  been entered?
  - In case active terminator leads to an error, delete it again?
  (problem synchronizing)
  - Improvements to script navigation commands.  Would like some
  uniformity with proof-find-next-terminator, and a better
  implementation.  Maybe we have four commands: find command start,
  command end, and move to next command/previous command.

*** D 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.  

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

*** X Implement proof-auto-retract idea.  [4hrs]

*** D 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)

*** D 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)

*** D proof-goal-command-regexp: the syntax of Coq spoils the
   uniform use of a regexp to match a goal (since it allows
   goals to begin Definition ...).  Nonetheless, it would be
   for this not to mean that everyone else needs to set
   proof-goal-command-p.  Perhaps some crucial regexps can
   be used via proof-string-match-p which would allow a 
   function to be invoked instead? (Cf font lock).
   Or via a new generic mechanism for matching or invoking a fn.

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

*** X Add support to filter out unwanted noise from the prover by setting
  up a regular expression  proof-shell-noise-regexp [2hr]
  (any useful examples of noise?)

*** D 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;"  Probably by using a generic Emacs package.  [6hr]

*** D Review and prune "FIXME notes" which are notes about ongoing fixes
  or sometimes things to do.  [6hr]

*** D  Write proof-define-derived-mode which automatically adds a 
   call back hook somehow corresponding to our "proof-config-done"
   mess.  Propose this to maintainer of derived.el. (1.5hrs)

*** D 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;"))

*** 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 More flexible help configuration is needed.  HOL has some nice
  on-line help but no way in PG to help by library.  Perhaps
  a help browser is needed?  At least, optional arg to help command.
  [patch ready and waiting to go in]

*** X 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.

*** X Making undoing better.
  Rather than calculating an undo command each time an undo command
  is needed, another idea would be to keep the undo command in the
  span.  Then when we amalgamate spans we can construct new undo
  commands.  When we come to issue an undo, we either need to do
  each undo step in turn in reverse, just the final one, or perhaps
  some proof-assistant dependent filtering/modification of the
  set.   At the moment, though, PG is rather keen on issuing just
  one command to forget to some specific place in the script.
  [Maybe a design principle is that spans should coincide with
   undoable regions]

*** X A more flexible way of choosing which instance of PG we want,
    allowing matches on the buffer before choosing the mode function.


** 3. Things to do for the documentation

*** B New screenshots for web page, also would be nice for manual.

*** B Documentation:
      Check new doc for hiding; add doc for dependencies, tracing.
      Moving spans; navigating through locked region.  
      Favourite menu.

*** A Doc new bits: proof-next-error

*** A Doc new bits: font lock keywords, filename %e, %r.
  Added proof-{script,shell,goals,resp}-font-lock-keywords.
  Presently used only in proof-easy-config, will put into other
  mechanism

*** A Doc new bits: win32 support

*** A Doc new bits:  settings mechanism via defpacustom 

*** C Update front page image
  - Should include ??? logo to represent other provers

*** B Manual improvements before techreport publishing (see notes at end also):
  - Mention configuring function menus, outline.
  - Consider splitting up chapter 9?
  - document mouse functions, proof-cd, process quit timeout, 
    X-Symbol, prog-name-guess, new menu functions for display.
  - general tips on what to do when things go wrong: try
    interrupt, restart, finally exit proof assistant.
  - improvements after feedback from users.
  - add screenshots?
  - add more index entries

*** B Add something to better document two-buffer versus three-buffer
  interaction modes, and the use of proof-window-dedicated to
  trigger three buffer mode.

*** C Documentation in pdf format: need to fix inclusion of image 
  problem.

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

*** D texi-docstring-magic: difference between GNU Emacs and XEmacs regexps
  GNU Emacs gives buggy behaviour with "@lisp" regions.

*** B Doc enhancement: explain conditions for switching buffers and auto
  switching of scripting buffers.  (See doc of 
  proof-auto-action-when-switching-scripting)



** 4. Emacs issues

*** GNU Emacs issues

**** A Improve support for Emacs 21.
  To do:  PBP highlighting (?)

**** B Consider replacing buffer-substring -> buffer-substring-no-properties
  Text properties are passed around in spans, probably needlessly.
  (not the same in XEmacs?)

**** C Changed implementation of overlays inside Emacs itself.  We seem to
  need 'priority property of overlays for queue and locked to make 
  sure the colours show through.  Even then mouse highlighting is strange,
  and background face spoils the others.  Transparent?
  Same priority: we get mouse highlighting but no face property.
  Higher priority: we get blanking as mouse highlighting.  Yuk.
  ACTION: check Emacs Lispref for hints.  Maybe ask on newsgroup.

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

*** XEmacs issues

**** C Ask for easy-menu to support :visible keyword
   Very useful option of GNU Emacs easy menu to remove items
   from menu altogether, dynamically.   (Or at least, fairly
   dynamically.  Fully dynamically would be guitrocity).
   [NB: this is there now, perhaps, as :configured]

*** A Undo in "read-only" regions 

*** A Support for nested comments



** 5. Things to do for subterm markup / proof-by-pointing

*** B Unify proof-insert-pbp-command and proof-shell-insert-loopback-cmd.
  Add some debugging messages in proof-done-advancing to indicate
  Maybe pbp should be a new class of "'pbpadvancing" since we don't
  want to allow the flexible queue manipulation here?  Think on it.

*** B Change proof by pointing (pbp) stuff into proofstate buffer stuff.
  Outsource actual pbp/goals functionality 
  (separate pbp annotations from other annotations).
  Rename pbp-mode to response-mode or goals-mode (which doesn't
  support any actual proof-by-pointing), Make a file 
  proof-goals.el.  [4 hrs]

*** C Extend balloon-help (e.g. show pbp command)

*** C Fixing up errors caused by pbp-generated commands; currently, script
  management unwisely assumes that pbp commands cannot fail.
  da: Is this still true?   It looks fine to me.   I think "failure" 
  should mean generates an error.  With LEGO pbp, it uses "Try"
  tactic which always succeeds, whether or not something gets done.

*** C In case of pbp failure (real failure), we might keep a flag
  to indicate that the next pbp command should delete the 
  previous pbp command's insertion into the buffer, to replace
  it with another one.

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






** 6. Things to do for Web Pages, Distribution

*** C simplify editing of web pages by instead including files
   with version numbers in them, at least for development version.
   Can also use the link "-latest".

*** C Remove fileshow urls in html

*** D Add an animation, showing proof replay.

*** C Wanted for links: something to UITP.  

*** C Validate pages.  
   Current failures for HTML 4.0 to do with CGI-style arguments with "&",
   this is a problem with PHP3 really.

*** X Restructure so that page titles are different to help
  browsing.  (Move links_arr from header.html somewhere new,
  and set $pg_title appropriately before head.html is included).

*** X Add some one-stop-shop pages.  Ask permission to redistribute
  packages for PAs.  Maybe do Windows and Linux versions.




** 7. Future improvements to take advantage of newer Emacsen

*** X XEmacs 21.2 compatibility/improvements
**** Accelerators for PG menus?  (how to customize?)
**** Use one-shot-hook for splash display

*** X GNU and XEmacs improvements
**** Indirect Buffers 
  Maybe a cunning way to implement the response buffer and goals
  buffer, since they're basically variants on displaying fragments of
  the shell buffer output. Appears in XEmacs 21.2, GNU 20.5






** 8. Bugs in other software beyond our control

*** A Nasty bug in Emacs 21.{1,2} triggered by
    proof-shell-dont-show-annotations.  Report this.

*** X Code for find-alternate-file has annoying habit of nullifying
    buffer-file-name before kill functions are called, on a buffer
    named ** lose **.  This means PG has to keep a copy of the
    buffer file name to handle proof-included-files-list nicely.
    Would be better if (X)Emacs code didn't do this.

*** X useful if call-process would keep last error state 
      (primarily for exec-to-string, in case of errors)

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

*** X oddity: startup delay when running XEmacs remotely and local display
is 8 bit.  Suspect an XEmacs issue to do with face allocations.  Also
huge delay in buffers for Isabelle mode which try to highlight binders
(removed because they appear inside strings anyway)

*** X Error with pdftexinfo (still there?) 
Gives problem with @value{blah} inside @pdfurl.  May be absent from
pdftexinfo.tex, but that version doesn't seem to generate web links?




** 9. New Stable Version Release checklist


***  0. Make all files have same CVS branch with cvs commit -f 
***  1. Tests: multiple file test suites for LEGO, Isabelle; other egs
***  2. Check for compiler warnings running "make", on XEmacs & Emacs
***  3. Test cases using compiled code on Emacs and XEmacs.
***  4. Dates and versions updated.
        Check README, doc/ProofGeneral.texi, html/download.html, others.
***  5. ProofGeneral.texi docstring magic is up-to-date: cd doc; make magic
***  6. Update Emacs and prover versions in texi, html/ 
***  7. Check web page references from other places.
***  8. Validate web pages if they're changed much.
***  9. Update and distribute etc/announce.  
*** 10. Message to PG mailing list.