Re: [isabelle-dev] Annotations in Theories panel not visible
On 01.04.2014 07:54, Lars Noschinski wrote: I've tried on Linux with Swing LF Nimbus, GTK+, Metal, and it all works for me. Do you have any special GUI or font properties? If the problem still persists can you make a screenshot? I made a short video: http://www21.in.tum.de/~noschinl/jedit-annotations.webm. I tested the Metal and Nimbus LF; the font is IsabelleText. This is on a system running Debian stable with Gnome 3.4.2. I couldn't reproduce the behaviour on another machine with Debian testing and Gnome 3.8.4. Looking closer yet again, the annotations don't vanish, but the bars get too wide. If you look at the video above, the Theories panel is redrawn two times before the actual process of proving starts. Each time, the width of the bars increases. After the third iteration, it is wider than the panel. But there is no optical indication for this (e.g., a scrollbar), so it looks like part of the annotations vanish when processing procedes into the hidden part of the panel. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: improved support for Isabelle/ML
Am 31.03.2014 23:14, schrieb Makarius: On Fri, 28 Feb 2014, Makarius wrote: I've made another round of refinements (presently at Isabelle/f7ceebe2f1b5). There were some situations where the change propagation of blobs (auxiliary files) versus theories was not right, leading to an invalid perspective of the latter, and causing it to be rechecked to the bottom whenever it lost its physical editor view. This and some other fine points are now sorted out. Note that the basic model is this: auxiliary files are either managed by the editor (via document updates) or the prover (via file-system access). If that status changes, e.g. by opening or closing some ML file in the editor, the corresponding thy_load command (e.g. 'ML_file') is updated, and the theories rechecked from that point (according to their own perspective, not the whole text as before). Anything apart from that is probably a mistake. I could try harder to manage files always from the editor side, as done for theories, but then we hit the performance problems reported below ... Here are again some refinements towards scalable Isabelle/ML IDE support (presently Isabelle/075397022503): * ML_file references are *not* resolved by default as before, mainly due to performance and resource considerations. * A file that was opened once remains within the persistent document model. This means the effect to recheck a theory hierarchy from the point of that file happens only once, when it is first opened. Later it can be closed and re-opened without any change. * The main portion of semantic ML markup is now maintained persistently in ML, and sent to the Scala side via some Execution.print function, which is asynchronous, depends on perspective, and non-persistent. This means, whenever some already processed ML file is visited in the editor, substantial amounts of reports are sent over the wire on the spot -- there is a deep purple flash seen on the ML_file command. When the file becomes invisible later, these resources are freed after some timeout and the JVM gets a chance to perform GC eventually. With this increasingly complex setup --- scalability is never for free --- I can now process Main.thy with all ML files from src/HOL/Tools/BNF/ into the IDE. The JVM requires less than 1.5 GB and ML about 2 GB. This is great, especially since BNF is now distributed all over HOL---some parts (Ctr_Sugar.thy) are loaded very early, some in the middle (up to BNF_LFP.thy), and some towards the end, even after List.thy (BNF_GFP.thy). Now I can lookup library functions loaded in Ctr_Sugar, when working on the ML files in BNF_GFP without waiting for everything in between to reload. Do I understand the third bullet point correctly, in that closing ML buffers is not required anymore (to save space), since the memory associated to unfocused buffers will be freed by GC eventually? Thanks for the hard work towards the best IDE for a functional programming language! Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Unresponsive Isabelle/jEdit
Currently I have the problem that when opening a file in Multivariate_Analysis it can take quite some time until the theories it depends on are loaded. In this time I/jEdit does not respond to mouse or keyboard input. For example: 1) I'm opening ~~/src/HOL/Multivaraiate_Analysis/Complex_Analysis_Basic.thy 2) I/jEdit loads around 10 theories 3) I/jEdit stops at the end of Topology_Euclidean_Space 4) now I/jEdit is for a couple of minutes not responsible, and uses a lot of cpu resources (top says java, but maybe also poly) 5) this continuous with Cartesian_Euclidean_Space, and so on Before I/jEdit did always react to mouse or keyboard input, even when loading the theries. I tried to bisect the recent changes, and the problem seams to be appear with the changeset 0fc032898b05: back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);). - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Unresponsive Isabelle/jEdit
On Tue, 1 Apr 2014, Johannes Hölzl wrote:
Currently I have the problem that when opening a file in
Multivariate_Analysis it can take quite some time until the theories it
depends on are loaded. In this time I/jEdit does not respond to mouse or
keyboard input.
I tried to bisect the recent changes, and the problem seams to be appear
with the changeset
0fc032898b05: back to cumulative treatment of command status, which is
important for total accounting (amending
8201790fdeb9);).
Thanks for keeping an eye on it, and doing the bisection already.
At first I did not believe the result, because 0fc032898b05 looks quite
innocent. Some hours later, I realized that the use of local value
definition within a 'for' comprehension always entails a 'yield', which
means there is a potentially expensive map of the whole structure involved
(The Scala Language Specification Version 2.9, section 6.19).
The following changeset adddresses that:
# HG changeset patch
# User wenzelm
# Date 1396383901 -7200
# Tue Apr 01 22:25:01 2014 +0200
# Node ID 1a9f569b5b7e16760fc419df8f17e7216be795c7
# Parent a6f8c3566560fd9e8955c7240f4ac19cdc9e037d
some rephrasing to ensure that this becomes cheap foreach and not expensive
map (cf. 0fc032898b05);
diff -r a6f8c3566560 -r 1a9f569b5b7e src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala Tue Apr 01 20:22:25 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Apr 01 22:25:01 2014 +0200
@@ -114,11 +114,11 @@
var finished = 0
var warned = 0
var failed = 0
-for {
- command - node.commands
- states = state.command_states(version, command)
- status = command_status(states.iterator.flatMap(st =
st.status.iterator))
-} {
+for { command - node.commands }
+{
+ val states = state.command_states(version, command)
+ val status = command_status(states.iterator.flatMap(st =
st.status.iterator))
+
if (status.is_running) running += 1
else if (status.is_finished) {
val warning = states.exists(st = st.results.entries.exists(p =
is_warning(p._2)))
The node.commands structure contains all command spans of the theory,
which can be quite substantial especially in Multivariate_Analysis. The
plain iteration over the structure is already a bit slow, but a few
redundant maps of it can be deadly to real-time performance.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] logging and debugging output
Hello I am amazed at all the Isabelle/JEdit improvements of the last two years. It is very impressive! Now I started to use the development version of Isabelle instead of Isabelle 2013-2. My work is much more productive now, e.g., fewer crashes and the GUI is much more responsive. But still, Isabelle/JEdit gets unresponsive and unstable, then finally crashes completely. In most cases this happens after a try0 or try call. I suspect it could be a problem related to a fastforce call. Is there a way to look behind the scenes, e.g., to look at the communication between JEdit and Isabelle? Is there a system console or a logging console or any other way to get more debugging info? (I can only she the NullPointerExceptions in the lower right corner of the JEdit interface, i.e., the pink written message, and by clicking on it a pop up with the error message opens.) Best regards from Vienna, Stephan A. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
