path: root/todo

-*- mode:outline -*-

Proof General Low-level List of Things to Do
============================================

$Id$


* Contents
==========

 * Priorities
 * Things to do in the generic interface
 * Things to do for Proof-by-Pointing
 * Things to do for Lego
 * Things to do for Coq
 * Things to do for Isabelle
 * FSF Emacs issues
 * Stable version release checklist
 * Things to do for Proof General Project



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

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





* Things to in the generic interface
====================================

A Pending work, in progress [da]:
    - reorganization and improvement of menus, keybindings
	. use toolbar functions, but remove from proof-toolbar and reorganize.
	. update documentation
    - test support for x-symbol
    - document proof-mouse-track-insert (new name for proof-send-span,
re-enabled), proof-toggle-scripting, new configuration options.
    proof-cd

D Investigate possible toolbar refresh problems.
  Are extra clicks ever needed?  Wait for some comments.

D 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.
  
B After interrupt, queue region is left intact.  Seems odd. 
  Let's remove it.  Also interrupt needs other cleanups:
  position of proof-marker may be wrong.  Even the message
  appears in the goals buffer rather than the response buffer!

B bug: interrupting Isabelle process sometimes doesn't return, why?
  (see first half of interrupt error only:
    *** Interrupt.
    *** At command "time_use".
  
    uncaught exception ERROR
      raised at: library.ML:1100.35-1100.40
  But not "uncaught exception" part.  
  What is worse: prompt disappears!  But process still seems to be
  there underneath.  Not sure where this bug comes from.

  Moreover, killing process then hangs Emacs with message 
  "cleaning up", and get error
    (1) (error/warning) Error in process sentinel: (no-catch exited t)

  To see if this is some SML/NJ or Isabelle weirdness, test in 
  xterm: use "ROOT.ML", interrrupt, use "ROOT.ML" again.
  sig 11!  (flaky hardware?)  
    /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2ad09c43
  Not reliably repeatable, but:
    ProofGeneral.isa_restart(); 
    /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b


C Add new test cases for closure of unfinished proofs in Lego,
  Isabelle.

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?

   Also: movement when queue region is active is odd.
   E.g.: press C-c C-n twice on lego/example.l.  
   Point hops backwards!

C Usability enhancement:
   Rationalize next and undo.  Make same as toolbar 
   commands and have different commands for power users
   to assert/retract until point.
   At the moment this is done by binding to the toolbar
   commands, we need to remove these from proof-toolbar now.

C Usability enhancement:
   Have toolbar button/command to goto a point.
   Proof General itself should work out whether it's a 
   retraction or advancement!

C Unify toolbar and menu functions. (1h)

B Web pages: improve screenshots section to include a slideshow, or
  at least, a series of pictures of PG in action.  (3 hours)

C Nicety enhancement:
   Add messages "retracting buffer ... done" "processing ... done".
   This needs some call backs or setting of variables examined
   by proof-done-{advancing,retracting}

C Fix colouring of response buffer, may be broken.  The idea was
  that the latest message would always be highlighted, I think.

C Usability enhancement: remove stupid "I don't know what I should be doing"
  errors and replace with something more informative.

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

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

C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting
  ELISP_DIRS somehow.

B Improve relocatability of RPM package, and produce package for XEmacs
  which installs directly under ~/.xemacs/packages.

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

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

C Support for proof-guess-command-line, new generic setting added
  by Patrick.

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

D Add etc/announce to web pages somewhere.

D Key binding and interface issues
  - Consider change for prefix argument for C-c C-u and C-c u,
  it's quite easy to accidently delete by pressing C-c C-u
  repeatedly.

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 and hiding the special
    characters.  
    Maybe using x-symbol would give another approximation, too, although
    I'm put off that because it's not so standardly a part of XEmacs yet.
    Or maybe w3's code for HTML mark up could be borrowed.

X Multiple file improvements: add automatic/implict handling of 
  multiple files, by retracting across file boundaries automatically 
  if there is no support from the proof assistant to do this.  Idea is
  that when we retract file B and loaded files list is A B C D E,
  then C D E are retracted too (one by one).  Retraction should
  happen (before) first undo takes place in a buffer on the loaded
  files list.  Type theory proof assistants with a linear context
  can be handled perfectly this way.

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 bug: mentioned by Martin H. with Lego: "don't know what I should
  be doing..." error when it shouldn't happen.  
  [this item is useless without a more detailed description]

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

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)

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

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(?).  [4 hours]

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

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

