path: root/todo

-*- mode:outline -*-

* Proof General Low-level List of Things to Do

$Id$

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

** 0. Contents

 1. Priorities
 2. Things to do in the generic interface
 3. FSF Emacs issues
 4. Things to do for Proof-by-Pointing
 5. Bugs in other software beyond our control
 6. Stable version release checklist
 7. Things to do for Proof General Project
 8. 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


*** Outstanding bugs to investigate

C The PG isabelle-completion-table seems to be subject to case-fold, which
  it shouldn't be: \<sqinter> does not work, but \<Sqinter> is OK.

B Keybindings for processing theory in thy mode gone??

C Undoing comments with FSF Emacs weirdness.
 Noticed with Emacs 20.6.1.  Seems to affect all provers.
 Workaround:  use C-c C-RET or C-c C-r instead.
 Nasty workaround: (setq debug-on-quit t), hit "c" on each hang
 to continue.
 Seems to get stuck looping in {coq,lego,whetever}-find-and-forget
 but no problem when running with edebug edebug-defun on this function.
 Maybe filter specific glitch to do with spans?
 Bit of a showstopper for FSF emacs.

X Solaris bugs: font locking and button enabling.

  [Markus]: I can only produce this problem on Solaris, where we have
  both a mule and non-mule version of xemacs-21.1.8.  On my Linux box
  at home there is no problem present (using xemacs-21.1.7-mule).

  Note that on the Solaris boxes the problem is already exhibited by
  visiting a new/empty thy file: buttons are off and are not enabled
  by typing new stuff.

  Moved down the list now, instead we disable button enablers on
  Solaris.

*** Scheduled improvements for 3.2

**** C sanity checks for proof shell config variables.

**** C Canvas FSF Emacs to include -syntactic-context -locate-file fns from XEmacs.

**** A Clean up intro for PG-adapting manual.

**** C Fix mode naming for Isabelle 
     (might like isa-proofscript-mode -> isa-mode;
      but this conflicts with entry mechanism for thy/isa mode).

**** A Add Pierre's improvements for X-Symbol config to other provers.
       Perhaps there should be a default configuration for non-token
       input languages?

**** A make C-c C-l go to bottom of response buffer while output
       is arriving (set-window-point (point)) or similar.

**** A Doc new bits: which XEmacs packages does PG use?  (for INSTALL)

**** 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 for 3.2

**** A Doc new bits: win32 support

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

**** C Settings mechanism could be generalised

   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.

**** B New keymap(s) for proof assistants.  Added on C-c C-a

   Doc this change.
   Means old C-c C-a and C-c C-e are lost.
   Consider adding new submap for movement in proof script.

**** 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 Isabelle: I think show_sorts -> show_types, how can we reflect this ?

**** A Add efficiency improvement by turning on/off prover output.
  Patch already added to pre-release.
  Does it need adjusting to turn on output in case of error/interrupt?

  mmw: Performance problems in isa and isar have been fixed by
  removing eager annotations almost everywhere.

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

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

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

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

**** B Yet more proof assistants supported.  Perhaps we will introduce
  class of "unsupported" Proof General interfaces.

**** B 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 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]

**** D Remove pbp.el, unused file.



** 2. Things to in the generic interface

*** X Multiple session architecture (difficult)

  With some major re-engineering, PG could be made to work with multiple
  provers at once, and multiple instances of the same prover.

  Ideas: - introduce "session" notion
	 - have list of current sessions in progress,
	   values of active scripting buffer and other per-session vars
	   for each one
         - proof shell filter and other functions must automatically
           switch context to correct session
         - force everybody to use proof-easy-config macro, and set
	   <prover>-var automatically from <proof>-var there,
	   to get defaults for new sessions.

*** C 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 Add support for XEmacs 21 packaging.  Make suitable updates available
  on web page, and make RPM put things in the right place so no .emacs
  file may need editing(?).  [2 days]

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

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

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

*** C Investigate support under Mule.  Suggestion we need to set
  process-coding-system-alist somehow to prevent coding.
  What about Mew ?

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

