On Fri, 11 Apr 2014, stvienna wiener wrote:
quad core i7 cpu (i7-3720QM CPU @ 2.60GHz; Isabelle "sees" 8 workers)
This is a relatively recent CPU, with the typical hyperthreading of Intel.
Since that is used by default, you are mostly burning a lot of CPU cycles
without much gain. An explicit threads=4 in the menu Plugin Options /
Isabelle / General should improve the overall reactivity of the system.
$ hg id -i
907f04603177
That is the key information. Any discussion about Isabelle repository
content needs this unique version id to make clear what it is about, even
weeks, months, years later. (Sometimes old mailing list threads are quite
interesting again after a long time.)
$ hg identify --num
56527
That is a physical address, which only applies to a particular local clone
of the Mercurial repository. It is usually useless anywhere else.
Syslog Panel:
Unofficial version of Isabelle/HOL (unidentified repository version)
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
This means that some Isabelle/ML thread ran out if stack, e.g. due to
infinite recursion. It depends on many things if this is a problem, one
needs to figure out somehow which execution got out of control.
[isabelle3@st-pc787 isabelle]$ ./bin/isabelle jedit -l HOL
1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0: Exception in thread
"AWT-EventQueue-0"
1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:
java.lang.NullPointerException
1:27:48 AM [jEdit Worker #4] [error] ErrorListDialog$ErrorEntry:
/home/stephan/Isabelle/repo2/NotepadIssue.thy:
1:27:48 AM [jEdit Worker #4] [error] ErrorListDialog$ErrorEntry: Cannot
list directory.
(the problem above is perhaps due to unreadable files because the files
belong to a different user)
That looks like normal "Java application vomit", maybe just some low-level
file access error that causes an unexpected NPE elsewhere, or the NPE is
actually unrelated.
The look of it is not nice, but so far I don't see a problem here. In
Isabelle/ML, Isabelle/Scala, and Isabelle/jEdit I usually try hard to make
failure as nice as possible, but regular jEdit is sometimes falling into
old-fashioned Java ways.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
