Functionality compared to "official" Mizar distribution?

[pqnelson]

trafficstars

Since the publication of the associated paper (arXiv:2304.08391), it appears quite a bit has been done. So I wanted to ask: how does this compare to the "official" Mizar distribution?

I see there are parsers, readers, and many other wonderful things. But what remains to be done before this can act as a "standalone full distribution"?

[digama0]

The main thing that is implemented at this point is a full pipeline to check the MML. In particular that means it can start from the sources only and generate the prel/ directory (with the exception of a few files which are in the prel/ directory but are actually hand-written XML input files, for the axioms). What is not supported currently are external inputs, so if you want to make modifications you need to go through the motions as though this was a new article in the MML and develop it directly in the folder.

There is also a long list of "tooling" utilities which are not implemented (e.g. generating abstract files, removing irrelevant references, generating latex, ...). For generating latex in particular, I think there are still some non-public parts involved in the pipeline, so even using https://github.com/MizarProject/system I think you can't generate pdf files which look just like the ones that are published in the JFM.

There is an extended version of the paper which documents a lot of the work which has been done, but I am not sure whether it saw the light of day. I should put it up on arxiv.

[pqnelson]

(1) So it sounds like some "low hanging fruit" might be to write some CLI programs which can replace Mizar's verifier and accom (among others)? Cool, that's good to know.

I'm just trying to figure out how I can help make the Rust version more of a clone I could just "swap in" without a hitch.

(2) For land's sake, upload the paper! If nothing else, put it in a doc/ subdirectory of this project.

[pqnelson]

Thanks for posting the revised version of the paper to the arXiv; I printed it out a couple days before the fires ravaged LA (where I live). It was a pleasant read to study while the power was out last week (or was it the week before? Whenever, it was a pleasant read).

If I am reading things correctly, it appears that the only things missing would be:

1. generating all the non-XML intermediate files, and
2. the fn main() right now is hardcoded to check the MML (as opposed to being a replacement for mizf).

That second item seems to be the only thing preventing mizar-rs from being a drop-in replacement for the "official" Mizar distribution (modulo a few helper utilities), would that be fair to say?

[digama0]

Yes, that's correct. (And I would ask why (1) should even be a goal; the main reason I can see it being useful is for the htmlizer, which makes use of some of those intermediate files. Mixing and matching components of original mizar and mizar-rs is mostly only useful for debugging purposes, I don't expect users to have such a workflow.)

For (2), I think it might make sense to have a bash script frontend that just changes the CLI interface to match mizf, accom, and verifier, since the current CLI is not directly compatible but has enough options to act like all of those tools. I had some troubles with getting the CLI right since it has so many options that it's not very easy to use at this point - you probably want to use it through some wrapper. Or perhaps the CLI could be redesigned to hide more of those functionalities away such that the defaults work better; I would hate to lose the nice help message stuff one gets from using clap to implement the rust CLI.