*** D X-Symbol improvements: see if we can get support for 
  proof-xsym-extra-modes outside PG (just by loading proof-site).
  Will be handy for Isabelle's .itex Isabelle-LaTeX files.
  Then we can parameterise more of the xsym support, and
  remove spurious settings of calculated stuff from
  x-symbol-isa.el  (see FIXME comments in v3.1 there).

*** D X-Symbol improvement: turning it on/off seems to move point.

*** 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 texi-docstring-magic: first time deffn's, etc, are added, whitespace
  after magic comment is left.

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

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

*** C Make the remaining options in the quick-opts-menu be more
  dynamic: same function as in proof-x-symbol.el to redisplay
  after changing output hightlighting, make/delete frames,
  etc.

*** X Why does dired get loaded when PG loads?  (Can we speed 
  loading by avoiding a particular function?)

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

*** B Fix problems with C-x C-v and C-x C-w 

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

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

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

*** B Display functions: does auto-delete-windows work with
  window-dedicated as it should? (I thought it would switch 
  between 2/3 bufs as appropriate?).

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

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

*** B Continue program of making adaptation easier.  
   - Test proof-easy-config mechanism.
   - Add proof-shell-important-settings and test that they're set.

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

*** C See if there is a way of postponing func-menu loading.

*** C Quit timeout enhancement: instead of killing immediately after
  timeout, could give a message "not responding, kill immediately?"

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

*** B make pretty printer line width altering generic.
  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).

*** D 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 X-Symbol: is there a function to input in the minibuffer using
  a token language?

*** C Investigate possible toolbar refresh problems.
  Sometimes extra clicks *are* needed.  Why?

*** B "Confused" bug: shows up when do lots of C-c C-n as
  process is starting up, when it takes a long time, esp
  for Isabelle.  Perhaps in filter, more output arrives
  before properly initialized?  A bit of a mystery, since code
  explicitly waits for initialization to complete.

*** B C-x C-v does not seem to run kill buffer hooks properly: at
  least, what happens is buffer name changes to **lose** and
  (e.g.) a completely processed file doesn't get added to the
  included files list.  Auto retraction appears to work.

*** B Now we have proof-shell-error-or-interrupt-seen flag, we maybe don't
  need proof-shell-handle-error-hook: presently only use is in Plastic
  to set a similar flag.

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

*** B Oops --- here's an alternate and better fix to Isabelle goals
  problem: just 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.  This gets rid of the
  proof-goals-display-qed-message kludge.  See comments in code.

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

*** C 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 FSF Emacs.  Why?  See note at 
  end of proof-shell.  [2hrs]
  
C New modules: 
     proof-shell-{start,end,goal,blah} -> proof-goals-{blah} 
     pbp-{blah} -> proof-goals-{blah}, new proof-goals.el  
     Low-level commands in proof-script.el -> proof-core.el

*** C Package management for X-Emacs.  
    - Add auto-autoloads
    - install under ~/.xemacs

*** C Improve relocatability of RPM package.

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

*** 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.
  [30 mins]

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

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

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

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

*** D Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting
  ELISP_DIRS somehow.

*** 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 Robustify and cleanup code by allowing functions in place of regexps
  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.

*** D Internal improvements for marking up proof assistant output.
  We need a better mechanism for allowing "invisible" mark up
  of assistant output based on annotations.  Present code
  allows proof-shell-leave-annotations-in-output=t to work
  together with font-lock to do mark up.  
  Instead we need something more like what enriched-mode does
  (although I've just tried it and I foound that copying with 
  the mouse ignores the text properties, but copying with the 
  keyboard copies them!).  It uses a general library
  format.el for reading and writing files in multiple formats.
  This is not quite what we want for our purpose, but it might be a
  closer approximation than using font-lock-fontify and 
  deleting the special characters.   It would allow sgml-like
  markupo in the future, too.
  Or maybe w3's code for HTML mark up could be borrowed.

*** D Idea: introduce a dynamic follow mode which follows
  proof-locked-end rather than proof-queue-or-locked-end.
  Would be annoying for interactive use though, point would
  jump from under fingers (although no typing anyway, hardly
  matters).  Alternative is dynamic recenter mode to 
  keep end of locked region in buffer.

*** X Improve goto button image [suggestion from Markus]
  Is it possible to avoid the arrows to touch in the middle,
  emphasizing the 'point' a bit more.  The arrows look a bit outwards
  bent, too.

