Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle on MacBook Pro 2018

view this post on Zulip Email Gateway (Aug 22 2022 at 17:54):

From: Makarius <makarius@sketis.net>
OK, so nothing to do for the Isabelle2018 release.

Note that from Isabelle2017 to Isabelle2018 both Java and jEdit have
changed. If you need to run Isabelle2017 on that machine, you can use
the corresponding Isabelle components from Isabelle2018, e.g. in
$ISABELLE_HOME_USER/etc/settings:

init_components "$HOME/.isabelle/contrib"
"$ISABELLE_HOME/Admin/components/main"

init_component "$HOME/.isabelle/contrib/jdk-8u181"
init_component "$HOME/.isabelle/contrib/jedit_build-20180504"

After "isabelle components -a" it should work.

Side-remark: Isabelle repository clones refer to $HOME/.isabelle as
$ISABELLE_HOME_USER by default. You can keep several clones separate via
something like:

env ISABELLE_IDENTIFIER=Isabelle2017 bin/isabelle jedit

Then $ISABELLE_HOME_USER becomes $HOME/.isabelle/Isabelle2017 as usual.

It would be interesting to know which of the two components needs to be
changed.

For jdk it would mean that Oracle and Apple have been fighting again:
https://youtu.be/OVwsiIKOBsA?t=6m40s

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 18:16):

From: Tobias Nipkow <nipkow@in.tum.de>
I have just tried to run Isabelle 2017 on a MacBook Pro 2018 with Intel Core i9
running High Sierra Version 10.13.8 and it fails with the trace below. That is,
no window starts up, but the process is running and I have to ^C it.

My whole setup was copied across from a MacBook Pro 2016 with Intel Core i7
running High Sierra Version 10.13.6

Tobias

