search

digama0 / mizar-rs

Alternative Mizar proof checker (http://mizar.org/) written in Rust
GNU General Public License v3.0
47 stars 4 forks source link

Old MML #1

Closed vvs- closed 1 year ago

vvs- commented 1 year ago

Hi,

Are you aware of the fact that there is newer MML? I found it yesterday. Look here: http://mizar.uwb.edu.pl/~softadm/pub/system/i386-win32/mizar-8.1.12_5.73.1435-i386-win32.exe

BTW, Windows version seems to be always newer that that for Linux. And yes, their website is a mess :)

digama0 commented 1 year ago

The version is pinned for reproducibility purposes (I'm gearing up for a frozen version for a paper). Once that settles down it would make most sense to just compile it from source, now that the sources are online.

Besides this, there isn't much advantage to using a newer MML unless it fixes the bugs I have reported to the development team (that's why I'm using a patch). Hopefully the patch still applies to 5.73, I haven't tested it, but I'm guessing the patch is still needed. We can look into making the MML input configurable, but it should just amount to downloading your own version on the side and symlinking miz/ to it.

Ultimately, this is a checker which is supposed to be largely agnostic to the MML version. The only time it should need to be updated is when the checker version (8.1.12 here) changes, since that is essentially a language change.