*** X Check compilation okay, check on use of eval-and-compile.

*** D BUGLETS:
  - If Proof General is loaded with M-x load-library, it gets set up
    for *no* proof assistant!!
  - Repetition of "load .emacs" on menu bar even when it's been loaded.
  - 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?
  - are face defconsts still needed now we use defface?
  - XEmacs pg forces on font-lock!

*** 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)
  - Difference in menubar appearance depending on whether X-Symbol
  is loaded before Proof General or not.
  - 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.

*** X Update logo to include new "???" prover badge  (maybe it should be 
  "...") from graphics file elsewhere (da)

*** X Why don't PG's minor modes appear on XEmacs minor mode menu?
  (C-right on status bar).  Perhaps they shouldn't anyway, they're
  not very useful in non-scripting buffers.

*** X Usability enhancement:
   Enable toolbar in other PG buffers.  Should switch to active
   scripting buffer first if it is non current.
   In fact, a sensible subset of scripting commands would
   work from other buffers.
   This suggestion is based on observation of a user's
   confusion when the toolbar disappears from other PG buffers.

*** X Compatibility enhancement:
    - Consider sending comments to proof process after all.  They might
      contain special (e.g. LaTeX) directives or something.
      Probably only worth considering if/when it becomes a problem.

*** X bug: outline mode when proof-strict-read-only is nil ought to
  work, but there may be problems.

*** X CVS repository issues.
  Where are obsolete 'fileattr' files generated from/maintained?
  Should junk these (which appear to say that tms is watching everything).

