[isabelle-dev] logging and debugging output

[Makarius]

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 at 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