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.
Assignment 2 (PLNQ Proof Rules in MMT)
Dear all,
as discussed in the lecture on Wednesday, we have a second homework assignment: Finish the PLNQ proof rules that we started in the lecture.
You can find the assignment here: https://kwarc.info/teaching/LBS/assignment.pdf
A list of all assignments of this course is here: https://kwarc.info/teaching/LBS/assignments.pdf
In order to do the homework, you will have to install MMT. Installation instructions are here: https://uniformal.github.io//doc/setup/
MMT should run Linux, Mac OS and Windows.
It would be great if you try to set it up already - if you have any problems feel free to post here. We can also discuss any issues with MMT (installation/usage) during the lecture on Wednesday.
One more note regarding the editor: There are two supported editors for MMT - jEdit and IntelliJ. jEdit is a light-weight editor, but not particularly great (in my opinion). Therefore we generally recommend the bigger IntelliJ IDE (though jEdit completely suffices for this course). If you decide to give IntelliJ a try you should know that you can get a student license with your university email address.
Frederik
Hi Frederik,
last week at the end of the lecture, Mathub worked perfect, but now I am having trouble with opening.
It gives an error:
Cannot start compiler: the SDK is not specified for module “MMT-content”.
Specify the SDK in the Project Structure dialog.
Can you see the problem here?
Best,
Pelin
Hi Pelin,
maybe you can use it despite the error?
Otherwise: You can go to File → Project Structure and maybe see what’s going on there. I don’t have a project SDK specified, but it works for me without a problem.
However, in the platform settings I have Java (version 1.8) listed in the SDKs.
Does any of this help you?
Best,
Frederik