Materials and Software for the Practical Part

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.

Materials and Software for the Practical Part
Roughly every second lecture will focus on practical aspects of representing mathematical knowledge in a formal system developed in our group, namely the MMT system.

We will follow a tutorial given at https://gl.mathhub.info/Tutorials/Mathematicians
That file also includes installation instructions for MMT.

This week it is possible but not necessary yet to install MMT on your computers. But we recommend you install it by next week.

Michael & Florian


We will use https://gl.mathhub.info/Tutorials/KRMT to store the examples written in the lab.

1 „Gefällt mir“

MMT Installation
Hi,
I once used the official MMT installation guide to condense everything needed for the installation in 10 steps. Maybe it can help: https://github.com/zolekode/mmt
Disclaimer: Although this guide was already reviewed by a member of the KWARC Group, I would still highly recommend using the official guide in case there is a doubt or problem.

MMT-content folder is empty
I tried installing MMT with jEdit as described in https://gl.mathhub.info/Tutorials/Mathematicians/-/blob/master/tutorial/mmt-math-tutorial.pdf.
However, my MMT-content folder is empty. Is there any option to get the content so I can copy it into the directory?


@Anouk: I’d recommend switching to the IntelliJ IDE with the MMT plugin. With the MMT IntelliJ plugin you can install archives. For that choose ‘MathHub’ in the project pane – iirc – and right-click any archive you like (e.g. MathHub → MMT → urtheories) to run ‘install’.

Alternatively, with either IntelliJ or jEdit, you can just git-clone some existing MMT archive into there. For example, you can start with MMT/urtheories:

  1. create the folder hierarchy content/MathHub/MMT
  2. run [m]cd content/MathHub/MMT && git clone https://gl.mathhub.info/MMT/urtheories[/m]

(NB: you don’t really need the folder hierarchy from step 1, but I like to follow this approach since I have often need multiple MMT archives from different sources.

NB 2: I like to not only git-clone but have those repos as Git submodules as it allows to bind my current work git repo to the necessary versions of the archives.)


@Marcel: Thanks for your answer!
But I just realized that I had overseen a failure with the cloning of the git repository. I fixed it and now it works.


Hey, I said that upgrading the IntelliJ plugin should be as easy as [m]s/2019/2020[/m] because I do remember doing that in the past for another plugin. Well I tried it and to be honest I failed upgrading the MMT plugin, I guess it’s a bit more complicated than I expected.

Maybe I’ll look into it again, but maybe someone more into IntellIJ plugin development is around.


Yes, most likely because of Bump allowed version number after testing with IDEA 2020 · Issue #31 · UniFormal/IntelliJ-MMT · GitHub, i.e. the plugin’s metadata just states „I am only usable in < v20“. I made a PR there and asked the primary maintainer kindly to make another release.


@kissen A new version of the MMT plugin has been published by Dennis: https://plugins.jetbrains.com/plugin/11450-mmt. You should be able to simply update the MMT plugin from within IntelliJ IDEA.

Refactored example files
As announced in the lecture I have refactored the files.

I have also added a readme file that gives an overview of the files and their dependency order.