Benötigte MMT-Archive für KRMT

Master / Vertiefung Logikbasierte Wissensrepräsentation
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Benötigte MMT-Archive für KRMT
Richtig, weil das bisher nirgends explizit erwähnt wurde:
Um das auf studon verlinkte KRMT-Archiv auch wirklich zu benutzen muss:

  1. Das Archiv im content/MathHub-Ordner von MMT liegen (der sollte beim installieren von MMT (siehe docu) im selben Ordner wie die mmt.jar erstellt worden sein)
  2. folgende Archive müssen ebenfalls vorhanden sein (auch in content/MathHub):
    MMT/LFX, MitM/Foundation
    Ihr findet sie auf gl.mathhub.info, wenn ihr git installiert habt (wovon ich sort-of ausgehe) könnt ihr das auch mit
git clone https://gl.mathhub.info/<archivname>.git

(im richtigen Ordner natürlich, i.e. content/MathHub) erledigen :slight_smile:

3

Also ich hab beide Schritte ausgeführt, bekomme aber Fehler:

4

Irgendwas muss da bei dem Pfad kaputt gegangen sein: content/MathHub sollte die einzelnen Archive beinhalten. Ein Archiv ist dabei ein Ordner, der unterordner „source“, „META-INF“ etc. hat. Insbesondere sollte also zwischen „content/MathHub“ und „source“ noch ein „KRMT“ o.ä. sein.

Wenn er http://mathhub.info/MitM/Foundation?Logic nicht findet, heißt das, dass er das Archiv „MitM/Foundation“ nicht findet. Kannst du überprüfen, dass du das a) tatsächlich hast, es b) in content/MathHub liegt und c) in content/MathHub (oder content selbst) kein META-INF irgendeines anderen Archives liegt, das MMT durcheinanderbringt und dafür sorgt, dass es den ganzen MathHub-Ordner für ein einzelnes archiv hält? :wink:

5

Okay, ich hab die zum Archiv gehörenden Dateien jetzt in ein neues Unterverzeichnis KRMT verschoben. MitM/Foundation und MMT/LFX liegen dort wo sie sein sollen. Es kommen aber immer noch Fehler:

/blabla/KRMT/content/MathHub/KRMT/source/Numbers.mmt
1:error with unknown location: invalid object (unknown identifier: http://mathhub.info/Teaching/KRMT?Meta): http://mathhub.info/Teaching/KRMT?Meta
6:error while parsing: get error: backend: no backend available that is applicable to http://mathhub.info/Teaching/KRMT?Meta
36:error while parsing: get error: backend: no backend available that is applicable to http://mathhub.info/Teaching/KRMT?Meta
53:error while parsing: get error: backend: no backend available that is applicable to http://mathhub.info/Teaching/KRMT?Meta
6

Er findet also die theorie http://mathhub.info/Teaching/KRMT?Meta nicht. Die ist in Algebra.mmt. Damit er die findet kannst du jetzt zwei Dinge tun:

  • Entweder du öffnest einfach die Algebra.mmt ebenfalls in jEdit, dann ist sie im Memory und Numbers.mmt sollte fehlerfrei typechecken.
  • Alternativ kannst du auch das Archiv bauen, indem du in der MMT shell in jEdit (->Console-Plugin) eingibist: “build Teaching/KRMT mmt-omdoc”.

Letzteres geht aber davon aus, dass MMT tatsächlich realisiert, dass die beiden .mmt-Dateien tatsächlich zum Archiv gehören. Dazu braucht es also den source- und den META-INF-Ordner im KRMT-Ordner. Wenn die dateien vorher in MathHub rumlagen würde ich fast raten, dass das problematisch sein könnte - (wo ist denn z.B. der zum repository gehörige .git-Ordner jetzt?).

Im Zweifelsfall würde ich alles zu KRMT gehörige weglöschen und nochmal mit nem ganz normalen Linux/Windows/Whatever-terminal im MathHub ordner ne neue version auschecken, mit “git clone git@gl.mathhub.info:Teaching/KRMT.git” (das sollte das archiv automatisch in den Unterordner KRMT clonen) :slight_smile:

In jedem Falle solltest du aufpassen, dass git noch kapiert, wo das KRMT-Repository hingeklont wurde, da wir das ja im Verlaufe der Vorlesung auch regelmäßig updaten - wenn dann “git pull” nicht funktioniert wird das etwas hässlich :wink: