diff options
| -rw-r--r-- | coq/todo | 11 | ||||
| -rw-r--r-- | isar/todo | 12 |
2 files changed, 19 insertions, 4 deletions
@@ -5,7 +5,16 @@ See also ../todo for generic things to do, priority codes. -** B Proof-by-Pointing [1 month] +** C Auto-compile-vos + Would be nice to ressurect this: interaction between PG + and make system is tricky and tedious. + + +** D Loss of synchronisation with silent mode + Apocryphal story, no test cases. + + +** B Proof-by-Pointing [1 month+] (2002) 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. @@ -4,6 +4,12 @@ See also ../todo for generic things to do, priority codes. +** B Isabelle support for ML and legacy files: would like to remove "isa" instance + Could we handle theory files and even allow scripting in ML files + at the same time as Isar? Maybe not, if this is even beyond what + Isar interface would allow (unless we send an ML file + line-by-line with ML_command?) + ** B theorem dependencies: using Isar's "thm" command does not work at top level. This is annoying for browsing the fully qualified dependency names. (Even the ML_command "thm" @@ -12,12 +18,12 @@ See also ../todo for generic things to do, priority codes. ** B visualise dependencies: sometimes not applicable. -** C func-menu: observe proof-syntactic-context (general problem of -func-menu setup?); +** C func-menu: + observe proof-syntactic-context (general problem of func-menu setup?); ** C undo 'use' command: unlock corresponding ML file; ** C provide template for empty theory (or even just for Scratch.thy); ** C proper proof-by-pointing support (hard; needs major reworking of -Isabelle's pretty-printing subsystem); + Isabelle's pretty-printing subsystem); |