On 25 Jul 2014, at 11:20 am, Makarius wrote:
> On Fri, 25 Jul 2014, Gerwin Klein wrote:
>
>>
>> On 25 Jul 2014, at 10:23 am, Makarius wrote:
>>
>>> Oddly, people are still seen using 'find_theorems' etc. inlined into the
>>> source text. That was an intermediate approach from several years ago
On Fri, 25 Jul 2014, Gerwin Klein wrote:
On 25 Jul 2014, at 10:23 am, Makarius wrote:
Oddly, people are still seen using 'find_theorems' etc. inlined into the source
text. That was an intermediate approach from several years ago. If it is still
used today, what are the remaining resons fo
On 25 Jul 2014, at 10:23 am, Makarius wrote:
> Oddly, people are still seen using 'find_theorems' etc. inlined into the
> source text. That was an intermediate approach from several years ago. If it
> is still used today, what are the remaining resons for it?
Not having to touch the mouse is
On Fri, 27 Jun 2014, Makarius wrote:
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
On Fri, 27 Jun 2014, Makarius wrote:
On Fri, 27 Jun 2014, Peter Lammich wrote:
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
Hi Makarius,
On Thu, Jun 26, 2014 at 11:08 PM, Makarius wrote:
> 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.
I am using Isabelle via ProofGeneral on a s
On Sun, 29 Jun 2014, Cezary Kaliszyk wrote:
Hi Makarius,
On Thu, Jun 26, 2014 at 11:08 PM, Makarius wrote:
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.
On 27.06.2014 23:47, Makarius wrote:
> 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 ML mode.
For ML files, I occasionally had the problem t
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 ML
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 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 th
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 your
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 p
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 the
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 apply-s
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:
* 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 th
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 scro
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 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:
* 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 sledgehammerin
> 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 sh
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
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 ubun
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 defa
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 bar
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 unavoi
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 t
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 rel
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
> shortc
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 woul
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
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
On Sun, 25 May 2014, Jasmin Blanchette wrote:
-n no build dialog for session image on startup
I thought this only controlled whether the dialog is shown; not whether
the build takes place.
That was once a separate build_dialog tool, but it is now just an implicit
build, so I wi
Am 25.05.2014 um 14:59 schrieb Makarius :
> On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
>
>> In the course of a day, I typically find myself pulling from the Isabelle
>> repository several times. I am encouraged in this by my use of Mercurial
>> queues. So it's not untypical that m
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
In the course of a day, I typically find myself pulling from the
Isabelle repository several times. I am encouraged in this by my use of
Mercurial queues. So it's not untypical that my HOL image is slightly
out of date, usually in a harml
> (For now the list of Remaining uses of Proof General / Emacs seems to be
> empty. If there is anything remaining, this thread is still open to
> submissions.)
Let me make this list nonempty again.
In the course of a day, I typically find myself pulling from the Isabelle
repository several t
This is not a remaining use of Proof General, but of the Emacs text
editor: trimming the final newline of theory sources for document
preparation. This could lead to extra white space between sections in the
last decades, but it was just one of these habits to take care of that
manually.
jEd
On Tue, 29 Apr 2014, Matthew Fernandez wrote:
Currently most of my theories are generated by another tool. When
debugging the generated theories, I often have to open a file that I
know contains many broken proofs. In these circumstances it can be
beneficial to have a way of stepping into the
Thanks a lot.
Andreas
On 12/05/14 20:07, Florian Haftmann wrote:
1. Violation of well-sortedness constraints: type ... not an instance of
...
declare [[show_sorts]]
code_thms
Then, I use educated guessing and Emacs' incremental search to navigate
the code equations that have been output unti
The list of remaining uses of Proof General is shrinking dramatically
every day. We can continue this a bit more during May, all referring to
ongoing repository development.
During the month of June, I will be mostly on vacation. After that the
convergence towards the release needs to start.
> 1. Violation of well-sortedness constraints: type ... not an instance of
> ...
>
> declare [[show_sorts]]
> code_thms
>
> Then, I use educated guessing and Emacs' incremental search to navigate
> the code equations that have been output until I find the fault --
> usually, it's just a missing
On Thu, 8 May 2014, David Matthews wrote:
On 08/05/2014 11:25, Makarius wrote:
That sounds rather obvious, but also like even more complication.
David Matthews has provided a nice simplified version of pthreads in
Poly/ML. He could probably do more, but even on the more complex JVM
the inf
On Tue, 29 Apr 2014, Thomas Sewell wrote:
Back to the actual technical questions. What are the main performance
bottle-necks here? Printing of intermediate goal states? Or applying
intermediate steps repeatedly?
I suspect that the problem is not that the printing or the intermediate
calc
On Fri, 2 May 2014, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
Until then there are various approximations:
* Multiple floating instances of Output, with different Update / Auto
update state.
* The Output / Detach button to produce an unchanging Info window on the
On 08/05/2014 11:25, Makarius wrote:
On Thu, 8 May 2014, Thomas Sewell wrote:
If I knew a proper way to reduce the priority (or to pre-empt) worker
threads for that, I would do it. But it probably needs some work by
David Matthews on the ML thread infrastructure.
Preempting long-running t
On Thu, 8 May 2014, Thomas Sewell wrote:
If I knew a proper way to reduce the priority (or to pre-empt) worker
threads for that, I would do it. But it probably needs some work by
David Matthews on the ML thread infrastructure.
Consider me an unashamed pragmatist.
The important point is t
Thanks Makarius.
A few of us at NICTA have ported this change to our various versions of
Isabelle and begun playing with it. It seems to improve the situation
sometimes, though we haven't yet got a feel for when in particular it
helps. In fact, we haven't really understood what the change does
On Fri, 2 May 2014, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
> text ‹
> @{term ‹A \un B›}
> ›
>
> Here the \un works as expected -- the cartouche remains intact
> independently of its
> content, as long as the funny parentheses are nested properly.
But t
On Mon, 5 May 2014, Makarius wrote:
Users running on batteries might also want a mode that restricts all
threads to the behaviour above.
Have you tried that with "threads = 1" (there is also a special treatment for
high-priority prints in that mode)? So far I guess that most people run wit
On Mon, 5 May 2014, Thomas Sewell wrote:
The basic assumption is that each proof task does not run too long, and if
it does it is something to be improved in the application to make it more
smooth. In contrast, Proof General makes it more easy to produce huge and
heavy proof scripts that ca
On 03/05/14 00:05, Makarius wrote:
On Tue, 29 Apr 2014, Thomas Sewell wrote:
I tried an adjustment a while ago in which I had the goal state print
incrementally. Even if some of the subgoals took a while to print,
you'd see the line with "goal (12 subgoals)" immediately, and then
the subgoals
On Fri, 2 May 2014, Andreas Lochbihler wrote:
The reason is that I often add the delimiters only later. For example, when I
write a single-identifier term, I use
text {* @{term my_constant} *}
and some time later, I figure out that I have to add something, e.g., a type
constraint. Hence, I p
On 02/05/14 16:16, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
text ‹
@{term ‹A \un B›}
›
Here the \un works as expected -- the cartouche remains intact
independently of its
content, as long as the funny parentheses are nested properly.
But this correct nesting is
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
There are hardly any performance problems in terms of computing power,
possibly except for Isabelle processing a slow call to auto over and
over again. The efficiency problem is the interaction with the IDE. I
use the Find panel a lot, but then my
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
text ‹
@{term ‹A \un B›}
›
Here the \un works as expected -- the cartouche remains intact
independently of its
content, as long as the funny parentheses are nested properly.
But this correct nesting is exactly the problem. When I type \un
On Tue, 29 Apr 2014, Thomas Sewell wrote:
I tried an adjustment a while ago in which I had the goal state print
incrementally. Even if some of the subgoals took a while to print, you'd
see the line with "goal (12 subgoals)" immediately, and then the
subgoals as they were formatted. The short s
But I try to process such
theories with jEdit and only go back to XEmacs/PG when I cannot stand
Isabelle/jEdit any longer (which usually happens when I debug the code
generator setup).
That's an interesting observation. What are the particular properties
of »debugging« here that make PG prefera
> But I try to process such
> theories with jEdit and only go back to XEmacs/PG when I cannot stand
> Isabelle/jEdit any longer (which usually happens when I debug the code
> generator setup).
That's an interesting observation. What are the particular properties
of »debugging« here that make PG p
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
* What are your exact hardware parameters: CPU, main memory?
Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory
That is a recent high-end laptop or a midrange desktop machine.
JinjaThreads is *the* biggest Isabelle application on the planet, i
>> What is funny is that Proof General was actually one of the main
>> reasons of moving only
>> slowly in such token language reforms.
> I am glad that PG still works for most of my theories and I try to keep
> that state as long as feasible. There are already problems with new
> keywords declared
On 28/04/14 22:25, Makarius wrote:
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
My main usage of PG is when I want to construct a complicated proof method call
like
(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp
del: ...)+
that collapses an apply script of
On 28/04/14 23:18, Makarius wrote:
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
2. Reactivity when processing large files
With PG, I knew how to control the Isabelle prover. When I edit a large file in
a larger
project like JinjaThreads, every now and then, Isabelle changes the background
Hi Makarius,
On 28/04/14 23:10, Makarius wrote:
a) Given some text like
definition foo where "foo = ..."
when I add an attribute like [simp]: after the where, I get a symbol completion
popup to
replace the : with the element sign. Usually, my next thing is to move the
cursor with
the cursor
Back to the actual technical questions. What are the main performance
bottle-necks here? Printing of intermediate goal states? Or applying
intermediate steps repeatedly?
I suspect that the problem is not that the printing or the intermediate
calculations are taking too long. It's that
On 29/04/14 01:04, Makarius wrote:
On Mon, 28 Apr 2014, Matthew Fernandez wrote:
My reasons are mostly predictable execution, as I can control what the prover
is up to with
explicit stepping forwards and backwards. I can probably achieve the same
result toggling
continuous checking on/off in I
On Mon, 28 Apr 2014, Peter Lammich wrote:
1. I cannot really control what Isabelle/Jedit processes when, and it
invests computation power on the meaningless parts of the file
directly after the point where I am editing. I'm not even convinced
that it is the right approach to let Isabell
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
2. Reactivity when processing large files
With PG, I knew how to control the Isabelle prover. When I edit a large
file in a larger project like JinjaThreads, every now and then, Isabelle
changes the background colour from red to gray and then, ap
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
a) Given some text like
definition foo where "foo = ..."
when I add an attribute like [simp]: after the where, I get a symbol
completion popup to replace the : with the element sign. Usually, my
next thing is to move the cursor with the cursor k
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
My main usage of PG is when I want to construct a complicated proof method
call like
(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ...
simp del: ...)+
that collapses an apply script of a hundred lines. I haven't yet fou
On Mon, 28 Apr 2014, Matthew Fernandez wrote:
On 28/04/14 04:14, Makarius wrote:
Are there any remaining uses of Proof General, e.g. in the situation of
current
Isabelle/5b6f4655e2f2 ?
I'm mostly on Isabelle/jEdit now, but I do delve back into
Isabelle/Emacs (is that the current terminolo
I'm still a regular user of PG. From time to time, I test
Isabelle/jEdit, and my reasons for switching back to PG are somewhat
similar to what Andreas reported. My main problems with Isabelle/JEdit
are:
1. I cannot really control what Isabelle/Jedit processes when, and it
invests computation power
Hi Makarius,
Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and
ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to
working on small projects or refactoring existing sources. I really like the negative line
spacing set
On 28/04/14 04:14, Makarius wrote:
> Are there any remaining uses of Proof General, e.g. in the situation of
current
> Isabelle/5b6f4655e2f2 ?
I'm mostly on Isabelle/jEdit now, but I do delve back into Isabelle/Emacs (is
that the current
terminology for this creature?) every now and then. My re
On Sun, 27 Apr 2014, Manuel Eberl wrote:
I am not, as it were, a user of Proof General anymore; however, I would
like, if I may, to point out one thing that annoys me in jEdit and that
was, in my opinion, better in Proof General: the handling of
abbreviations for Unicode characters.
Please not
Hallo,
I am not, as it were, a user of Proof General anymore; however, I would
like, if I may, to point out one thing that annoys me in jEdit and that
was, in my opinion, better in Proof General: the handling of
abbreviations for Unicode characters.
The current behaviour with “immediate completio
Are there any remaining uses of Proof General, e.g. in the situation of
current Isabelle/5b6f4655e2f2 ?
This is neither a joke nor a running gag -- I just can't think of anything
myself after the introduction of the spell checker.
Makarius
78 matches
Mail list logo
