diff options
| -rw-r--r-- | coq/README | 2 | ||||
| -rw-r--r-- | coq/todo | 40 | ||||
| -rw-r--r-- | isa/todo | 28 | ||||
| -rw-r--r-- | isar/todo | 3 | ||||
| -rw-r--r-- | phox/README | 2 |
5 files changed, 4 insertions, 71 deletions
@@ -6,7 +6,7 @@ Later contributions by Patrick Loiseleur, Pierre Courtieu, Status: supported Maintainer: Pierre Courtieu -Coq version: 6.3, 6.3.1, 7.0 +Coq version: 6.3, 6.3.1, 7.x Coq homepage: http://pauillac.inria.fr/coq/assis-eng.html ======================================== @@ -5,32 +5,7 @@ See also ../todo for generic things to do, priority codes. -** B See if there is a way to turn off the superfluous output of scripts - - from Coq when inside ProofGeneral, i.e. output like this: - - Intros A B G. - Induction G. - Apply conj. - Assumption. - - Assumption. - - and_comms is defined - - In PG, only the last line is relevant!! - If it isn't possible to turn it off, can we send a suggestion - to the Coq implementors for the next version? - -** B Fix silly startup sychronization problem that displays - cwd on startup. - -** B C-c C-c breaks the coherence with prover state - (da: can somebody tell me if this is still true? - what problem specifically?) - Pierre: I never had this problem, it's all I can say - -** B Proof-by-Pointing [2 weeks] +** B Proof-by-Pointing [1 month] 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. @@ -38,6 +13,7 @@ See also ../todo for generic things to do, priority codes. da: I have old version of code sent to my by Healf. Pierre: Since the code is to be changed, I suggest that we wait for V7. + da: V7 is here now... ** C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? pierre: Yes, the greatest would be to allow users to easily declare @@ -50,17 +26,6 @@ See also ../todo for generic things to do, priority codes. Coq developers to be unicode compliant or something like that. -** C Retraction in a Section should retract to the beginning of the whole - section. See the section "Granularity of - Atomic Commands" for a proposal on how to generalise the current - implementation so that it can also deal with sections. - [See also the LEGO problem with Discharge] (6h) - -** C Correct the C-c C-c bug (typing C-c C-c during the execution of a - tactic breaks the consitency with Coq) - -** C Fix the coq-lift-global code - ** 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) @@ -75,4 +40,3 @@ See also ../todo for generic things to do, priority codes. ** 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] - @@ -23,10 +23,6 @@ See also ../todo for generic things to do, priority codes. when undoing qed -** C Investigate fix for looping rewriting in Isabelle. Continual - and frequent messages from the prover lock out the user. - Is there any easy way of fixing this? - ** C X-Symbol support for theory files: bugs at the moment, because of duplicate calls to proof-x-symbol-mode and mess with font-lock initialization. Problem with current version: @@ -52,30 +48,6 @@ See also ../todo for generic things to do, priority codes. ** D Switching to other file with C-c C-o could be more savy with file names and extensions (use some standard function?) -** X weird bug: interrupting Isabelle process (under sml-nj) 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 - ** X Write perl scripts to generate TAGS file for ML and thy files. (60h, any volunteers?) (hard); @@ -13,6 +13,3 @@ func-menu setup?); ** C proper proof-by-pointing support (hard; needs major reworking of Isabelle's pretty-printing subsystem); - -** C tune behaviour of goals/response buffers (e.g. hide empty -response buffers when using 2 buffer model); diff --git a/phox/README b/phox/README index 909ae8a8..c50f814f 100644 --- a/phox/README +++ b/phox/README @@ -4,7 +4,7 @@ Written by Christophe Raffalli Status: supported Maintainer: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> -PhoX version: 0.7 +PhoX version: 0.8 PhoX homepage: http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html ======================================== |