Формальная проверка ключа с помощью Xtext 2.25

#java #eclipse #key-formal-verification

Вопрос:

Я работаю над проектом с формальной проверкой с помощью ключа на Java. Для этого я использую плагин Eclipse. Все работало нормально, когда у меня была Xtext версии 2.10. Однако по некоторым причинам я решил обновить Xtext до 2.25. К сожалению, сейчас я получаю следующую ошибку:

 
!ENTRY org.eclipse.e4.ui.workbench 4 0 2021-05-20 11:22:24.373
!MESSAGE Failed to evaluate: AndExpression [children=[WithExpression [variable=selection, children=[AndExpression [children=[<test property="isGoal" plug-in activation: eager/>]]]]]]
!STACK 0
org.eclipse.core.runtime.CoreException: No property tester contributes a property org.key_project.keyide.ui.isGoal to type class org.eclipse.jface.text.TextSelection
    at org.eclipse.core.internal.expressions.TypeExtensionManager.getProperty(TypeExtensionManager.java:131)
    at org.eclipse.core.expressions.TestExpression.evaluate(TestExpression.java:104)
    at org.eclipse.core.expressions.CompositeExpression.evaluateAnd(CompositeExpression.java:54)
    at org.eclipse.core.expressions.AndExpression.evaluate(AndExpression.java:36)
    at org.eclipse.core.expressions.CompositeExpression.evaluateAnd(CompositeExpression.java:54)
    at org.eclipse.core.expressions.WithExpression.evaluate(WithExpression.java:84)
    at org.eclipse.core.expressions.CompositeExpression.evaluateAnd(CompositeExpression.java:54)
    at org.eclipse.core.expressions.AndExpression.evaluate(AndExpression.java:36)
    at org.eclipse.ui.internal.services.EvaluationReference.evaluate(EvaluationReference.java:79)
    at org.eclipse.ui.internal.services.EvaluationReference.evaluate(EvaluationReference.java:109)
    at org.eclipse.ui.internal.services.EvaluationReference.changed(EvaluationReference.java:103)
    at org.eclipse.e4.core.internal.contexts.TrackableComputationExt.update(TrackableComputationExt.java:108)
    at org.eclipse.e4.core.internal.contexts.EclipseContext.processScheduled(EclipseContext.java:364)
    at org.eclipse.e4.core.internal.contexts.EclipseContext.set(EclipseContext.java:379)
    at org.eclipse.ui.internal.services.EvaluationService$1.changed(EvaluationService.java:79)
    at org.eclipse.e4.core.internal.contexts.TrackableComputationExt.update(TrackableComputationExt.java:108)
    at org.eclipse.e4.core.internal.contexts.EclipseContext.processScheduled(EclipseContext.java:364)
    at org.eclipse.e4.core.internal.contexts.EclipseContext.set(EclipseContext.java:379)
    at org.eclipse.ui.internal.e4.compatibility.SelectionService.handleSelectionChanged(SelectionService.java:85)
    at org.eclipse.ui.internal.e4.compatibility.SelectionService.lambda$0(SelectionService.java:72)
    at org.eclipse.e4.ui.internal.workbench.SelectionAggregator$1.run(SelectionAggregator.java:123)
    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
    at org.eclipse.e4.ui.internal.workbench.SelectionAggregator.notifyListeners(SelectionAggregator.java:120)
    at org.eclipse.e4.ui.internal.workbench.SelectionAggregator$5.lambda$0(SelectionAggregator.java:220)
    at org.eclipse.e4.core.contexts.RunAndTrack.runExternalCode(RunAndTrack.java:59)
    at org.eclipse.e4.ui.internal.workbench.SelectionAggregator$5.changed(SelectionAggregator.java:220)
    at org.eclipse.e4.core.internal.contexts.TrackableComputationExt.update(TrackableComputationExt.java:108)
    at org.eclipse.e4.core.internal.contexts.EclipseContext.processScheduled(EclipseContext.java:364)
    at org.eclipse.e4.core.internal.contexts.EclipseContext.set(EclipseContext.java:379)
    at org.eclipse.e4.ui.internal.workbench.SelectionServiceImpl.setSelection(SelectionServiceImpl.java:34)
    at org.eclipse.ui.internal.e4.compatibility.CompatibilityPart.selectionChanged(CompatibilityPart.java:471)
    at org.eclipse.jface.viewers.Viewer$1.run(Viewer.java:151)
    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
    at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:174)
    at org.eclipse.jface.viewers.Viewer.fireSelectionChanged(Viewer.java:148)
    at org.eclipse.jface.text.TextViewer.fireSelectionChanged(TextViewer.java:2621)
    at org.eclipse.jface.text.TextViewer.selectionChanged(TextViewer.java:2600)
    at org.eclipse.jface.text.TextViewer.setSelectedRange(TextViewer.java:2287)
    at org.eclipse.jface.text.DefaultTextDoubleClickStrategy.doubleClicked(DefaultTextDoubleClickStrategy.java:192)
    at org.eclipse.jface.text.TextViewer$TextDoubleClickStrategyConnector.getPreviousOffset(TextViewer.java:238)
    at org.eclipse.swt.custom.StyledTextListener.handleEvent(StyledTextListener.java:95)
    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:89)
    at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4443)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1512)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1535)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1520)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1324)
    at org.eclipse.swt.custom.StyledText.sendWordBoundaryEvent(StyledText.java:8401)
    at org.eclipse.swt.custom.StyledText.getWordPrevious(StyledText.java:5508)
    at org.eclipse.swt.custom.StyledText.getWordPrevious(StyledText.java:5482)
    at org.eclipse.swt.custom.StyledText.handleMouseDown(StyledText.java:6193)
    at org.eclipse.swt.custom.StyledText.lambda$1(StyledText.java:5796)
    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:89)
    at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4443)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1512)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1535)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1520)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1324)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4229)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3839)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$5.run(PartRenderingEngine.java:1157)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:338)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1046)
    at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:155)
    at org.eclipse.ui.internal.Workbench.lambda$3(Workbench.java:644)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:338)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:551)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:156)
    at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:152)
    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:203)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:401)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:255)
    at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:64)
    at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.base/java.lang.reflect.Method.invoke(Method.java:564)
    at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:653)
    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:590)
    at org.eclipse.equinox.launcher.Main.run(Main.java:1461)
    at org.eclipse.equinox.launcher.Main.main(Main.java:1434)

 

