Hi René,
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
...
Just wanting to report this,
Thank you for your report. This is now fixed (cf.
On 27.06.2014 07:52, John Wickerson wrote:
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.
On Fri, 27 Jun 2014, Peter Lammich wrote:
I have compiled a list of problems that I encountered during my work.
OK, I will go through it one by one to eliminate them -- either by
pointing out known ways how to do it in Isabelle/jEdit, or by fine-tuning
the system in this stage before the
On Fri, 27 Jun 2014, Peter Lammich wrote:
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.
Better reverse all that, just
On Fri, 27 Jun 2014, Peter Lammich wrote:
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
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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.
The
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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.
That clickable area is convenient, but not strictly necessary. It is
absent in PG anyway. Whenever the Prover IDE outputs an error message,
e.g. in tooltips or the Output panel, it includes the source position
information, *if* that is available.
The problem is, that I cannot make the
The default guess is that the JVM has too little heap space. You have
called 4 GB unreasonably large before, which is an indication that your
defaults are far too low.
OK, I'll try more on my 8Gb machine ... or upgrade my machine.
If problems happen again with 4-8 GB JVM heap, you
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fri, 27 Jun 2014, Peter Lammich wrote:
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)
Other people have given some hints already.
You should also take the time to *print* and
On Fr, 2014-06-27 at 13:58 +0200, Makarius wrote:
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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.
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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,
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fri, 27 Jun 2014, Peter Lammich wrote:
If problems happen again with 4-8 GB JVM heap, you should describe what
really happens, with clear experimental setup.
Giving a clear experimental setup is a real problem for errors that
appear nondeterministically.
The first thing is to describe
On Fri, 27 Jun 2014, Peter Lammich wrote:
* Regular messages (writeln, warning, error) also appear in the
squiggly rendering of the sources, to be hovered over and inspected
without scrolling *the* Output. There is in fact no reason to have
just one (or two or three) focal
On Fri, 27 Jun 2014, Makarius wrote:
On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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
On Fr, 2014-06-27 at 14:22 +0200, Makarius wrote:
On Fri, 27 Jun 2014, Peter Lammich wrote:
If problems happen again with 4-8 GB JVM heap, you should describe what
really happens, with clear experimental setup.
Giving a clear experimental setup is a real problem for errors that
appear
Some more explanations on the meta-model of this thread:
* We have about 1 week left on isabelle-dev, to discuss whatever might
prevent using Isabelle/jEdit smoothly, and why people fall-back on PG
as a reflex.
* Then there will be Isabelle2014-RC0, as a published release candidate,
On Mon, 16 Jun 2014, John Wickerson wrote:
This mailing list is for Isabelle developers, not Isabelle users.
This sounds like isabelle-dev would be an exclusive member's only club,
which it isn't. The Isabelle front-page explains the mailing list like
this:
* isabelle-...@in.tum.de
I occasionally get a modal dialog reporting that a the file I currently edit
was changed on disk by another program and therefore automatically reloaded. I
didn't touch or modify the program myself, and ls -l does not indicate a recent
modification either.
This is for a fairly recent
On Fri, 27 Jun 2014, Clemens Ballarin wrote:
I occasionally get a modal dialog reporting that a the file I currently
edit was changed on disk by another program and therefore automatically
reloaded. I didn't touch or modify the program myself, and ls -l does
not indicate a recent
On Fri, 27 Jun 2014, Peter Lammich wrote:
* Writing tools in ML (ML-blocks in thy-file)
Just a side remark: in the repository version we are talking about, and
thus the coming release, ML in auxiliary files works smoothly and often
better than the ML blocks, because the file gets its own
27 matches
Mail list logo
