-
Notifications
You must be signed in to change notification settings - Fork 13
Errors
ComFreek edited this page Feb 28, 2019
·
8 revisions
Solutions are marked by "⇨", optionally also with a target audience:
- MMT shell: for users of the shell interface, i.e. of
java -jar mmt.jar - API: for users of the API. There's a quickstart tutorial for API users if you haven't read that yet.
Common reasons:
The archive declaring the element referenced by …
- … has not been loaded
- ⇨ MMT shell:
archive add <archive-path> - ⇨ API:
ctrl.addArchive(…), see the tutorial
- ⇨ MMT shell:
- … has not been built before
- ⇨ MMT shell:
archive add <archive-path>,build archiveID scala-bin,build archiveID mmt-omdoc.
- TODO: Link to document explaining build steps of archives](https://github.com/UniFormal/uniformal.github.io/wiki/Issues#documentation-on-how-to-build-archives-w-or-wo-scala-Sources)
- TODO: Link to documentation explaining where the archiveID comes from and which common ones there are (e.g.
MMT/urtheories, …), the tutorial has an explanatory comment in the source code. Maybe expand that as a page on its own?
- ⇨ API: TODO???
- ⇨ MMT shell:
- … has been built, but with errors (or errors from transitive dependencies)
- ⇨ MMT shell: closely inspect the errors, start with the first one!
- e.g. if you references
theory X { a: N }whereNis not (obviously) not found. - e.g. if you references
theory Y { include X }whereXhad errors building
- … has been built with another commit/branch/version of MMT
- ⇨ MMT shell: build as above in step "has not been built before". If you want to be double sure, clean via
build archiveID -Scala-binandbuild archiveID -mmt-omdocbefore the equivalent commands without-.
- ⇨ MMT shell: build as above in step "has not been built before". If you want to be double sure, clean via
- … has been built with another Scala version than the current one
- ⇨ rebuild as above.
TODO How to be sure which Scala version is in use?
- ⇨ rebuild as above.
The errors looks similar to
Exception in thread "main" invalid object (semantic object not found): scala://lf.mmt.kwarc.info?NormalizeCurrying
at info.kwarc.mmt.api.symbols.RuleConstantInterpreter.$anonfun$createRule$2(RuleConstant.scala:59)
at scala.Option.getOrElse(Option.scala:138)
- ⇨ Ensure you added all necessary extensions, most notably the LF plugin:
import info.kwarc.mmt.lf ctrl.extman.addExtension(new lf.Plugin())
- ⇨ Ensure you loaded all necessary archives, most notably
MMT/urtheories,MitM/Foundation
TODO: Link on how to load archives. - ⇨ Ensure all loaded archives have been built with the same Scala, Java and MMT version you are using
⇨ Clean and rebuild all those archives on the MMT shell (started with the Java you're using) viabuild archiveID -scala-bin,build archiveID -mmt-omdoc,build archiveID scala-bin,build archiveID mmt-omdoc.
TODO: Link to page explaining archive building.