smglom: Einige Fehler bis hin zu reals.mmt

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.

smglom: Einige Fehler bis hin zu reals.mmt
Ich habe das smglom Archiv soeben heruntergeladen und einige Dateien enthalten Fehler laut MMT. Ist der smglom/master Branch WIP oder liegt das an meinem System?
Zum Beispiel functional-analysis/norms.mmt und arithmetics/reals.mmt: [siehe Anhang]. Auch calculus/derivatives.mmt enthält Fehler.

Insbesondere gibt es da eine Warnung mit “free variables remained: NAT”. Wahrscheinlich hängen fast alle Theorien von NAT ab?

Mein System:

  • Java 1.8.0_181 64-bit.
  • Frische jEdit und MMT-Installation von vor paar Tagen + “lmh install MitM/smglom”.
  • Reproduzierbar sowohl auf zwei Windows-Rechnern als auch in Lubuntu-VM.

(@Jazzpirate: Ich wollte morgen sowieso wieder im Arbeitsraum vorbeischauen :))

Attachment:
mmt-errors.png: https://fsi.cs.fau.de/unb-attachments/post_157775/mmt-errors.png


Jupp, da ist der zustand inkonsistent aus… gründen. Da werd ich mich mit dem nächsten release drum kümmern, weil da auch noch ein paar andere sachen aufgeräumt werden müssen

1 „Gefällt mir“