[isabelle-dev] logging and debugging output

Fri Apr 11 00:27:05 CEST 2014

Previously when I found Isabelle/jEdit choking due to JVM memory exhaustion I stuck this in my
~/.isabelle/etc/settings:

  JEDIT_JAVA_OPTIONS="${JEDIT_JAVA_OPTIONS} -Xmx4096m"

This increases the JVM heap size to 4GB. Having said that, the Java exception trace you posted below
doesn't look to me like JVM memory exhaustion.

Isabelle masters, please correct me if I'm wrong or if this is bad advice.

On 11/04/14 08:11, stvienna wiener wrote:
>
>
>
> 2014-04-02 10:47 GMT+02:00 Makarius <makarius at sketis.net <mailto:makarius at sketis.net>>:
>
>     On Wed, 2 Apr 2014, stvienna wiener wrote:
>
>     What is your OS and hardware platform (memory, number of cores)?
>
>
> I am running a 64-bit arch linux distribution, but without any 32-bit compatibility libraries. I
> have a labtop with a quad core i7 cpu (i7-3720QM CPU @ 2.60GHz; Isabelle “sees” 8 workers), 16GB of
> memory and a fast SSD.
>
>
> What is the right way to allocate more memory to Isabelle/JEdit from the start on? I mean I have
> 16GB and it seems with the default settings JEdit uses only 1 GB.
>
>     If you have an exception trace, the obvious thing is to show that here.
>
>
>
> *I am running Isabelle development version*
>
> $ hg id -i
>
> 907f04603177
>
> $ hg identify --num
>
> 56527
>
>
> How are issues supposed to be reported? Should I give a snipped in the E-Mail and post the rest to
> pastebin or so? If you have suggestions tell me (I posted the full stacktrace here in the e-mail).
>
>
> *POSSIBLE ISSUE 1*
>
> Syslog Panel:
>
> Unofficial version of Isabelle/HOL (unidentified repository version)
>
> Warning - Unable to increase stack - interrupting thread
>
> Warning - Unable to increase stack - interrupting thread
>
>
> *POSSIBLE ISSUE 2*
>
> [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:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3414)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3405)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> org.gjt.sp.jedit.EditAction$Wrapper.actionPerformed(EditAction.java:212)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2018)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2341)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:402)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.AbstractButton.doClick(AbstractButton.java:376)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:833)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.plaf.basic.BasicMenuItemUI$Handler.mouseReleased(BasicMenuItemUI.java:877)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:289)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Component.processMouseEvent(Component.java:6505)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> javax.swing.JComponent.processMouseEvent(JComponent.java:3320)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Component.processEvent(Component.java:6270)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Container.processEvent(Container.java:2229)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Component.dispatchEventImpl(Component.java:4861)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Container.dispatchEventImpl(Container.java:2287)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Component.dispatchEvent(Component.java:4687)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4832)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.LightweightDispatcher.processMouseEvent(Container.java:4492)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.LightweightDispatcher.dispatchEvent(Container.java:4422)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Container.dispatchEventImpl(Container.java:2273)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Window.dispatchEventImpl(Window.java:2719)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.Component.dispatchEvent(Component.java:4687)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue.dispatchEventImpl(EventQueue.java:735)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue.access$200(EventQueue.java:103)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue$3.run(EventQueue.java:694)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue$3.run(EventQueue.java:692)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.security.AccessController.doPrivileged(Native Method)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:87)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue$4.run(EventQueue.java:708)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue$4.run(EventQueue.java:706)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.security.AccessController.doPrivileged(Native Method)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventQueue.dispatchEvent(EventQueue.java:705)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:242)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:161)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:146)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:138)
>
> 1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
> java.awt.EventDispatchThread.run(EventDispatchThread.java:91)
>
> 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.
>
> 1:28:40 AM [jEdit Worker #2] [error] BufferSaveRequest: Unable to save buffer
> java.io.FileNotFoundException: /home/stephan/Isabelle/repo2/NotepadIssue.thy/Untitled-1 (Not a
> directory)
>
> 1:28:40 AM [jEdit Worker #2] [error] ErrorListDialog$ErrorEntry:
> /home/stephan/Isabelle/repo2/NotepadIssue.thy/Untitled-1:
>
> 1:28:40 AM [jEdit Worker #2] [error] ErrorListDialog$ErrorEntry: Cannot save:
> /home/stephan/Isabelle/repo2/NotepadIssue.thy/Untitled-1 (Not a directory)
>
>
> (the problem above is perhaps due to unreadable files because the files belong to a different user)
>
>
>
>
> Stephan A. (from Vienna)
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.