C Reorganize menus in a better way.  Have generic scripting commands
  for keyboard or menu/toolbar use. (2hrs)
    
C Implement proof-auto-retract idea.  (4hrs)

C Make and test generic versions of <..>-goal-command-p, 
  <...>-count-undos, to simplify prover-specific code.  

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

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

D  Review "FIXME notes" which are notes about ongoing fixes or
   sometimes things to do. 

D  automise testing procedures in etc/

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

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

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

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

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

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.

  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.

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 Web pages:
   - Check appearance in V3 browsers.
   - Make front page logo be an image map.  
   - Reduce text size and front page image, for 1024x768 screens.
   - Validate pages.  
      Current failures for HTML 4.0 to do with CGI-style arguments with "&",
      this is a problem with PHP3 really.
   - 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).
   - Add pdf documentation as soon as DCS upgrades its ancient
      TeX installation, or as soon as making release from elsewhere
      works.  Also need to fix inclusion of image in pdf. 
   - Add status bar messages to navigation bar
   - Get rid of footer() function.
   - Convert to SSI only plus a meta-generation phase?

X 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.
  [ This item reduced to X since Poly/ML is now obsolete.  This may
    still be useful for future proof assistants, though. ]

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.

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.

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.

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



* Things to do for 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.



* Things to do for Lego
=======================

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. Specifically, after having processed
  a script (interactively), it would be nice if one could now save the
  buffer in object format. At the moment, it only gets converted
  (automatically) when it is read in indirectly at a later stage.
  However, there is currently no LEGO command to do this.  [4h]



* Things to do for Coq
======================

A C-c C-c breaks the coherence with prover state

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)

D Add Patrick Loiseleur's commands to search for vernac or ml files.
  (they are in a separate file that is part of Coq distrib.
   should I really integrate that in PG ? Patrick) 

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]



* Things to do for Isabelle
===========================

B auto-adjust Pretty.setmargin when window is resized

C Unify display of proof output for final level "No subgoals" 
  case with other levels  (i.e. remove spurious newlines).
  NB: spurious newlines may be liked by other provers.

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.  Would be a nice addition. (4 hours)

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

D Switching to other file with C-c C-o could be more savy
  with file names and extensions (use some standard function?)

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).  Does anyone
  actually want this?

X Manage multiple proofs, perhaps by automatically inserting
  push_proof() and pop_proof() commands into the proof script.
  But would lead to unholy mess for script management!



* FSF Emacs issues
==================

A bug: FSF Emacs problem (showstopper): highlighting of locked region
  and queue region seems faulty nowadays for me (da). 
  Only tested on Linux. 
  Going back to 2.0 does not fix problem, on 20.2 or 20.3

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.

X possible bug: Thomas had 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.


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

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

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




* 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)
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 and prover versions in texi, html/ 
7. Check web page references from other places.
8. Validate web pages if they're changed much.

   


* Things to do for Proof General Project
========================================

A Try to get small project grant from LFCS to help with
  development of Proof General

A Consider writing another grant proposal related to
  Proof General to generate funding for Proof General.

A Find new person to help advance and develop Proof General.

A Find new person to help maintain Coq Proof General

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

   * Fix page rearrangement to insert a blank page
   * Fix typos/other stuff found by Dave.
   * Suggestions, typos, contributions by Healf.  
     (Dave has email)
   * Improve trivial and uniformative docstrings.
   * Fixup markup mistakes by editing docstrings.
   * Update menus in texi
  [6 hours]

A Write paper for system demonstration of Proof General
  for some conference.  Write paper on design and
  development of Proof General.