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.
Installationsdinge für/bis morgen
Sooo, also. Für folgende Dinge wäre es gut, möglichst viel vorzubereiten vor morgen - auch wenn ich mit Problemen rechne / rechnen muss:
1. MMT
Die prinzipielle Installationsanleitung findet ihr hier: https://uniformal.github.io/doc/setup/
Relevant ist hierbei auch jEdit mit dem zugehörigen Plugin. Bitte lest die Dokumentations aufmerksam, wenn es schwierigkeiten gibt, bitte schreien 
Beim installieren erstellt MMT einen “content”-Ordner, in dem üblicherweise MathHub/MMT/urtheories und andere archive automatisch per git geklont werden sollten. Diesen content-Ordner solltet ihr um folgendes Archiv erweitern: https://gl.mathhub.info/Teaching/LBS.
Das ganze wird zusätzlich noch erklärt in unserem KRMT-MMT-Tutorial, das ihr unter https://gl.mathhub.info/Teaching/KRMT findet (unter source/tutorial/mmt-math-tutorial.pdf), das durchzulesen schadet also auch nicht
2. GF C- und Java-Bindings
Hier wird’s jetzt hässlich. Um die java-bindings nutzen zu können braucht ihr die GF sourcen, welche ihr hier findet: https://github.com/GrammaticalFramework/GF. Lest euch jeweils in src/runtime/c und (anschließend!) in src/runtime/java die “anleitungen” durch (es läuft üblicherweise auf “make” und “sudo make install” hinaus) und, falls alles funktioniert, merkt euch wo die libraries hininstalliert wurden/werden 
3. Die MMT-GF-Bridge
…findet ihr hier: https://github.com/UniFormal/GFScala
Ich empfehle euch stark zum damit arbeiten IntelliJ zu benutzen (Enterprise version kostenlos für “Studenten”:=“Menschen mit Uni-Emailadresse” ), hauptsächlich weil ich euch da helfen kann die dependencies anständig einzurichten. Bei Eclipse… you’re on your own 
Was ihr als dependencies braucht ist 1. die mmt.jar und 2. die compilierten/installierten/registrierten/wasauchimmer c- und java-bindings für GF aus dem vorherigen schritt (daher zielordner merken)
IntelliJ-Projekt
- File → New → Project from existing sources, den ordner mit der MMT-GF-Bridge auswählen, im prinzip einfach nur immer weiter klicken.
- Eine beliebige .scala-file im Projekt öffnen; oben sollte eine toolbar aufpoppen “No scala SDK in module” - “add sdk” wählen und scala 2.11.8(!!) benutzen (sonst gibt’s komische versionskonflikte)
- File → Project Structure - > Modules → Im tab “Dependencies” 1. die mmt.jar aus Schritt 1 und 2. den pfad zu dem GF-Bindings aus Schritt 2 als Dependencies hinzufügen (rechts auf das grüne plus, dann “JARs or directories”
So, das Projekt an sich sollte jetzt funktionieren
Zu guter letzt:
1. Pfad in der Datei [m]{path/to/mmt/folder}/content/LBS/source/tutorial/three.mmt[/m]:
Konkret: [m]meta ?LogicSyntax?correspondsTo `{path/to/mmt/folder}/content/LBS/source/tutorial/two.pgf [/m] ({path/to/mmt/folder} Teil umbiegen s.d. er zum lokalen Pfad passt.)
- Klicken auf Build sollte folgende Fehlermeldung geben (in jEdit):
{path/to/mmt/folder}/content/LBS/source/tutorial/three.mmt
5:unbound token: {path/to/mmt/folder}content/LBS/source/tutorial/two.pgf
2. In File [m]{path/to/GFScalaBridge}src/main/scala/info/kwarc/gf/Test.scala[/m] Klasse “DennisTest” wie folgt anpassen:
[m] “/home/jazzpirate/work/mmt/content”, [/m]-> “{path/to/mmt/folder}content/”
[m] prefixes.toList,
“”,
Some(8080),
true,[/m]
[m]Some(“/path/to/logfile.html”)[/m] → Logfile target, nach belieben anpassen
3. (Nur unter Linux)
[m]sudo mv /usr/lib/libpgf.so.0 /usr/lib/libpgf.so.bckp
sudo cp /usr/local/lib/libpgf.so.0 /usr/lib/libpgf.so.0[/m]
Genaueres dazu siehe https://groups.google.com/forum/#!topic/gf-dev/oUpxMbEW7oM
4.Testen: Rechtsklick auf Test.scala → Run ‘GFMMT’
Sollte ohne Fehler durchlaufen.
1 „Gefällt mir“
Nachdem alles von GF nun auf Windows funktioniert (Anleitung folgt), bekomme ich noch folgende Fehlermeldung beim Ausführen von Test.scala:
[quote]Exception in thread “main” java.io.FileNotFoundException: source/tutorial/two.pgf
at org.grammaticalframework.pgf.PGF.readPGF(Native Method)
at info.kwarc.gf.Grammar$.apply(Grammar.scala:24)
at info.kwarc.gf.MMTGF.getGrammar(MMTGF.scala:21)
at info.kwarc.gf.GFMMT$.run(Test.scala:133)
at info.kwarc.gf.Test.main(Test.scala:100)
at info.kwarc.gf.GFMMT.main(Test.scala)[/quote]
Test.scala ist bereits angepasst:
abstract class DennisTest(prefixes : String*) extends Test(
"D:\\Documents\\__UnsyncedUni\\LBS\\MMT\\content\\",
prefixes.toList,
"",
Some(8080),
true,
Some("D:\\Documents\\__UnsyncedUni\\LBS\\mmtlog.html")
)
Ich konnte es allerdings mit folgendem Workaround in MMTGF.scala beheben:
[code=java] def getGrammar(th : DeclaredTheory) = {
val strings = th.metadata.get(key).map(.value.asInstanceOf[OMSemiFormal].toStr(true).filter(!=‘"’))
- println(strings)
- Grammar(strings:_*)
- Grammar(strings.map(path => “D:/Documents/__UnsyncedUni/LBS/MMT/content/LBS/” + path):_*)
}[/code]
Ich wäre für richtige Lösungen dankbar Ich habe noch nicht den Überblick über die MMT-Klassen, was sich wie zusammenfügt, und wüsste nicht, wo es am besten wäre, den Pfad, der ja eigentlich von DennisTest kommen sollte, vorne anzuhängen
Hmm, ich würde raten dass du slashes statt backslashes in Dateipfaden benutzen solltest - hast du mal versucht “D:\Documents\__UnsyncedUni\LBS\MMT\content\” direkt durch “D:/Documents/__UnsyncedUni/LBS/MMT/content” zu ersetzen? (Analog für “D:\Documents\__UnsyncedUni\LBS\mmtlog.html”)
Ich glaube der String wird nämlich in ne File-case-class gefüttert die slashes als trenner interpretiert… Hab aber MMT noch nie wirklich unter windows benutzt deswegen muss ich da ein bisschen raten…
Da kommt leider derselbe Fehler.
Ich denke nicht, dass es an MMT liegt, sondern an der Bridge, genauer am folgenden Codeteil aus GFScala/src/main/scala/info/kwarc/gf/Grammar.scala:
object Grammar {
def apply(filenames : String*) : Grammar = {
if (filenames.length == 1 && File(filenames.head).getExtension.contains("pgf"))
return new Grammar(PGF.readPGF(filenames.head))
Dort wird an die native Funktion PGF.readPGF aus der jpgf.dll nur der relative Dateipfad übergeben.
EDIT: Die neueste Test.scala gibt übrigens folgende Loginformation aus:
Der Pfad stimmt fast, es fehlt nur noch ein Ordner dazwischen: D:\Documents__UnsyncedUni\LBS\MMT\content\LBS\source\ Frag1 \frag1Syn.pgf.
Ah! Nein, ich hab tatsächlich einfach nur vergessen die frag1.pgf in src direkt zu committen (bei mir ist sie nämlich da) 0o
Hab das gerade nachgeholt. Sorry für die Verwirrung
Ich kann frag1.pgf unter source leider immer noch nicht finden: https://gl.mathhub.info/Teaching/LBS/tree/master/source
Tatsache… jetzt bn ich verwirrt; welche pgf file hab ich dann gegitaddet? 0o
Anyway, die Test.scala in GFScala referenziert eine Theorie die in source/three.mmt liegt, die wiederum referenziert tutorial/two.pgf, und die existiert auch und sollte genug Beispiele beinhalten für die Tableaux-Aufgabe. Insbesondere referenziert die Test.scala nichts außerhalb dessen, und die Beispiele die da gegeben sind sollten alle funktionieren.
Was ich mir bei der anderen MMT-file gedacht hab, die irgendne andere pgf referenziert versteh ich grad selber nicht mehr genau, ist aber auf jeden Fall kein Fehler in der Implementation sondern im content und könnt ihr getrost ignorieren (wenn ihr nicht andere Fehler dadurch habt?)
Die Test.scala führt beim Ausführen immer noch zu der Exception von vor zwei Posts.
Bei mir und im Online-Repo referenziert sie noch frag1log: GFScala/src/main/scala/info/kwarc/gf/Test.scala at d6edf6fbab1648c38fe5aa50c385c5610b3aee69 · UniFormal/GFScala · GitHub
Ich habe das dort mal auf [m]val gr = gf.getGrammar(MMTGF.dpath ? „three“)[/m] geändert, dann kommt in dieser Zeile aber diese Exception:
[quote]gf: http://mathhub.info/Teaching/LBS?three →
Exception in thread „main“ java.util.NoSuchElementException: head of empty list
at scala.collection.immutable.Nil$.head(List.scala:420)
at scala.collection.immutable.Nil$.head(List.scala:417)
at info.kwarc.gf.Grammar$.apply(Grammar.scala:26)
at info.kwarc.gf.MMTGF.getGrammar(MMTGF.scala:37)
at info.kwarc.gf.MMTGF.getGrammar(MMTGF.scala:44)
at info.kwarc.gf.GFMMT$.run(Test.scala:145)
at info.kwarc.gf.Test.main(Test.scala:110)
at info.kwarc.gf.GFMMT.main(Test.scala)[/quote]
In der ersten Zeile des Logs kann die URI anscheinend auch nicht aufgelöst werden, hinter dem → ist ein leerer String.
Ich würde zumindest gerne mal Test-Objekte für meinen Modelchecker haben, bevor ich ihn programmiere, damit ich ungefähr eine Ahnung habe, wie die Objekte intern strukturiert und zu pattern matchen sind.
Jupp, ich hab auch festgestellt dass der selbe Fehler jetzt auch bei mir auftaucht 0o Ich bin mir unsicher, woher das kommt bzw. warum der vorher nicht da war… ich hab mal den pfad in der .mmt angepasst und gepusht
Das mit dem Tableaux eilt ja auch nicht