search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 22 forks source link

View missing assignment in combination with structures causes type checker crash, throws exception. #559

Open rappatoni opened 3 years ago

rappatoni commented 3 years ago

This somewhat contrived example...

namespace http://mathhub.info/Panoptikum/examples❚
fixmeta ur:?LF ❚

theory base =
prop : type ❙
❚

theory struct1 =
include ?base ❙
structure test : ?base =
prop = prop ❙
❚
sth: prop ❙
❚

theory struct2 =
include ?base ❙
structure test2 : ?base =
prop = prop ❙
❚
sth: prop ❙
❚

view breaks : ?struct1 → ?struct2 =
// include ?base❙
sth = sth❙
❚

...leads MMT to throw the following: 

MMT Error: class java.lang.IllegalArgumentException: Invalid range specified: (-1, 0); 
com.intellij.openapi.util.TextRange.assertProperRange(TextRange.java:222)
com.intellij.openapi.util.TextRange.assertProperRange(TextRange.java:217)
com.intellij.openapi.util.TextRange.assertProperRange(TextRange.java:213)
com.intellij.openapi.util.TextRange.<init>(TextRange.java:41)
com.intellij.openapi.util.TextRange.<init>(TextRange.java:30)
com.intellij.openapi.util.TextRange.create(TextRange.java:148)
com.intellij.openapi.util.TextRange.from(TextRange.java:143)
info.kwarc.mmt.intellij.checking.ExtAnnotator.$anonfun$apply$4(Checking.scala:99)
info.kwarc.mmt.intellij.checking.ExtAnnotator.$anonfun$apply$4$adapted(Checking.scala:97)
info.kwarc.mmt.intellij.checking.ExtAnnotator$Jar$1$$anon$3.apply(Checking.scala:47)
jdk.internal.reflect.GeneratedMethodAccessor174.invoke(Unknown Source)
java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
java.base/java.lang.reflect.Method.invoke(Method.java:566)
info.kwarc.mmt.intellij.checking.Checker.$anonfun$check$4(Checker.scala:32) info.kwarc.mmt.intellij.checking.Checker.$anonfun$check$4$adapted(Checker.scala:32) info.kwarc.mmt.intellij.checking.Checker$ErrorForwarder.addError(Checker.scala:62) info.kwarc.mmt.api.ErrorHandler.apply(Error.scala:277) info.kwarc.mmt.api.checking.ExtendedCheckingEnvironment.errorCont(MMTStructureChecker.scala:23) info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$7(MMTStructureChecker.scala:226) scala.Option.flatMap(Option.scala:283) info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:274) info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73) info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96) info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131) info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501) info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:695) info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481) info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readView$1(StructureParser.scala:821) scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18) info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34) info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31) info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237) info.kwarc.mmt.api.parser.KeywordBasedParser.readView(StructureParser.scala:821) info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:421) info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93) scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18) info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34) info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31) info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237) info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93) info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83) info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102) info.kwarc.mmt.api.frontend.Controller.read(Controller.scala:291) info.kwarc.mmt.intellij.checking.Checker.check(Checker.scala:34) jdk.internal.reflect.GeneratedMethodAccessor495.invoke(Unknown Source) java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) java.base/java.lang.reflect.Method.invoke(Method.java:566) scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvokeraw(JavaMirrors.scala:391) scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:395) scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:411) info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:31) info.kwarc.mmt.intellij.checking.ExtAnnotator$Jar$1$.check(Checking.scala:50) info.kwarc.mmt.intellij.checking.ExtAnnotator.$anonfun$apply$5(Checking.scala:110) scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18) info.kwarc.mmt.intellij.MMT.logged(Plugin.scala:191) info.kwarc.mmt.intellij.checking.ExtAnnotator.apply(Checking.scala:109) info.kwarc.mmt.intellij.checking.ExtAnnotator.apply(Checking.scala:15) com.intellij.codeInsight.daemon.impl.AnnotationHolderImpl.applyExternalAnnotatorWithContext(AnnotationHolderImpl.java:203) com.intellij.codeInsight.daemon.impl.ExternalToolPass.doApply(ExternalToolPass.java:217) com.intellij.codeInsight.daemon.impl.ExternalToolPass$1.lambda$run$1(ExternalToolPass.java:184) com.intellij.openapi.application.ReadAction.lambda$run$1(ReadAction.java:52) com.intellij.openapi.application.impl.ApplicationImpl.runReadAction(ApplicationImpl.java:889) com.intellij.openapi.application.ReadAction.compute(ReadAction.java:61) com.intellij.openapi.application.ReadAction.run(ReadAction.java:51) com.intellij.codeInsight.daemon.impl.ExternalToolPass$1.lambda$run$2(ExternalToolPass.java:181) com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcess$2(CoreProgressManager.java:178) com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:658) com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:610) com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:65) com.intellij.openapi.progress.impl.CoreProgressManager.runProcess(CoreProgressManager.java:165) com.intellij.openapi.progress.util.BackgroundTaskUtil.runUnderDisposeAwareIndicator(BackgroundTaskUtil.java:254) com.intellij.codeInsight.daemon.impl.ExternalToolPass$1.run(ExternalToolPass.java:179) com.intellij.util.ui.update.MergingUpdateQueue.execute(MergingUpdateQueue.java:333) com.intellij.util.ui.update.MergingUpdateQueue.execute(MergingUpdateQueue.java:323) com.intellij.util.ui.update.MergingUpdateQueue.lambda$flush$1(MergingUpdateQueue.java:273) com.intellij.util.ui.update.MergingUpdateQueue.flush(MergingUpdateQueue.java:287) com.intellij.util.ui.update.MergingUpdateQueue.run(MergingUpdateQueue.java:242) com.intellij.util.concurrency.QueueProcessor.runSafely(QueueProcessor.java:238) com.intellij.util.Alarm$Request.runSafely(Alarm.java:376) com.intellij.util.Alarm$Request.run(Alarm.java:362) java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515) java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) com.intellij.util.concurrency.SchedulingWrapper$MyScheduledFutureTask.run(SchedulingWrapper.java:220) com.intellij.util.concurrency.BoundedTaskExecutor.doRun(BoundedTaskExecutor.java:216) com.intellij.util.concurrency.BoundedTaskExecutor.access$200(BoundedTaskExecutor.java:27) com.intellij.util.concurrency.BoundedTaskExecutor$1.execute(BoundedTaskExecutor.java:195) com.intellij.util.ConcurrencyUtil.runUnderThreadName(ConcurrencyUtil.java:208) com.intellij.util.concurrency.BoundedTaskExecutor$1.run(BoundedTaskExecutor.java:184) java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128) java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628) java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668) java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665) java.base/java.security.AccessController.doPrivileged(Native Method) java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665) java.base/java.lang.Thread.run(Thread.java:834)
ComFreek commented 3 years ago

Can you reproduce the error when pasting the MMT document into a new file and then hitting typechecking using the MMT IntelliJ plugin?

I've once had a similar, if not the same error: apparently due to some invalid/incomplete change management on the MMT side, the IntelliJ plugin received invalid source refs leading to an exception. I think hitting "clear all" and retypechecking solved it.

PS: You can format code in GitHub via three backticks. I've added them for you :smile: