Issue with 2023 CADE example
When trying to build this file - https://gl.mathhub.info/MMT/LATIN2/-/blob/master/source/casestudies/2023-cade/test-mmt-based-prover.msl?ref_type=heads I got the following error. This is a sample of the output from near the end, I can post the whole output if necessary.
debug: scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
debug: info.kwarc.mmt.api.frontend.actions.ExecActionHandling.runMSLFile(ExecAction.scala:48)
debug: info.kwarc.mmt.api.frontend.actions.ExecActionHandling.runMSLFile$(ExecAction.scala:40)
debug: info.kwarc.mmt.api.frontend.Controller.runMSLFile(Controller.scala:74)
debug: info.kwarc.mmt.api.frontend.RunFile.doIt(Make.scala:80)
debug: info.kwarc.mmt.api.frontend.RunFile.run(Make.scala:71)
debug: info.kwarc.mmt.api.frontend.Shell.deferToExtension(Shell.scala:88)
debug: info.kwarc.mmt.api.frontend.Shell.mainRaw(Shell.scala:151)
debug: info.kwarc.mmt.api.frontend.Shell.main(Shell.scala:58)
debug: info.kwarc.mmt.api.frontend.Run.main(Shell.scala)
error: (error) unbound token: @
error: (error) unbound token: ?
error: (error) unbound token: @
error: (error) unbound token: ,
error: (error) unbound token: @
error: (error) unbound token: ?
error: (error) unbound token: @
error: (error) unbound token: ,
error: (error) invalid unit: latin:/?LinearLogic?bang_right?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ ? (WhyNot/diamond @ ?) , A?Bang/box @ Γ ? (WhyNot/diamond @ ?) , !A INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?bang_right?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ ? (WhyNot/diamond @ ?) , A?Bang/box @ Γ ? (WhyNot/diamond @ ?) , !A INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?bang_right?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ ? (WhyNot/diamond @ ?) , A?Bang/box @ Γ ? (WhyNot/diamond @ ?) , !A INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?bang_right?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ ? (WhyNot/diamond @ ?) , A?Bang/box @ Γ ? (WhyNot/diamond @ ?) , !A INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?bang_right?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ ? (WhyNot/diamond @ ?) , A?Bang/box @ Γ ? (WhyNot/diamond @ ?) , !A INHABITABLE
error: (error) unbound token: @
error: (error) unbound token: ,
error: (error) unbound token: ?
error: (error) unbound token: @
error: (error) unbound token: @
error: (error) unbound token: ,
error: (error) unbound token: ?
error: (error) unbound token: @
error: (error) invalid unit: latin:/?LinearLogic?whynot_left?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ , A ? WhyNot/diamond @ ??Bang/box @ Γ , ?(A ? WhyNot/diamond @ ?) INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?whynot_left?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ , A ? WhyNot/diamond @ ??Bang/box @ Γ , ?(A ? WhyNot/diamond @ ?) INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?whynot_left?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ , A ? WhyNot/diamond @ ??Bang/box @ Γ , ?(A ? WhyNot/diamond @ ?) INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?whynot_left?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ , A ? WhyNot/diamond @ ??Bang/box @ Γ , ?(A ? WhyNot/diamond @ ?) INHABITABLE
error: (error) invalid unit: latin:/?LinearLogic?whynot_left?type: Judgment |-- {A}{Γ,?}Bang/box @ Γ , A ? WhyNot/diamond @ ??Bang/box @ Γ , ?(A ? WhyNot/diamond @ ?) INHABITABLE
error: (error) unbound token: ¬
error: (error) unbound token: ?
Exception in thread "main" java.lang.StackOverflowError
at scala.collection.immutable.List.prependedAll(List.scala:148)
at scala.collection.immutable.List$.from(List.scala:651)
at scala.collection.immutable.List$.from(List.scala:648)
at scala.collection.IterableFactory.apply(Factory.scala:103)
at scala.collection.IterableFactory.apply$(Factory.scala:103)
at scala.collection.immutable.List$.apply(List.scala:648)
at info.kwarc.mmt.api.utils.URI.pathNoTrailingSlash(URI.scala:110)
at info.kwarc.mmt.api.DPath.equals(Path.scala:92)
at info.kwarc.mmt.api.MPath.equals(Path.scala:140)
at scala.runtime.BoxesRunTime.equals2(BoxesRunTime.java:133)
at scala.runtime.BoxesRunTime.equals(BoxesRunTime.java:119)
at scala.collection.mutable.HashMap$Node.findNode(HashMap.scala:611)
at scala.collection.mutable.HashMap.get(HashMap.scala:88)
at info.kwarc.mmt.api.libraries.ModuleHashMap.get(Library.scala:21)
at info.kwarc.mmt.api.libraries.Library.$anonfun$modulesGetRoot$1(Library.scala:99)
at info.kwarc.mmt.api.utils.MyList.mapFind(MyList.scala:10)
at info.kwarc.mmt.api.libraries.Library.modulesGetRoot(Library.scala:98)
at info.kwarc.mmt.api.libraries.Library.info$kwarc$mmt$api$libraries$Library$$getContent(Library.scala:209)
at info.kwarc.mmt.api.libraries.Library.get(Library.scala:128)
at info.kwarc.mmt.api.libraries.Lookup.$anonfun$getO$1(Lookup.scala:37)
at info.kwarc.mmt.api.libraries.Lookup.optional(Lookup.scala:30)
at info.kwarc.mmt.api.libraries.Lookup.getO(Lookup.scala:37)
at info.kwarc.mmt.api.libraries.Library.getInTheory(Library.scala:426)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInElement(Library.scala:371)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInTerm(Library.scala:262)
at info.kwarc.mmt.api.libraries.Library.get(Library.scala:138)
at info.kwarc.mmt.api.libraries.Library.makeAssignment$1(Library.scala:246)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInTerm(Library.scala:339)
at info.kwarc.mmt.api.libraries.Library.$anonfun$getAssignmentInModuleOrLink$5(Library.scala:573)
at scala.Option.foreach(Option.scala:437)
at info.kwarc.mmt.api.libraries.Library.$anonfun$getAssignmentInModuleOrLink$4(Library.scala:567)
at info.kwarc.mmt.api.libraries.Library.$anonfun$getAssignmentInModuleOrLink$4$adapted(Library.scala:564)
at scala.collection.immutable.List.foreach(List.scala:333)
at info.kwarc.mmt.api.libraries.Library.getAssignmentInModuleOrLink(Library.scala:564)
at info.kwarc.mmt.api.libraries.Library.getInLink(Library.scala:489)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInElement(Library.scala:382)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInTerm(Library.scala:267)
at info.kwarc.mmt.api.libraries.Library.get(Library.scala:138)
at info.kwarc.mmt.api.libraries.Lookup.$anonfun$getAs$2(Lookup.scala:59)
at info.kwarc.mmt.api.libraries.Lookup.as(Lookup.scala:21)
at info.kwarc.mmt.api.libraries.Lookup.getAs(Lookup.scala:59)
at info.kwarc.mmt.api.libraries.Lookup$ApplyMorphs$.liftedTree1$1(Lookup.scala:245)
at info.kwarc.mmt.api.libraries.Lookup$ApplyMorphs$.traverse(Lookup.scala:244)
at info.kwarc.mmt.api.libraries.Lookup$ApplyMorphs$.traverse(Lookup.scala:238)
at info.kwarc.mmt.api.objects.Traverser.apply(Traverse.scala:41)
at info.kwarc.mmt.api.libraries.Library.mapTerm$1(Library.scala:669)
at info.kwarc.mmt.api.libraries.Library.$anonfun$translateByModuleOrLink$3(Library.scala:686)
at scala.Option.map(Option.scala:242)
at info.kwarc.mmt.api.libraries.Library.$anonfun$translateByModuleOrLink$2(Library.scala:686)
at scala.Option.orElse(Option.scala:477)
at info.kwarc.mmt.api.libraries.Library.translateByModuleOrLink(Library.scala:686)
at info.kwarc.mmt.api.libraries.Library.translateByLink(Library.scala:654)
at info.kwarc.mmt.api.libraries.Library.translate(Library.scala:613)
at info.kwarc.mmt.api.libraries.Library.getInTheory(Library.scala:446)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInElement(Library.scala:371)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInTerm(Library.scala:262)
at info.kwarc.mmt.api.libraries.Library.get(Library.scala:138)
at info.kwarc.mmt.api.libraries.Library.$anonfun$getDeclarationInTerm$5(Library.scala:284)
at scala.Option.foreach(Option.scala:437)
at info.kwarc.mmt.api.libraries.Library.$anonfun$getDeclarationInTerm$4(Library.scala:282)
at info.kwarc.mmt.api.libraries.Library.$anonfun$getDeclarationInTerm$4$adapted(Library.scala:275)
at info.kwarc.mmt.api.objects.Context.$anonfun$mapVarDecls$1(Context.scala:331)
at scala.collection.immutable.List.map(List.scala:250)
at info.kwarc.mmt.api.objects.Context.mapVarDecls(Context.scala:329)
at info.kwarc.mmt.api.libraries.Library.getDeclarationInTerm(Library.scala:275)
at info.kwarc.mmt.api.libraries.Library.get(Library.scala:138)
at info.kwarc.mmt.api.libraries.LookupWithNotFoundHandler.$anonfun$get$2(Lookup.scala:273)
at info.kwarc.mmt.api.frontend.Controller.iterate(Controller.scala:484)
at info.kwarc.mmt.api.frontend.Controller.iterate(Controller.scala:474)
at info.kwarc.mmt.api.frontend.Controller$$anon$1.handler(Controller.scala:328)
at info.kwarc.mmt.api.libraries.LookupWithNotFoundHandler.get(Lookup.scala:273)
at info.kwarc.mmt.api.libraries.Lookup.$anonfun$getO$2(Lookup.scala:56)
at info.kwarc.mmt.api.libraries.Lookup.optional(Lookup.scala:30)
at info.kwarc.mmt.api.libraries.Lookup.getO(Lookup.scala:56)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:202)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
at info.kwarc.mmt.api.uom.RuleBasedSimplifier$$anon$1.traverse(RuleBasedSimplifier.scala:218)
The last lines repeat about a hundred times. Then the installer hangs.
Edited by Patrick Nicodemus