tirix
commented
4 months ago Anyway this looks very interesting, so I would love to see this project developed further.
My initial commit is 3 years ago, and actually I made a previous attempt in Java using MMJ2 as a basis a few years before that. So this is a long running project I've always come back to, but I have many such projects running!
The current set.rmm file does not work with the current set.mm file. This issue arises because a few theorems used in Rumm have been renamed in set.mm over the last year. I fixed these outdated labels to renew compatibility with the latest version of set.mm. While I tested this and should compile, I'd still recommend to verify that no issues have arisen.
The fact that rumm is not time resilient is unfortunate, because one has to periodically fix deprecated theorems and apply renamings. A solution might be to integrate the set.rmm file into the set.mm repository and add a check for it. This would ensure that any renaming in set.mm would also be reflected in Rumm, though it may complicate set.mm development in the long term, so this deserves further thinking.
I believe the power of tactics lies in the ability to construct more elaborated ones on top of them. Rumm lets the user do that, but if those derived tactics become non-usable after a few months, it would make progress difficult.
Anyway this looks very interesting, so I would love to see this poject developed further.