Email Gateway (Aug 18 2022 at 17:38): Email Gateway (Aug 18 2022 at 17:38):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hello,
i hope this is also the right list for jedit stuff.
I disabled the Auto-parsing in Isabelle. as it was the only way, to
disable the Isabelle-parsing. just to read some files.
Now i wanted to reactivate the parsing, so i ticked the option,
restartet jedit and got the following error:
the following plug-in could not be loaded:
/home/nils/Isabelle2011/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar:
Cannot start: java.lang.reflect.InvocationTargetException
Try updating to a newer version of the plug-in.
Workaround: delete the properties file in
.isabelle/Isabelle2011/jedit. jedit will create a new working one.
if you are lucky, you can also copy one of the properties files from
the backup directory in the same location and rename it.
the pre-2011 version of jedit ran much butter on my machine. the new
one has problems clearing the ram, when i load and afterwards close
multiple theory files in a row. for me the auto-trace is not really
useful, as I usually have one or two theories to work on, and some
more, wherein i just want to lookup things. So like it was before, to
enable parsing for every buffer on it's own was better for me.
to mention something positive: i really like the sidekick showing some
sort of outline of the theory.
best regards
Nils
Email Gateway (Aug 18 2022 at 17:39):From: Makarius <makarius@sketis.net>
In the old Proof General model, the user "schedules" everything by hand --
individual commands and theory buffers. This is convenient for experts
who want to control every aspect of the system themselves, but it is also
a bit inefficient. A modern operating system also does the scheduling for
the user, not the user for the operating system.
Session management above means dependency management and scheduling of
checking. For Isabelle/Scala/jEdit in Isabelle2011 I've successfully
removed the old stuff (which was also a lot of work), but managed to
implement only little of the new world order when the release deadline was
approaching. This is why it is still a bit awkward to work with files in
Isabelle/jEdit right now, but you can expect it to get better again next
time.
Makarius
Email Gateway (Aug 18 2022 at 17:39):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
so i'm looking forward to the next version, and in the meantime try to
get some RAM.
thanks for your decision-explanation
Nils
Email Gateway (Aug 18 2022 at 17:40):From: Makarius <makarius@sketis.net>
On Fri, 29 Apr 2011, Nils Jähnig wrote:
i hope this is also the right list for jedit stuff.
Yes, isabelle-users is for everything that is part of official Isabelle
release. In contrast, when you start compiling things on your own from
some repository version you should discuss things on the isabelle-dev
mailing list (and reveal your version via "isabelle version -i").
I disabled the Auto-parsing in Isabelle. as it was the only way, to
disable the Isabelle-parsing. just to read some files. Now i wanted to
reactivate the parsing, so i ticked the option, restartet jedit and got
the following error:the following plug-in could not be loaded:
/home/nils/Isabelle2011/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar:
Cannot start: java.lang.reflect.InvocationTargetException Try updating
to a newer version of the plug-in.
Proper session management is still largely missing, so disabling and
re-enabling these global options is not really supported at the moment.
the pre-2011 version of jedit ran much butter on my machine. the new one
has problems clearing the ram, when i load and afterwards close multiple
theory files in a row.
Resource management is as absent in the 2011 version as in the ones
before, but their might be more content produced. How much RAM do you
have anyway. I think you can work several hours on 2 GB.
for me the auto-trace is not really useful, as I usually have one or two
theories to work on, and some more, wherein i just want to lookup
things. So like it was before, to enable parsing for every buffer on
it's own was better for me.
What is auto-trace?
The continous checking that is always enabled is a corollary of the
absence of session manament. I hope to have that in better shape for the
next Isabelle release -- it also affects the way traditional
batch-processing works, so it all takes a bit longer than anticipated.
Makarius
Email Gateway (Aug 18 2022 at 17:46):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
the pre-2011 version of jedit ran much butter on my machine. the new one
has problems clearing the ram, when i load and afterwards close multiple
theory files in a row.Resource management is as absent in the 2011 version as in the ones before,
but their might be more content produced. How much RAM do you have anyway.
I think you can work several hours on 2 GB.
I have 2 GB of RAM at work. but usually some other programs running
(even without other programs running it freezes sometimes).
It is when I'm looking through other theory-files (which get parsed),
when the RAM gets full.
At home, where I use jedit via Cygwin on Windows, I have 4 GB of RAM,
where it's running smoother. But it actually uses more than 2GB of RAM
(together with Winows).
for me the auto-trace is not really useful, as I usually have one or two
theories to work on, and some more, wherein i just want to lookup things. So
like it was before, to enable parsing for every buffer on it's own was
better for me.What is auto-trace?
I'm sorry, i meant auto-parsing.
The continous checking that is always enabled is a corollary of the absence
of session manament. I hope to have that in better shape for the next
Isabelle release -- it also affects the way traditional batch-processing
works, so it all takes a bit longer than anticipated.
I'm not sure, if I got you right (maybe due to me writing
"auto-trace"). my idea was to get back to the not-enabled checking,
without any options. pressing three keys to activate the parsing is no
big deal. on the other hand I don't see a big advantage in having all
theories parsed without pressing a button (please correct me, if I'm
wrong). how does the absence of session management intefere here?
Nils
Last updated: Apr 20 2024 at 01:05 UTC