Manpage

[benjub]

First two commits: minor edits in the manpage and README.txt
Third commit: add bib words "criterion" and "criteria"; fixes #96 (which stemmed from a real-world case, not merely a theoretical one, see there).

[wlammen]

I am at a loss to decide whether the addition of CRITERI* is a necessity, or a nice to have, or just noise. This should be done by those writing a bibliography on a more regular base. From a technical point of view, I think, one should have a closer look at

1. the comment in line 5217 should be updated to include mmhlpa.c;
2. the keywords here seem to be mostly in alphabetic order, except for the first 5 entries, that are used frequently enough to play an outstanding role in a not further specified search operation. CLAIM, for example, appears only three times in mmbiblio.html. I don't see a compelling reason to have it far up in the list, in comparison to the freshly added items.

[benjub]

I have to cite Criterion of [BourbakiTop1] p. I.2 in https://us.metamath.org/mpeuni/ishmeo.html (as a temporary solution, I used "Proposition"). Since the irregular plurals are aslo added in this list (e.g., scolion/scolia), I also added "criteria".
Do you prefer to put the list in alphabetical order ?

[benjub]

1. the comment in line 5217 should be updated to include mmhlpa.c;

I don't understand this. Line 5217 of which file ? mmhlpa.c has been updated (see its Line 1133).

[wlammen]

It is line 5274 ff (I got it wrong, don't know why), and it reads
/* **IMPORTANT** Make sure to update mmhlpb.c HELP WRITE BIBLIOGRAPHY if new items are added to this list. */
Here the wrong file is mentioned.

[wlammen]

Do you prefer to put the list in alphabetical order ?

I don't see a good reason to deviate from it without necessity. Since the list is duplicated (in a different form, but essentially the items correspond to each other), you can better check the correctness with the aid of some ordering, keeping the exemptions at a minimum.

[benjub]

@wlammen : done. (I don't understand the necessity of if( 0 || ...) instead of if (...) on Line 5276.)

Added: the necessity to add a keyword at two places (mmwtex.c and mmhlpa.c) shows an opportunity for code refactoring, for instance having as global variable the array of keywords.

[wlammen]

This list is searched sequentially. Matching an item at the beginning is obviously way more efficient (1 comparison) than one at the end (40 comparisons). So if you know, the keyword in str2 is 'theorem' 70% of the time, it makes some sense, to have it at the beginning. This is the gist of the deleted comment here. I think, the first 5 elements of the old list were deliberately put in the early position for speed up. The tail starting with 'AXIOM' are matched fairly seldom, so their exact position does not really matter, and we can keep an alphabetic order there, without compromising speed to a noticeable degree.

What do I personally think of it? Well, if search time really matters, than there are better strategies around, like binary search, for example. This is a poor man's optimization. It may have an improving effect, though, depending on how often a search is called. Without knowing details, I would keep the first five elements, but order the tail.

The 0 in the beginning of the list is likely optimized out and just there to keep all items, including the first, in the same textual format.

[wlammen]

From a technical point of view, I do not object to this PR any more, unless you see a slow down due to the impoverished search.
Maybe one should add a
// ---- end of optimized search -----
in between head and tail of the list, for better understanding.

[benjub]

I do not know C well enough, so I rely on you here. What order do you prefer ? Is the following ok (including comments) ?

           /* **IMPORTANT** Make sure to update mmhlpa.c HELP WRITE BIBLIOGRAPHY
              if new items are added to this list. */
           if (0
              /* The first five keywords are more frequent so are put first for
                  efficiency; the rest is in alphabetical order. */
              || !strcmp(mid(str2, k, (long)strlen("THEOREM")), "THEOREM")
              || !strcmp(mid(str2, k, (long)strlen("EQUATION")), "EQUATION")
              || !strcmp(mid(str2, k, (long)strlen("DEFINITION")), "DEFINITION")
              || !strcmp(mid(str2, k, (long)strlen("LEMMA")), "LEMMA")
              || !strcmp(mid(str2, k, (long)strlen("EXERCISE")), "EXERCISE")
              // ---- end of optimized search -----
              ... [alphabetical]

?

[wlammen]

This is fine

[benjub]

Thanks. That's the content of my latest commit. So I guess you can approve. (On this repository, I have no right to approve or merge --- and am not asking for one.)

[wlammen]

I have no right to merge either

[david-a-wheeler]

I think I have the great cosmic power to merge :-). I don't have any objections to this. However, I want to make sure there's been time for anyone to object.

The "big" change is allowing "criterion" and "criteria" as names of things to reference, that makes sense. We'll need to modify the documentation elsewhere, e.g., in set.mm.

@digama0 - any issues?

[benjub]

We'll need to modify the documentation elsewhere, e.g., in set.mm.

Good catch. I will. But in order to pass the CI process, we need to have this PR merged, then make a new version 0.199 (with a few other PRs that could be merged), and then make the CI test (the .yml) use that version.

[benjub]

@digama0 - any issues?

To paraphrase @david-a-wheeler : is it good with you @digama0 ?

[david-a-wheeler]

I'll merge if we don't hear any objections in the next day or two. Please remind me to do so!

[benjub]

@david-a-wheeler: I guess you can merge !

[david-a-wheeler]

@benjub - okay, merging!

(Standing waaaay back :-) ).

[david-a-wheeler]

I've merged it. We probably need to have a discussion about how to merge metamath-exe code changes. I think "someone else reviews" is a good start. We might want to give a little time before merging, so that people can object. I hope that makes sense.

[jkingdon]

I've merged it. We probably need to have a discussion about how to merge metamath-exe code changes. I think "someone else reviews" is a good start. We might want to give a little time before merging, so that people can object. I hope that makes sense.

What we currently say is:

We especially encourage discussion and, perhaps, letting a bit of time pass before merging, if a change seems large or risky (given the general philosophy described in the "Maintenance mode" section above).

(excerpt from https://github.com/metamath/metamath-exe/blob/master/CONTRIBUTING.md - see also the rest of that file). Of course anything there can be revisited, but I think it probably bears some resemblence to the consensus as of when we switched from Norm's maintainership to community maintainership.

[david-a-wheeler]

I agree. I think we should leave a little extra time for non-trivial code changes, to give more time for objections, because unlike the .mm databases we can't prove it's correct :-). But yes, let's continue to have proposals posted, & wait for a second "yes" along with time to allow for objections.

[benjub]

The information in the quoted CONTRIBUTING.md file looks sensible. On the other hand, the more PRs are stalling in the queue (currently, five), the more likely the merge conflicts.

On a minor note, I had to use the incorrect reference Proposition of [BourbakiTop1] p. I.2 in https://us.metamath.org/mpeuni/ishmeo.html instead of Criterion of [BourbakiTop1] p. I.2 so that it pass the CI check, which uses the current metamath-0.198. This was at the origin of the current PR. When a 0.199 is released, I'll fix that.

[jkingdon]

because unlike the .mm databases we can't prove it's correct :-).

