Right. For some reason I didn't notice it until now; I was probably overwhelmed with the TLA+learning experience.
On 12.05.2015 12:02, Robert Shore wrote:
> Summary: Cannot create new spec with symbolic link in path.
>
> Version: toolbox 1.5 dated 4-May
> Host: Linux 3.13.0-46-generic #79-Ubuntu SMP Tue Mar 10 20:06:50 UTC
> 2015 x86_64 x86_64 x86_64 GNU/Linux
>
> Details: menu => File => Open spec => Add New Spec. If the root-module
> file path contains a symbolic link, the toolbox reports an internal
> error. The log is the following:
> !ENTRY org.eclipse.core.jobs 4 2 2015-05-11 19:02:22.819
> !MESSAGE An internal error occurred during: "NewSpecWizard job".
> !STACK 0
> org.eclipse.core.runtime.AssertionFailedException: assertion failed:
> at org.eclipse.core.runtime.Assert.isTrue(Assert.java:110)
> at org.eclipse.core.runtime.Assert.isTrue(Assert.java:96)
> at
> org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper.storeRootFilename(PreferenceStoreHelper.java:33)
> at org.lamport.tla.toolbox.spec.Spec.createNewSpec(Spec.java:162)
> at
> org.lamport.tla.toolbox.ui.handler.NewSpecHandler$1.run(NewSpecHandler.java:110)
> at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
>
> Workaround: Make sure that the file path contains no symbolic links
Thanks Robert, we will add it to the list of known problems for 1.5.0.
Hopefully we will be able to remove this restriction in a subsequent
release.
Btw. this restriction is also present in 1.4.8 when one adds a module.
Thus, to avoid inconsistencies the symlink check is now done when the
spec gets imported.
Thanks
Markus
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/qOY8Iqcg7nM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.