Когда я искал решения, я обнаружил, что другие натыкаются на аналогичную проблему, но с другой библиотекой. Решение состояло в том, чтобы просто обновить библиотеку.
Сайт обновления eclipse с ключа сломан, поэтому я не могу обновить свой проект. Моя текущая версия ключа-Eclipse 1.0.0

Комментарии:

1. возможно, вам следует проверить, где определена цель org.key_project.keyide.ui.и в этом плагине (возможно, org.key_project.keyide.ui) можно активировать, а если нет, то почему бы и нет. вы также должны проверить, где используется org.key_project.keyide.ui.isGoal, и можете ли вы удалить его оттуда

2. Я даже не использую метод цели. Мой проект не запустится, потому что зависимость (org.key_project.keyide.ui) содержит синтаксическую ошибку. Это странно, потому что я скачал последний ключ с GitHub, и там нет org.key_project.keyide.ui.isGoal. Удалось найти только de.uka.ilkd.ключ.ядро.цель и de.uka.ilkd.ключ.доказательство.цель.

3. поиск внутри org.key_project.keyide.ui/plugin.xml (или как бы ни назывался плагин) для цели

4. Плагин активирован из того, что я понял. Вот файл непосредственно из репозитория key_project.

5. что-нибудь еще в журнале ошибок