Hi all. I have given Isabelle/jEdit another try and worked with it for almost two weeks, on different tasks: * Porting the CAVA afp entries (depending on >300 theory files) from 2013-2 to devel.
* Formalizations and proof development (The standard usage) * Writing tools in ML (ML-blocks in thy-file) I have compiled a list of problems that I encountered during my work. I have added descriptions to how PG solved these problems. The problem report here refers to Isabelle version 2ccd6820f74e. My overall impression is that Isabelle/jEdit is usable but much less mature than PG: It does not scale well to large projects, and tends to be unstable. It has many cool advanced features, but lacks important basic ones. However, in my opinion, Isabelle/jEdit is approaching a level of maturity required for production use, once the user knows about its deficits and how to avoid them. I will continue using Isabelle/jEdit for a few more weeks, hoping that a few more basic features will be added/fixed before the next release ... SCALABILITY & STABILITY: * Isabelle/jEdit gets really slow and unresponsive when many files are loaded (you have to wait seconds for a keystroke to show its effect). As all prerequisite theories (not in an image) are automatically loaded, this is unavoidable. In PG, it's no problem to load a theory with many prerequisites, nor to have many buffers open simultaneously. NOTE: This problem could be solved in my case by 1) giving jEdit a ridiculously large amount of heap space (4Gb) and, 2) using images for prerequisite theories. * Isabelle/jEdit does not scale to large files. Error markers on the right side are only displayed for a context around the current cursor position. There seems to be no way to jump to the error position. If the error happens to be displayed as a red bar on the right side of the editor area, pixel-accurate mousing is required to jump to the error, and not to a position dozens of lines away. In PG, you could always jump to the position where processing failed by Ctrl-. . Moreover, you got error messages with file names and line numbers, that you could use to navigate to the error position easily. * Isabelle/jEdit seems to be quite unstable. Within one week, it happened several (3 or 4) times that the whole thing just became unresponsive, and had to be restarted to continue work. In PG, those things happen perhaps once in a month. IMPORTANT FEATURES THAT ARE MISSING & OVERLY TEDIOUS WORKFLOWS * Isabelle/jEdit does not support highlighting of paranthesis in the output window (it does work in PG!). This is an essential feature to read bigger goal states. Moreover, the output buffer does not support middle-mouse-button copy-and-paste on my ubuntu-box, while it perfectly works in the editor window. * Long list of warnings, e.g. "duplicate simp rule", or tracing messages produced by a method appear before the subgoals in the output, and thus makes them inaccessible without lots of scrolling. This feature is a real flow-stopper when exploring proofs. In PG, it is possible to have separate buffers for the goal-state, the tracing, and the warning messages, thus you always see the current subgoal you are working on without scrolling down some buffer every time. * If sledgehammer (both over panel and as command) is running, further processing of the file is blocked/very slow. Thus, it is not possible to run sledgehammer and, in parallel, continue exploration to find your own proof. In PG, parallel sledgehammering works, and I used it extensively. In Isabelle/jEdit I now think twice before I invoke sledgehammer, because it just interrupts my workflow and I have to wait for it to finish staring at the sledgehammer-window and doing nothing. * Isabelle/jEdit cannot open a theory-file without processing it. This is in particular a problem when porting stuff and opening the original version of the same file to look something up. Even worse: Once opened, you cannot close the file again, and it will remain in the theory panel (with an error marker) until you quit jEdit. In PG, it is no problem to open a file without processing it. * The standard search (Ctrl-F) function does not allow to enter non-ASCII characters at all. This is a real show-stopper if you search for a text containing such characters. In PG, you could at least use \<...> - tokens to enter non-ASCII characters. Moreover, I would like an incremental search, but there is probably a jEdit pluging somewhere? (Probably with the same problems of entering non-ASCII characters) * When theories have inconsistent file/theory name, you will only find the error by stepwise going back the chain of "bad theory" - errors, file by file. This is simply tedious. In PG, you got a backtrace in the output, and could immediately identify the broken file. * Auto-Completion does not really work. You have to decide for a "completion delay". If you choose it too short, some completions will not appear at all. If you choose it too long, it interrupts your typing flow when entering special characters. In PG, there is no context-sensitive completion at all ... the one in jedit is actually not usable without tolerating .5sec completion delay on every special character you want to type) Moreover, the completion mechanism for entering special characters seems not to be as mature as the one in PG was: When entering sequences that should be completed, e.g., \lambda, this only works if there are no characters behind. All in all, I am typing significantly more to enter special characters than I did in PG. * "Disappearing Proofs" in PG is a really nice feature to keep overview, in particular in larger files. In PG, I used it heavily. There is nothing similar in Isabelle/jEdit. Code-folding can be used to a certain extent, but it cannot handle apply-style proofs, and is not applied automatically as in PG. Moreover, code-folding still seems not to work properly: Sometimes, fold-markers simply do not appear, sometimes they appear at completely wrong places. I'm not sure whether this is a non-deterministic effect, or depends on some garbage text at the end of the theory file. -- Peter _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
