Grammar

[tirix]

This PR brings in the "grammar" changes discussed with Mario on the thread "community verifier". It also includes a mechanism for parsing parser commands.

This includes/builds on top of the changes in the Outline PR #8 , so it shall be merged afterwards.

[david-a-wheeler]

This looks awesome! This is also a huge change, so I'm going to post to the metamath mailing list to hear any last-minute comments before i merge it. I expect I'll merge it.

[tirix]

Sure! Mario @digama0 was concerned about two things:

• the grammar could have been implemented as a KLR(5) grammar, like for MMJ2. This would have avoided the need for the "parser hints". This change is a bigger undertaking, likely of the same complexity as this PR. I'd like to go ahead with this version, improvements can still be made later on, keeping the same API.
• these $j parser commands could have been implemented with an enum with two values, to make the difference between the parser command name, and the arguments. I did not make the difference and implemented them all using the MM parser's Token, which is a lightweight pointer to the source. That change would be easier to implement.

[digama0]

what's the reason for the subset.mm file? I haven't looked at it (too big for github) but it seems like it should be in a test or examples directory if it is testing some mm features.

[digama0]

I'm okay with merging this early and revising it later if we come up with something better. More docs would be good though, in addition to the style issues already mentioned. We should strive for 100% doc comments on public items, and I think it would be a good idea to do this for private items too, at least in the algorithm-heavy areas. (I use #![warn(missing_docs)] at the top level, which is good at enforcing this principle.)

[tirix]

what's the reason for the subset.mm file?

It's indeed a subset of set.mm I used for testing, I don't think it brings anything beyond parsing the full set.mm, so I'll delete it. I also believe we shall add test files in a test or examples directory.

[tirix]

I'm okay with merging this early and revising it later if we come up with something better.

Thanks, and thank you for the review!

More docs would be good though, in addition to the style issues already mentioned. We should strive for 100% doc comments on public items, and I think it would be a good idea to do this for private items too, at least in the algorithm-heavy areas. (I use #![warn(missing_docs)] at the top level, which is good at enforcing this principle.)

I agree. I already have comments on several private items, but I'm feeling like the crate/lib docs shall only contain the API documentation. I thought about adding explanation for the parsing algorithm in a separated /doc directory. What's your opinion?

[digama0]

I agree. I already have comments on several private items, but I'm feeling like the crate/lib docs shall only contain the API documentation. I thought about adding explanation for the parsing algorithm in a separated /doc directory. What's your opinion?

I think that it's fine to add explanation of the algorithm in the public docs, for example in the module doc comment. Certainly it's fine to put such information on private or crate local declarations, which are not shown in rustdoc unless you specifically ask for them (but will still appear in hovers et al). I'm not a fan of completely separate documentation in a doc/ folder, especially for something like an implementation description that might go out of date if someone touches the grammar.rs file. (Separate documentation is better for things like a user manual, where the order of presentation doesn't have much to do with the code layout.)

[david-a-wheeler]

@digama0 - thanks so much for your thorough review!

@tirix said:

the grammar could have been implemented as a KLR(5) grammar, like for MMJ2. This would have avoided the need for the "parser hints". This change is a bigger undertaking, likely of the same complexity as this PR. I'd like to go ahead with this version, improvements can still be made later on, keeping the same API.

@digama0 said:

I'm okay with merging this early and revising it later if we come up with something better.

That all makes sense to me. I'm hoping that one of you will be willing to make that change eventually too :-). But improvements are improvements, and this looks like an overall big improvement to me.

@tirix - let me know when you're finished with the fixes you're going to make in this PR. Once you're done I think we should merge!

[david-a-wheeler]

@tirix @digama0 - I just added you to the set of people authorized to make changes directly. @tirix - merge this PR at your convenience.

My main request is please propose changes via pull requests, so others can comment (just as has been done here). I suspect we'll eventually move this to the metamath repo, but no need to wait for that step.

[tirix]

@david-a-wheeler it seems the Ubuntu 16 test never starts. Do you have any idea why? This made both last runs fail.

[david-a-wheeler]

I've forced a re-run of the tests. The problem isn't that Ubuntu 16 is failing, it seems to not even be starting. Ubuntu 16 is relatively old, it's possible that GitHub is not supporting it well. If we can't get it restarted, we should probably just drop it.

[david-a-wheeler]

Ubuntu 16 will be removed September 20, 2021, from GitHub Actions. That hasn't happened yet, but is about to, so there's not much incentive to keep using Ubuntu 16. It's old anyway.

I think we should just remove Ubuntu 16 from the list of test environments. Any other opinions?

[david-a-wheeler]

Let's ignore the Ubuntu 16 results. I'll create a separate change to remove Ubuntu 16.

[david-a-wheeler]

Removing Ubuntu 16 is done here: https://github.com/david-a-wheeler/metamath-knife/pull/12

[david-a-wheeler]

Other than Ubuntu 16 failing, which we should ignore, is all good for merging?

[david-a-wheeler]

@tirix - merge when you think it's ready!

[tirix]

Thanks a lot! The checks are now passing, so I'd like to merge and continue with format and clippy in another PR, but I don't have write access, so I cannot merge myself. Please go ahead!

[digama0]

This PR still has the 2018 stuff in it. Can you split that off in a separate PR (that this one depends on) and make sure this one only has diff changes from the grammar addition?

[tirix]

