#530 Confusing Error Log
This report concerns at least Rodin Platform 2.0.1 with Event-B Theory Feature 0.5.0.
When the attached Event-B project (MathExtensions consisting of the theory ThoughtExperiment) is built from scratch (e.g. by first removing all proof files, then running "Clean" with auto-proving on and then interactively pro), the Error Log grows with three occurrences of "java.lang.AssertionError: Unknown expression: q tothepower (s+y)" and three occurrences of "java.lang.AssertionError: Unknown expression: [[2]] tothepower ([[1]]+[[0]])". When the proof obligation "rew1/S/rhs1" is discharged interactively, the Error Log grows with another three occurrences of "java.lang.AssertionError: Unknown expression: [[2]] tothepower ([[1]]+[[0]])". When the project is deleted from the workspace, the Errow Log grows with two occurrences of "Failed to create deployed theories project." The session data and stack traces associated with these messages are displayed below.
No error message or error mark is ever produced into Rodin Problems, Event-B Explorer or Event-B Theory Editor. Nothing special gets observed in interactive proving either. It is actually tempting to consider all the above-mentioned messages in the Error Log as false alarms. However, in experiments with another plugin I have learnt to take the Error Log seriously.
Session Data:
eclipse.buildId=unknown
java.version=1.6.0_22
java.vendor=Sun Microsystems Inc.
BootLoader constants: OS=win32, ARCH=x86, WS=win32, NL=fi_FI
Command-line arguments: -os win32 -ws win32 -arch x86
Stack Traces:
java.lang.AssertionError: Unknown expression: q tothepower (s+y)
at org.eventb.internal.pptrans.translator.IdentityTranslator.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.IdentityTranslatorBase.idTransRelationalPredicate(Unknown Source)
at org.eventb.internal.pptrans.translator.IdentityTranslator.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.decomposeBoundIdentifiers(Unknown Source)
at org.eventb.pptrans.Translator.decomposeIdentifiers(Unknown Source)
at org.eventb.internal.pp.sequent.InputPredicate.translate(Unknown Source)
at org.eventb.internal.pp.sequent.InputPredicate.translate(Unknown Source)
at org.eventb.internal.pp.sequent.InputSequent.translate(Unknown Source)
at org.eventb.pp.PPProof.translate(Unknown Source)
at org.eventb.internal.pp.PPProverCall.run(Unknown Source)
at java.util.concurrent.Executors$RunnableAdapter.call(Unknown Source)
at java.util.concurrent.FutureTask$Sync.innerRun(Unknown Source)
at java.util.concurrent.FutureTask.run(Unknown Source)
at java.lang.Thread.run(Unknown Source)
java.lang.AssertionError: Unknown expression: [[2]] tothepower ([[1]]+[[0]])
at org.eventb.internal.pptrans.translator.IdentityTranslator.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.IdentityTranslatorBase.idTransRelationalPredicate(Unknown Source)
at org.eventb.internal.pptrans.translator.IdentityTranslator.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.IdentityTranslatorBase.idTransBinaryPredicate(Unknown Source)
at org.eventb.internal.pptrans.translator.IdentityTranslator.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translateQPred(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.translate(Unknown Source)
at org.eventb.internal.pptrans.translator.BoundIdentifierDecomposition.decomposeBoundIdentifiers(Unknown Source)
at org.eventb.pptrans.Translator.decomposeIdentifiers(Unknown Source)
at org.eventb.internal.pp.sequent.InputPredicate.translate(Unknown Source)
at org.eventb.internal.pp.sequent.InputPredicate.translate(Unknown Source)
at org.eventb.internal.pp.sequent.InputSequent.translate(Unknown Source)
at org.eventb.pp.PPProof.translate(Unknown Source)
at org.eventb.internal.pp.PPProverCall.run(Unknown Source)
at java.util.concurrent.Executors$RunnableAdapter.call(Unknown Source)
at java.util.concurrent.FutureTask$Sync.innerRun(Unknown Source)
at java.util.concurrent.FutureTask.run(Unknown Source)
at java.lang.Thread.run(Unknown Source)
org.eclipse.core.internal.resources.ResourceException: The resource tree is locked for modifications.
at org.eclipse.core.internal.resources.WorkManager.checkIn(WorkManager.java:115)
at org.eclipse.core.internal.resources.Workspace.prepareOperation(Workspace.java:1914)
at org.eclipse.core.internal.resources.Project.create(Project.java:269)
at org.eclipse.core.internal.resources.Project.create(Project.java:256)
at org.eclipse.core.internal.resources.Project.create(Project.java:249)
at org.eventb.theory.core.TheoryCoreFacade$3.run(TheoryCoreFacade.java:580)
at org.rodinp.internal.core.BatchOperation.executeOperation(Unknown Source)
at org.rodinp.internal.core.RodinDBOperation.run(Unknown Source)
at org.rodinp.core.RodinCore.run(Unknown Source)
at org.eventb.theory.core.TheoryCoreFacade.ensureDeploymentProjectExists(TheoryCoreFacade.java:574)
at org.eventb.theory.core.TheoryCoreFacade.getDeploymentProject(TheoryCoreFacade.java:668)
at org.eventb.theory.rbp.base.RuleBaseManager.processDelta(RuleBaseManager.java:134)
at org.eventb.theory.rbp.base.RuleBaseManager.processDelta(RuleBaseManager.java:128)
at org.eventb.theory.rbp.base.RuleBaseManager.elementChanged(RuleBaseManager.java:112)
at org.rodinp.internal.core.DeltaProcessor$2.run(Unknown Source)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.rodinp.internal.core.DeltaProcessor.notifyListeners(Unknown Source)
at org.rodinp.internal.core.DeltaProcessor.firePostChangeDelta(Unknown Source)
at org.rodinp.internal.core.DeltaProcessor.fire(Unknown Source)
at org.rodinp.internal.core.DeltaProcessor.resourceChanged(Unknown Source)
at org.rodinp.internal.core.DeltaProcessingState.resourceChanged(Unknown Source)
at org.eclipse.core.internal.events.NotificationManager$2.run(NotificationManager.java:291)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.internal.events.NotificationManager.notify(NotificationManager.java:285)
at org.eclipse.core.internal.events.NotificationManager.broadcastChanges(NotificationManager.java:149)
at org.eclipse.core.internal.resources.Workspace.broadcastPostChange(Workspace.java:327)
at org.eclipse.core.internal.resources.Workspace.checkpoint(Workspace.java:381)
at org.eclipse.ltk.core.refactoring.PerformChangeOperation$1.run(PerformChangeOperation.java:263)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:1975)
at org.eclipse.ltk.core.refactoring.PerformChangeOperation.executeChange(PerformChangeOperation.java:306)
at org.eclipse.ltk.internal.ui.refactoring.UIPerformChangeOperation.executeChange(UIPerformChangeOperation.java:92)
at org.eclipse.ltk.core.refactoring.PerformChangeOperation.run(PerformChangeOperation.java:218)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:1975)
at org.eclipse.ltk.internal.ui.refactoring.WorkbenchRunnableAdapter.run(WorkbenchRunnableAdapter.java:87)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
This artifact has been marked as a duplicate of artifact 3110755 with reason:
Same bug
This artifact has been marked as a duplicate of artifact 3110755 with reason:
Same bug