Not logged in. · Lost password · Register

Jazzpirate
Member since Oct 2016
806 posts
Subject: 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 :D
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) ;)
Jazzpirate
Member since Oct 2016
806 posts
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 :)
Jazzpirate
Member since Oct 2016
806 posts
Für potentielle Probleme:
https://groups.google.com/forum/#!topic/gf-dev/oUpxMbEW7oM
lmr
?!
Member since Oct 2017
22 posts
+1 Jazzpirate
Zu guter letzt:
1. Pfad in der Datei {path/to/mmt/folder}/content/LBS/source/tutorial/three.mmt:
Konkret: meta ?LogicSyntax?correspondsTo `{path/to/mmt/folder}/content/LBS/source/tutorial/two.pgf ({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 {path/to/GFScalaBridge}src/main/scala/info/kwarc/gf/Test.scala Klasse "DennisTest" wie folgt anpassen:
  "/home/jazzpirate/work/mmt/content", -> "{path/to/mmt/folder}content/"
  prefixes.toList,
  "",
  Some(8080),
  true,

  Some("/path/to/logfile.html") -> Logfile target, nach belieben anpassen

3. (Nur unter Linux)
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

Genaueres dazu siehe https://groups.google.com/forum/#!topic/gf-dev/oUpxMbEW7oM

4.Testen: Rechtsklick auf Test.scala -> Run 'GFMMT'
Sollte ohne Fehler durchlaufen.
This post was edited on 2017-11-23, 16:42 by lmr.
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
433 posts
Nachdem alles von GF nun auf Windows funktioniert (Anleitung folgt), bekomme ich noch folgende Fehlermeldung beim Ausführen von Test.scala:
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)

Test.scala ist bereits angepasst:
  1. abstract class DennisTest(prefixes : String*) extends Test(
  2.  "D:\\Documents\\__UnsyncedUni\\LBS\\MMT\\content\\",
  3.   prefixes.toList,
  4.  "",
  5.   Some(8080),
  6.  true,
  7.   Some("D:\\Documents\\__UnsyncedUni\\LBS\\mmtlog.html")
  8. )

Ich konnte es allerdings mit folgendem Workaround in MMTGF.scala beheben:
  1.    def getGrammar(th : DeclaredTheory) = {
  2.      val strings = th.metadata.get(key).map(_.value.asInstanceOf[OMSemiFormal].toStr(true).filter(_!='"'))
  3. -    println(strings)
  4. -    Grammar(strings:_*)
  5. +
  6. +    Grammar(strings.map(path => "D:/Documents/__UnsyncedUni/LBS/MMT/content/LBS/" + path):_*)
  7.    }

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 ;)
Jazzpirate
Member since Oct 2016
806 posts
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...
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
433 posts
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:
  1. object Grammar {
  2.   def apply(filenames : String*) : Grammar = {
  3.     if (filenames.length == 1 && File(filenames.head).getExtension.contains("pgf"))
  4.       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:
gf: http://mathhub.info/Teaching/LBS?frag1log -> D:\Documents\__UnsyncedUni\LBS\MMT\content\LBS\source\frag1Syn.pgf
Der Pfad stimmt fast, es fehlt nur noch ein Ordner dazwischen: D:\Documents\__UnsyncedUni\LBS\MMT\content\LBS\source\ Frag1 \frag1Syn.pgf.
This post was edited on 2017-12-03, 19:17 by Marcel[Inf].
Jazzpirate
Member since Oct 2016
806 posts
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
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
433 posts
Ich kann frag1.pgf unter source leider immer noch nicht finden: https://gl.mathhub.info/Teaching/LBS/tree/master/source
Jazzpirate
Member since Oct 2016
806 posts
Tatsache... jetzt bn ich verwirrt; welche pgf file hab ich dann gegitaddet? 0o :D

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?)
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
433 posts
Die Test.scala führt beim Ausführen immer noch zu der Exception von vor zwei Posts.

Quote by Jazzpirate:
Anyway, die Test.scala in GFScala referenziert eine Theorie die in source/three.mmt liegt
Bei mir und im Online-Repo referenziert sie noch frag1log: https://github.com/UniFormal/GFScala/blob/d6edf6fbab1648c3…

Ich habe das dort mal auf val gr = gf.getGrammar(MMTGF.dpath ? "three") geändert, dann kommt in dieser Zeile aber diese Exception:
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)
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.
Jazzpirate
Member since Oct 2016
806 posts
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 ;)
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen