Fresh installation lacks `instantiation` (first try to apply rule) folder:

[Robert-Brune]

Description

Dialogue window for rules does not open the first time after fresh installation.
After a restart of KeY it is suddenly available.

Reproducible

always (after fresh installation)

Can be resolved by just closing and restarting KeY,
as the missing directory is found then.

Steps to reproduce

1. "Fresh" KeY installation mv ~.key ~.key-old
2. Open example (e.g. KeY Book / Chapter 15 / Building Propositional Proof)
3. Try to apply Rule local cut (or different rule requiring user input)
   • This triggers the error message (see stack trace).
   • No dialogue is opened.
   • This also creates the missing directory ~/.key/v3.0/instantiations .
   • Also following tries to apply such a rule always recreate the error message and no dialogue opens.
4. Restart KeY
5. Open example
6. Apply rule successfully (the dialogue opens)

Works analogous with KeY Book / Chapter 15 / Building First Order Proof and rule allLeft.

Additional information

Compare last statement ~/.key/instantiations which should be, ~/.key/v3.0/instantiations [~for user home dir]

[16:42:54.282] INFO  AbstractProblemLoader - Replay result: Proof replayed successfully.
Exception in thread "AWT-EventQueue-0" java.lang.ExceptionInInitializerError
	at de.uka.ilkd.key.control.AbstractProofControl.completeAndApplyApp(AbstractProofControl.java:361)
	at de.uka.ilkd.key.control.AbstractProofControl.selectedTaclet(AbstractProofControl.java:235)
	at de.uka.ilkd.key.control.AbstractProofControl.selectedTaclet(AbstractProofControl.java:201)
	at de.uka.ilkd.key.ui.MediatorProofControl.selectedTaclet(MediatorProofControl.java:68)
	at de.uka.ilkd.key.gui.nodeviews.CurrentGoalView.selectedTaclet(CurrentGoalView.java:252)
	at de.uka.ilkd.key.gui.nodeviews.CurrentGoalViewMenu$TacletAppAction.actionPerformed(CurrentGoalViewMenu.java:864)
	at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972)
	at java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2314)
	at java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:407)
	at java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)
	at java.desktop/javax.swing.AbstractButton.doClick(AbstractButton.java:374)
	at java.desktop/javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:986)
	at java.desktop/javax.swing.plaf.basic.BasicMenuItemUI$Handler.mouseReleased(BasicMenuItemUI.java:1030)
	at java.desktop/java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:299)
	at java.desktop/java.awt.Component.processMouseEvent(Component.java:6621)
	at java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3398)
	at java.desktop/java.awt.Component.processEvent(Component.java:6386)
	at java.desktop/java.awt.Container.processEvent(Container.java:2266)
	at java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4996)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2324)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4828)
	at java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4948)
	at java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4575)
	at java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4516)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2310)
	at java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2780)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4828)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:775)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:720)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:714)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:400)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:87)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:98)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:747)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:745)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:400)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:87)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:744)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)
Caused by: java.lang.RuntimeException: java.nio.file.NoSuchFileException: ~/.key/instantiations
	at de.uka.ilkd.key.control.InstantiationFileHandler.getStoragePath(InstantiationFileHandler.java:59)
	at de.uka.ilkd.key.control.InstantiationFileHandler.<clinit>(InstantiationFileHandler.java:23)
	... 44 more
Caused by: java.nio.file.NoSuchFileException: /Users/robert/.key/instantiations
	at java.base/sun.nio.fs.UnixException.translateToIOException(UnixException.java:92)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:106)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:111)
	at java.base/sun.nio.fs.UnixFileAttributeViews$Basic.readAttributes(UnixFileAttributeViews.java:55)
	at java.base/sun.nio.fs.UnixFileSystemProvider.readAttributes(UnixFileSystemProvider.java:171)
	at java.base/java.nio.file.Files.readAttributes(Files.java:1854)
	at java.base/java.nio.file.FileTreeWalker.getAttributes(FileTreeWalker.java:220)
	at java.base/java.nio.file.FileTreeWalker.visit(FileTreeWalker.java:277)
	at java.base/java.nio.file.FileTreeWalker.walk(FileTreeWalker.java:323)
	at java.base/java.nio.file.FileTreeIterator.<init>(FileTreeIterator.java:71)
	at java.base/java.nio.file.Files.walk(Files.java:3911)
	at java.base/java.nio.file.Files.walk(Files.java:3966)
	at de.uka.ilkd.key.control.InstantiationFileHandler.getStoragePath(InstantiationFileHandler.java:50)
	... 45 more

---

• Commit: 56541d