Can you split the 2018 stuff off in a separate PR ?

Sure, I did this is PR #13 .

[david-a-wheeler]

@tirix - #13 switches to 2018, but so does this one. Sounds like you want to merge #13 first, then this one (#9). Is that correct?

[tirix]

Sounds like you want to merge #13 first, then this one (#9). Is that correct?

Yes, exactly! This is what I understood Mario wanted to do. Once #13 will be merged, this one shall only show the additions for the grammar, and nothing else.

[david-a-wheeler]

@tirix - I've merged #13 . We now have some merge conflicts. Can you fix the conflicts so we can merge this?

Also: Where practical, I suggest making commits with a smaller number of changes in the future (as compared to their parent commit). That reduces the likelihood of merge conflicts, smaller changes are easier to review, and if only some parts work out it's easy to cherry-pick. I don't know if that's possible for this grammar change, as that's wider-reaching, but I thought I should mention it.

[tirix]

@digama0 If you'd like to further split this big PR into more smaller parts, we could split out:

• the parsing of the $j additional information comments,
• some changes I did in this branch on the "Outline" part (like changing indentation, and making the result an Arc)

This would further reduce the scope of this PR. @david-a-wheeler if we do split this further, then we shall wait a bit longer until those smaller PR are merged before we merge this PR.

[digama0]

some changes I did in this branch on the "Outline" part (like changing indentation, and making the result an Arc)

This should definitely be in a different PR if it's not related. Hopefully that is easy to do?

the parsing of the $j additional information comments,

I don't mind this being in the same PR since it is related to the grammar addition, but if you think it is clearer and you are up to the task then splitting it up is also good.

@david-a-wheeler By the way, I personally prefer to always use the squash-and-merge option because it leads to a cleaner (linear) history (which is easier to do e.g. rebases with in git), with each commit being tied to a PR (with the associated discussion), and also PR authors don't need to worry too much about commit messages for "internal" commits and can focus the documentation in either the first commit on the branch or the PR description.

[david-a-wheeler]

@digama0 : Squash & merge eliminates some history though. I'm familiar with it & do it sometimes, but if the history isn't too complicated I like to let the history be real. This one is getting complex though.

@tirix : If it's easy to split up the changes, great, let's do that. If it's too complex, let's merge together. In the future it'd be better to have separate changes in separate commits... but I'd rather have improvements in any form than worry about that.

[tirix]

If it's easy to split up the changes, great, let's do that.

I've isolated those changes in #14 , we can first merge #14, then this PR.

[digama0]

@digama0 : Squash & merge eliminates some history though. I'm familiar with it & do it sometimes, but if the history isn't too complicated I like to let the history be real. This one is getting complex though.

The history isn't lost, the commit-by-commit breakdown is still available on the PR page, and the sequence of commit messages is preserved in the merged commit message if you don't do anything. For complex PRs like this one, I think squashing is even more important, because they clarify what things are actually supposed to be changed as opposed to iterative fixes and patches interspersed with half baked feature additions. The blow by blow is useful during the PR process because it allows reviewers to see what changed since the last review of the PR, but when everything is done it is mostly uninformative, especially if care is taken to separate out the actual distinct features into separate PRs (i.e. moving the outline and rust 2018 parts out of this PR).

[david-a-wheeler]

14 is merged, let's merge this one soon.

@digama0 - it's true that the GitHub PR records the past, but that's only around as long as GitHub exists & shares that data. GitHub is currently going strong & I don't see them disappearing soon, but the list of websites that were dominant at one time & then disappeared is very long (geocities, megaupload, MySpace, etc.). Assuming external sites will live forever is risky. Git can record history & its data is easily transferred. I'll leave it to @tirix if he thinks it's useful to merge this sequence of commits into a single change or not.

@tirix - I definitely want this merged in. Would you like to squash it into a single change, or would it be useful to record the blow-by-blow?

[digama0]

@digama0 - it's true that the GitHub PR records the past, but that's only around as long as GitHub exists & shares that data. GitHub is currently going strong & I don't see them disappearing soon, but the list of websites that were dominant at one time & then disappeared is very long (geocities, megaupload, MySpace, etc.). Assuming external sites will live forever is risky.

I'm not assuming that github will live forever, but rather that all github data is relevant, including comments, issues and PRs, and if we ever needed to migrate away from it we would need to collect all of this data, not just the git repo itself. In any case I don't think it's worth planning for such an eventuality at the cost of the current developer experience.

[tirix]

It looks like there are pro's and con's for squashing, in general I think I would prefer keeping all commits separated, but I guess it's a matter of taste about what you would like the commit history to look like.

This is a case of relevant development, which spawned over several months for me. Of course at the intermediate commits there was only limited or partial functionality. I don't think I committed too often: there is often one, at most a handful of commits a day.

I believe in the future, the best way for such a development would be to open a feature branch on the main repository, so that anyone can try it out and/or contribute, and to have a running open PR where the changes are visible.

In any case I can squash the commits for this PR if this the preferred way!

[david-a-wheeler]

@tirix - I agree, there are pros & cons. If you think the history has no value, squash, otherwise merge the whole collection. Merge once you think think branch is ready, and you choose if it should be squashed or not!

What's most important is that your improvements get added :-).

I agree that it's best to have many separate feature branches. That way, if one turns out to not work, it's easy to simply drop it & add the rest. Sometimes that isn't practical, but that's a good default.