Re: [isabelle-dev] Remaining uses of Proof General?
Great list Peter! > * 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) There is already an incremental search, but by default it has no keyboard shortcut. Myself, I have re-bound Ctrl-F to "Incremental Search Bar", and am quite happy with that. (This is in jEdit's "Global Options", then "Shortcuts".) John ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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
[isabelle-dev] jdk-7u60
With f7a604a2fa63 we are back to the latest stable Java 7, and stability is particilarly important for the Isabelle2014 release. The excursion to Java 8 was interesting, but Oracle still has many fine points to sort out. The jEdit guys had some discussions on their development mailing list, but I did not follow the details. I've myself occasionally seen spurious JVM exceptions in jdk-8u5 that were not there on jdk-7u40, and jdk-7u60 seems to make some actual improvements beyond "critical patch updates". Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
This is a reminder that this thread is still open, until the end of next week when the question will be moved to isabelle-users, with the appearance of Isabelle2014-RC0 (that will be published from the running repository *without* a repository fork yet). At the moment (06599233e54e) there are no remaining uses of Proof General to the best of my knowledge. If anybody has counter-examples they should be put on the table for discussion. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?
On Fri, 6 Jun 2014, Thomas Sewell wrote:
In case anyone else gets stuck in this situation, here is my best workaround:
cat thys/*/ROOT | grep session | cut -d' ' -f2 | xargs -n 10 isabelle build
-d thys
By focusing on (the dependencies of) 10 sessions at a time, isabelle seems to
get the job done.
The grepping and cutting is a bit ugly. Would it make sense to have an
equivalent of 'findlogics' which found sessions? That would allow
isabelle findsessions -d (DIR) | xargs -n 10 isabelle build -d (DIR)
I take this as a reminder that "isabelle findlogics" is actually legacy
for Proof General, which is to be discarded eventually.
Isabelle system programming is now done in Isabelle/Scala, starting
already 5 years ago, and working more and more smoothly as it is actually
being used. So no more bash, perl, ruby, python, sed, awk scripting, just
plain Scala programming with some Isabelle library operations.
For example, the recently updated build_doc tool (bc61161a5bd0) is now a
proper Isabelle/Scala tool, which merely happens to have a bash wrapper
for historical reasons (it is still required for some administrative bash
scripts).
For regular use, the tool can be used directly in the Console/Scala shell
of Isabelle/jEdit like this (e.g. in current f40ac83d076c):
import isabelle._
Build_Doc.build_doc(Options.init, new Build.Console_Progress(true), docs =
List("jedit"))
This has the advantages of statically-typed programming in an interactive
TTY loop, over an untyped scripting language like bash. It requires a bit
of practice and giving up old customs to become fluent with it, but then
it works surprisingly well. I've done that in the past few weeks
routinely, when working on the Isabelle manuals. It also saves a lot of
JVM process creation and warmup-time.
That approach might be a bit shocking to hardcore Linux users, but for
most Isabelle users it makes more and more sense. Isabelle/jEdit is an
IDE, which means "Integrated Development Environment", so it is not
surprising that it has an integrated system programming shell.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problems with datatype-new
Hi René,
this is a tactic failure in the recent size extension (the interface
with fun). We will work on it.
Thanks for the report,
Dmitriy
On 25.06.2014 13:49, René Thiemann wrote:
Dear all,
I have an unexpected problem when defining a datatype using datatype_new.
theory Test
imports
"$AFP/Collections/ICF/impl/RBTSetImpl"
begin
datatype_new ('a,'b) bar = Foo 'a "'b option" "'b rs"
(*
Proof failed.
1. ⋀g ga h.
local.bar.ctor_rec_bar
(λx. case local.bar.Rep_bar_pre_bar x of (l, la, xa) ⇒ h (g l)
(map_option (λx. x) la) xa) =
local.bar.ctor_rec_bar (λx. case local.bar.Rep_bar_pre_bar x of (x1,
xa, xb) ⇒ h (g x1) xa xb)
The error(s) above occurred for the goal statement⌂:
⋀g ga h. local.bar.rec_bar h ∘ local.bar.map_bar g = local.bar.rec_bar (λx. h
(g x))*)
end
The problem vanishes if I make the datatype slightly more easier, e.g., if
- I declare 'a or 'b as dead
- 'b option or 'b rs is changed to pure 'b
- 'a is dropped
Just wanting to report this,
René
Isabelle: 52dfde98be4a
AFP: 23c1c5591d9f
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