*** X 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?
  [da: can't repeat this now, presume it has gone away?]

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

*** D Check matching code carefully, in view of bug reported (now fixed)
  for Isabelle.
  Examine syntax tables for all instances, and whether
  word matching is based on whitespace constituents or non-word
  constituents.  [6 hrs]

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

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

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

*** D Add support to filter out unwanted noise from the prover by setting
  up a regular expression  proof-shell-noise-regexp [2hr]

*** 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.  [2hr]

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

*** X 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.
  Wait until it's a problem for somebody.
  [Trouble with this is that terminators are used for active
   terminator mode, among several other things]

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

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

*** X automise testing procedures in etc/

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

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

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

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

*** D Make wellclean target remove images in html/images which are
  generated from the image directory.  Consider putting all the
  image sources in images/

*** X splash screen: report XEmacs problem of not displaying transparent
  gif properly.

*** X Consider filtering out special annotations from shell buffer
  rather than merely making them invisible.   Probably NOT:
  this is a design decision that interaction with the shell
  should be minimal, so we don't help with fontifying or
  fixing cut-and-paste.

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

*** 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 General customization: how should it work?
  Presently we have a bunch of variables in proof.el which are
  set from a bunch of similarly named variables in <engine>-syntax.el.
  Seems a bit daft: why not just have the customization in
  one place, and settings hardwired in <engine>-syntax.el.
  That way we can see which settings are part of instantiation of
  proof.el, and which are part of cusomization for <engine>.

*** X Moreover, 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!
  [see proof-easy-config.el]

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

*** X Provers with sophisticated/configurable syntax should tell Emacs
  about their syntax somehow, rather than trying to duplicate
  specifications inside Emacs.
  Maybe some particular ATerm format would help with this?

*** 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 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 Improve efficiency for processing for large proofs.
  Currently worse case is about 75%/25% CPU to Prover/XEmacs when
  processing long output stretches on zermelo.  
    (Example: time_use_thy in src/HOL/Real/ROOT.ML)
  Processing large scripts is likely to be worse, and needs work.
  But we can sidestep the issue by using prover-silent modes,
  now in 3.2.
  




** 3. FSF Emacs issues

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



** 4. Things to do for 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 Usability enhancement: have a ballon-help style popup (in the
  minibuffer) to indicate what command pbp will choose, without
  actually running it. 

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





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

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

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

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

*** C add notify when updated option

*** C Wanted for links: something to UITP.  Are there any pages?

*** C Broken (old) links:
    (Applications of a Type Theory based Proof Assistant)
    http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html

*** C Reduce text size and front page image, for 1024x768 screens.

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

*** C Add etc/announce somewhere.

*** X Convert to SSI only plus a meta-generation phase?

*** X Check appearance in V3 browsers.
 

*** X Make front page logo be an image map.  

*** X Add status bar messages to navigation bar

*** X Get rid of footer() function.




** 6. 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 FSF 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, FSF 20.5






** 7. Bugs in other software beyond our control

*** 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 spurious byte comp warning in XEmacs 21.1.4:
  While compiling proof-x-symbol-encode-shell-input:
     ** buffer-substring called with 3 args, but requires 0-3
  for this code:
               (prog1 (buffer-substring)
                 (kill-buffer (current-buffer))

*** X Error with pdftexinfo (hacked version of teTeX pre-release, 1.0.6).
Gives problem with @value{blah} inside @pdfurl.  May be absent from
pdftexinfo.tex, but that version doesn't seem to generate web links?

*** (/usr/share/texmf.local/pdftex/texinfo/pdftexinfo.tex
Loading texinfo [version 1999-09-25.10]: Basics, pdf,
(/usr/share/texmf/pdftex/plain/misc/pdfcolor.tex) fonts, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, (/usr/share/texmf/tex/plain/dvips/epsf.tex) localization,
and turning on texinfo input format.)) (ProofGeneral.aux) [1[/usr/share/texmf/d
vips/config/pdftex.map][/usr/share/texmf.local/dvips/config/dalucida.map][/usr/
share/texmf.local/dvips/adobe/agaramon/pad.map][/usr/share/texmf.local/dvips/co
nfig/wp1.map][/usr/share/texmf.local/dvips/config/mscore.map][/usr/share/texmf.
local/dvips/config/barbedor-ttf.map][/usr/share/texmf.local/dvips/config/goodtt
.map]] [2] (Preface)
! Undefined control sequence.
@indexbreaks ->@catcode `@-=@active @let -
                                          @realdash 
@value ...ode `@-=12 @catcode `@_=12 @indexbreaks 
                                                  @let _@normalunderscore @v...
<argument> @value 
                  {URLpghome}
@pdfurl ...r{/Subtype /Link /A << /S /URI /URI (#1
                                                  ) >>}@endgroup 
@douref ...->@begingroup @unsepspaces @pdfurl {#1}
                                                  @setbox 0 = @hbox {@ignore...
l.264 @uref{@value{URLpghome}}
                              .  Visit this page for
? x
<cmtt10.pfb><cmsy10.pfb><8r.enc><bsfr8a.pfb><bsfc8a.pfb>
Output written on ProofGeneral.pdf (2 pages, 54702 bytes).






   




** 8. New Stable Version Release checklist


***  0. Make all files have same CVS branch with cvs commit -f 
    (only seems to work locally, not via cvs server).
    Innessential convention.  Could increment head number.
***  1. Test 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)
    Even if the code is faulty afterwards, compiling is 
    worthwhile just because it shows up bugs in unbound variables, etc.
***  4. Dates and versions updated.
        Check README, doc/ProofGeneral.texi, html/download.html
***  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.






** 9. Things to do for Proof General Project


*** A Try to get small project grant from LFCS to help with
  development of Proof General.  Latest news: success is 
  doubtful. Needs a self-contained project that 
  *would be useful to LFCS*.  
  One idea: an LFCS CDROM featuring Proof General and 
  bundled with other theorem provers?    How much does a 
  short-run (200 CDs?) cost?

*** A 

*** A Write grant proposal on white paper for Proof General Kit.

*** A Find new people to help advance and develop Proof General.
  Getting more instances would be a good way.  Also encouraging
  feedback.  Hear stories of bugs by word-of-mouth, they don't
  get reported often enough.
  Consider passing on project elsewhere if no LFCS interest.

*** A Polish ProofGeneral.texi and publish as a tech report
  For PG 3.2, probably.  

*** A Write paper on design and development of Proof General.

*** A Write white paper on future of PG project.

*** A Add more PG projects, publicise them.

*** A Push PG research directions:
	- configuration management / dependency organization
	- ideas about proof engineering cf software engineering
	- research on ways of conducting a formalization, cf
	  ways of writing a program.  Common idioms that PG could
	  help with.

*** A Add instructions for developers to use cvs repository 
    remotely.