Errors

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.

The "user" and "dev" annotations annotate the most probable target audience.

user: errors when using archives that should work

When you as an end user are advised to use a specific set of archives, which some developer confirmed to work, but these archives do not work for you, then here is a general check list:

• For every archive:

  • Does git status show a clean working directory?
  • Is the archive git pulled at the version the developer advised you to use? Often in fast development cycles, developers advise you to always favor the devel branch (where existent) over the master branch of archives.
  • After git pulling, does git status show a clean working directory? (just to be sure you didn't introduce anything else by accident)

• Are you using the mmt.jar the developer advised you to use? If they advise you to use "the latest devel one", you can ask them if the latest one from the UniFormal/MMT CI suffices.

user|dev: "no backend available that is applicable to "

Quick explanation: A backend is a data structure MMT uses to keep track of everything that has been processed so far (for fast lookup). You can query a backend with an MMT URI to get the actual data structure of the constant/theory/... . Usually, there's multiple backends, one for each archive loaded, that are queried one after the other. If the error above occurs, this means that no backend had any fitting data for that URI.

Common reasons for this error message:

The archive declaring the element referenced by …

• … has not been loaded
  • ⇨ MMT shell: archive add <archive-path>
  • ⇨ API: ctrl.addArchive(…), see the tutorial
• … 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???
• … 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 } where N is not (obviously) not found.
  • e.g. if you references theory Y { include X } where X had 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-bin and build archiveID -mmt-omdoc before the equivalent commands without -.
• … 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?

Alternatively, it is also possible that you are querying for the wrong URI, if you constructed that one separately.

dev: Scala match error even though you are sure you are handling that case

Perhaps you are missing an OMS as below?

case OMBIND(Lambda.path, boundCtx, t) => ???

case OMBIND(OMS(Lambda.path), boundCtx, t) => ???

user|dev: typechecking of constant fails

general tips

Here are some tips if typechecking of a constant fails and none of the error messages tell you anything related to {"X not found", "Y unbound in context"`}. If you do have such error messages, be sure to check the next section out in addition.

The tips are ordered from the (most frequent problems and easiest solutions) to (less frequent and more elaborate solutions).

1. Read your constant declaration again. Should it really typecheck?
2. Have you perhaps mixed up meta-levels/notations?

• For example, in the setting tp: prop, tm: tp -> type with A: tp the constant declaration c: A fails. That's because it needs to be c: tm A. On the meta-level of the object logic being formalized here, of course A is the type. But on the meta-levels above (including the ones for LF and MMT), A is not an inhabitable type, but only tm A is.

3. Read the error messages precisely. Start at the first one. For constants with simple terms (as their type or definienis), you might go through the individual judgements MMT determinde to be checked and see whether they match what you, as a human, would think, too. For more complex terms, this is probably hopeless to go through.

4. Try cleaning and rebuilding the caches:

• build <archive> -mmt-omdoc [<optional specific file relative to soure>]
• build <archive> mmt-omdoc [<optional specific file relative to soure>]

For example, if you work with the MitM/Foundation in the source file source/dir/test.mmt and you suspect the erroneous caches/problems have only been introduced by that file, it suffices to run:

• build MitM/Foundation -mmt-omdoc dir/test.mmt
• build MitM/Foundation mmt-omdoc dir/test.mmt

"X not declared in context"

1. Do you bind a variable with name "X"? E.g. do you have [X] ... in your constant declaration where [.] is LF's lambda?

   • If so, verify that you have not declared any other symbol (incl. constants) in the reachable scope with the same name X. Bound variable names must not clash with symbol names due to bug UniFormal/MMT#543.
   • Even if you have none such symbol declaration with the same name, you might have had one in the past and the caches might still contain it. Clean the caches and rebuild as outlined in the previous section, point 4.

user|dev: "invalid object", "semantic object not found"

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) via build archiveID -scala-bin, build archiveID -mmt-omdoc, build archiveID scala-bin, build archiveID mmt-omdoc.
  TODO: Link to page explaining archive building.