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
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
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
On Fri, 25 Apr 2014, Makarius wrote:
trimming it down to the simplest possible approach.
I have done this now in Isabelle/e1317a26f8c0 (and the row of changes
before it).
So most of the PIDE operating system functionality is now
re-implemented by more basic means, in just 48 hours. It
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
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
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,
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
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
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
10 matches
Mail list logo
