diff options
| -rw-r--r-- | TODO | 2 | ||||
| -rw-r--r-- | coq/todo | 4 | ||||
| -rw-r--r-- | todo | 11 |
3 files changed, 10 insertions, 7 deletions
@@ -18,6 +18,8 @@ Plans for upcoming 3.x versions * Support turning on/off prover output automatically, e.g. Coq's "Begin Silent" and "End Silent" commands. +* Fix Isabelle's "Stack overflow in regexp". See isa/BUGS. + * Make an XEmacs package * Support more proof assistants @@ -32,7 +32,9 @@ See also ../todo for generic things to do, priority codes. ** B Proof-by-Pointing [2 weeks] da: Yves Bertot told me that his CtCoq proof-by-pointing code is in the Coq kernel now, so would be useful for PG. - We need a Coq hacker to do this (Pierre?) + We need a Coq hacker to do this. + Perhaps for new version of Coq. + da: I have old version of code sent to my by Healf. ** C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? @@ -29,12 +29,9 @@ X (Low) e.g. probably not worth spending time on *** Top Priority Fixes for 3.1 - - Solaris ^G problem and FSF Emacs mule/non-mule support - - Recognition of ; only at eol (DvO reported bug here, shouldn't happen) - - Web page: add notify when updated option - - Manual: credits for other bug reporters + - Manual: credits for bug reporters - Would be nice to fix spurious output of Coq and HOL from first line - when synchronization is gained. + when synchronization is gained. How? *** Scheduled improvements for 3.2 @@ -802,7 +799,7 @@ C New modules: *** A Update ETAPS demo -*** A Add some one-stop-shop pages. Ask permission to redistribute +*** 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. @@ -811,6 +808,8 @@ C New modules: 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: |