If we had a bigger testsuite and more static and/or automated tests using valgrind or similar, we could get a bit closer than where we are today. But I doubt we'll be using proofs of correctness on metamath-exe (or, perhaps, any of our tools) any time soon.

[jkingdon]

On the other hand, the more PRs are stalling in the queue (currently, five), the more likely the merge conflicts.

I'm thinking (some?) (all?) should be closed as "won't merge, see Maintenance Mode". But saying Maintenance Mode in the abstract is easier than rejecting a particular pull request in the concrete, and I also don't know whether my impulse on that topic matches other people's.

[benjub]

As for the current PRs, I unfortunately do not know enough C yet to tell what should be done with them. I think that at least @wlammen's PR #86 should eventually be merged.

In general, using a program in maintenance mode in a CI check can have some unwanted consequences: what is being checked cannot itself evolve as one would wish. One can of course have finer control by looking what parts of the program are used in the CI checks and what parts of the program have to remain in maintenance mode.

As for adding new functionalities in metamath.c, that probably should not be a priority. But when this is clearly separate from the verifier part of metamath.c, it should not compromise the latter, and I would be pretty glad to have the hypotheses and DV usage qualifiers of #92.

[digama0]

Just a quick comment: I don't have a lot of time to work on metamath these days, but I do try to review stuff that goes in to metamath-exe, especially functional changes in the C code. Just ping me if there is a PR that needs my attention.

[jkingdon]

As for the current PRs, I unfortunately do not know enough C yet to tell what should be done with them. I think that at least @wlammen's PR #86 should eventually be merged.

Yeah, good point, that one clearly seems like the kind of fix which ideally would get the kind of review (and presumably merging) that apparently hasn't happened yet.

In general, using a program in maintenance mode in a CI check can have some unwanted consequences: what is being checked cannot itself evolve as one would wish.

It isn't supposed to be that deep of a freeze. In the words of CONTRIBUTING, 'We aren't making a rigid "never change metamath-exe" rule but we are saying that we expect such changes will be primarily to tweak parts of metamath-exe which are getting in our way, more so than expand what it can do.'

As for adding new functionalities in metamath.c, that probably should not be a priority. But when this is clearly separate from the verifier part of metamath.c, it should not compromise the latter

Because C has no memory protection, there is no guarantee of this. There are also other considerations like:

• how do I declare a particular piece of code as being part of the verifier or not?
• when reviewing a pull request, how do I know whether it touches the verifier?
• is our code well enough modularized that we can put a lot of things in this repo without hitting a wall on overall complexity?
• given that we have so many verifier implementations, is the verifier even the part to worry about the most?

, and I would be pretty glad to have the hypotheses and DV usage qualifiers of #92.

That is definitely in the class of things where I was asking myself "but can't this be a separate tool?" I mean, there might be reasons why we don't make it separate (depending on how hard of a line we want to draw, the implementation difficulty of various choices, etc). Same applies to a few of the others but for the most part we haven't had explicit discussions on it (at least, not on a per-pull-request basis).