08:17:16 [main] [error] GUIUtilities: error displaying splash screen !
08:17:16 [main] [error] GUIUtilities: java.lang.reflect.InvocationTargetException
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue.invokeAndWait(EventQueue.java:1321)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue.invokeAndWait(EventQueue.java:1296)
08:17:16 [main] [error] GUIUtilities: at
javax.swing.SwingUtilities.invokeAndWait(SwingUtilities.java:1348)
08:17:16 [main] [error] GUIUtilities: at
org.gjt.sp.jedit.GUIUtilities.showSplashScreen(GUIUtilities.java:1957)
08:17:16 [main] [error] GUIUtilities: at
org.gjt.sp.jedit.jEdit.main(jEdit.java:388)
08:17:16 [main] [error] GUIUtilities: at
sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
08:17:16 [main] [error] GUIUtilities: at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
08:17:16 [main] [error] GUIUtilities: at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
08:17:16 [main] [error] GUIUtilities: at
java.lang.reflect.Method.invoke(Method.java:498)
08:17:16 [main] [error] GUIUtilities: at
isabelle.Main$.$anonfun$main$3(main.scala:106)
08:17:16 [main] [error] GUIUtilities: at isabelle.Main$.main(main.scala:115)
08:17:16 [main] [error] GUIUtilities: at isabelle.Main.main(main.scala)
08:17:16 [main] [error] GUIUtilities: Caused by: java.lang.NullPointerException
08:17:16 [main] [error] GUIUtilities: at
sun.font.FontDesignMetrics.getDefaultFrc(FontDesignMetrics.java:157)
08:17:16 [main] [error] GUIUtilities: at
sun.font.FontDesignMetrics.getMetrics(FontDesignMetrics.java:278)
08:17:16 [main] [error] GUIUtilities: at
sun.swing.SwingUtilities2.getFontMetrics(SwingUtilities2.java:1113)
08:17:16 [main] [error] GUIUtilities: at
javax.swing.JComponent.getFontMetrics(JComponent.java:1626)
08:17:16 [main] [error] GUIUtilities: at
org.gjt.sp.jedit.gui.SplashScreen.<init>(SplashScreen.java:42)
08:17:16 [main] [error] GUIUtilities: at
org.gjt.sp.jedit.GUIUtilities$9.run(GUIUtilities.java:1961)
08:17:16 [main] [error] GUIUtilities: at
java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:301)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue.dispatchEventImpl(EventQueue.java:756)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue.access$500(EventQueue.java:97)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue$3.run(EventQueue.java:709)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue$3.run(EventQueue.java:703)
08:17:16 [main] [error] GUIUtilities: at
java.security.AccessController.doPrivileged(Native Method)
08:17:16 [main] [error] GUIUtilities: at
java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:80)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventQueue.dispatchEvent(EventQueue.java:726)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:201)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:116)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:105)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
08:17:16 [main] [error] GUIUtilities: at
java.awt.EventDispatchThread.run(EventDispatchThread.java:82)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: Exception in thread
"AWT-EventQueue-0"
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: java.lang.NullPointerException
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Window.init(Window.java:497)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Window.<init>(Window.java:537)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Frame.<init>(Frame.java:420)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Frame.<init>(Frame.java:385)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.JFrame.<init>(JFrame.java:189)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.View.<init>(View.java:1328)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.jEdit.newView(jEdit.java:2612)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.PerspectiveManager$PerspectiveHandler.endElement(PerspectiveManager.java:363)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.endElement(AbstractSAXParser.java:609)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.dtd.XMLNSDTDValidator.endNamespaceScope(XMLNSDTDValidator.java:266)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.dtd.XMLDTDValidator.handleEndElement(XMLDTDValidator.java:2005)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.dtd.XMLDTDValidator.endElement(XMLDTDValidator.java:879)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanEndElement(XMLDocumentFragmentScannerImpl.java:1782)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl$FragmentContentDriver.next(XMLDocumentFragmentScannerImpl.java:2967)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl.next(XMLDocumentScannerImpl.java:602)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.next(XMLNSDocumentScannerImpl.java:112)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanDocument(XMLDocumentFragmentScannerImpl.java:505)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:841)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:770)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.parsers.XMLParser.parse(XMLParser.java:141)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.parse(AbstractSAXParser.java:1213)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.util.XMLUtilities.parseXML(XMLUtilities.java:140)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.SettingsXML.load(SettingsXML.java:155)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.PerspectiveManager.loadPerspective(PerspectiveManager.java:107)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.jEdit$9.run(jEdit.java:4253)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:311)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue.dispatchEventImpl(EventQueue.java:756)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue.access$500(EventQueue.java:97)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue$3.run(EventQueue.java:709)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue$3.run(EventQueue.java:703)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.AccessController.doPrivileged(Native Method)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:80)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue.dispatchEvent(EventQueue.java:726)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:201)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:116)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:105)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
08:17:17 [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.run(EventDispatchThread.java:82)

[1]+ Done isabelle17 jedit hw_original.thy
lapnipkow1d:Desktop nipkow$
lapnipkow1d:Desktop nipkow$
lapnipkow1d:Desktop nipkow$ isabelle17 jedit
08:18:09 [main] [error] GUIUtilities: error displaying splash screen !
08:18:09 [main] [error] GUIUtilities: java.lang.reflect.InvocationTargetException
08:18:09 [main] [error] GUIUtilities: at
java.awt.EventQueue.invokeAndWait(EventQueue.java:1321)
08:18:09 [main] [error] GUIUtilities: at
java.awt.EventQueue.invokeAndWait(EventQueue.java:1296)
08:18:09 [main] [error] GUIUtilities: at
java
[message truncated]

view this post on Zulip Email Gateway (Aug 22 2022 at 18:16):

From: Tobias Nipkow <nipkow@in.tum.de>
PS It seems to work fine with a recent version of Isabelle (c9570658e8f1).
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 18:16):

From: Makarius <makarius@sketis.net>
That version is relatively old (20-Jul-2018).

How does it work with Isabelle2018-RC4? E.g. from
http://isabelle.in.tum.de/website-Isabelle2018-RC4

I want to make that final today or tomorrow, but don't want to see odd
conflicts between Oracle and Apple.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 18:16):

From: Tobias Nipkow <nipkow@in.tum.de>
On 14/08/2018 10:24, Makarius wrote:

On 14/08/18 08:42, Tobias Nipkow wrote:

PS It seems to work fine with a recent version of Isabelle (c9570658e8f1).

That version is relatively old (20-Jul-2018).

How does it work with Isabelle2018-RC4? E.g. from
http://isabelle.in.tum.de/website-Isabelle2018-RC4

Seems to work fine.

Tobias

I want to make that final today or tomorrow, but don't want to see odd
conflicts between Oracle and Apple.

Makarius

smime.p7s

Last updated: Nov 21 2024 at 12:39 UTC