Faster

[benjub]

This could subsume PR #6. In addition to it (described in #4), it achieves a 3 to 4 times speedup by verifying compressed proofs directly without converting them to normal format.

Also some bug fixes (including the one mentionned in metamath/metamath-exe#81) and code documentation.

This could be used in https://github.com/metamath/set.mm/blob/develop/.github/workflows/verifiers.yml: probably no need to split set.mm into main/mathbox thanks to speedup, and also one should probably use normal arguments instead of bash redirections to avoid the bug described in metamath/metamath-exe#81.

[benjub]

Thanks @tirix. It looks like @david-a-wheeler has no time for this now. So maybe I can either modify https://github.com/metamath/set.mm/blob/develop/.github/workflows/verifiers.yml to use my fork of mmverify.py, or maybe better as you suggest, put a copy of this faster mmverify.py in a new folder, say metamath/set.mm/verifiers ? Maybe @digama0 has some advice ?

[david-a-wheeler]

@benjub - How about I give you rights to push changes to this directly? Just give others a chance to review the change first.

[david-a-wheeler]

@benjub @tirix - I agree that in the longer term this should probably move to the "Metamath" group instead. In the short term, I've added @benjub as a collaborator so merges can now happen directly.

Sorry I haven't been very available, it's quite out of my control.

[benjub]

Thanks @david-a-wheeler. As you propose, I'll merge this PR after and if this is reviewed. Maybe by @tirix or @digama0 if/when they have time.

[david-a-wheeler]

Thank you. And again, my apologies for my delays. I've had a lot of personal issues that have prevented me from giving these issues the time I want to give them.

[david-a-wheeler]

Good. I've invited @tirix and @digama0 also as collaborators. Moving this to the Metamath org might be good long-term, but this will at least get things unstuck.

[tirix]

Ok, took the time to review!
Nothing breaking for sure, just a few questions.

[tirix]

Obviously this is not from your code, but the reverse here is a bit surprising at first sight.
I assume it's more efficient to pop the last element than the first one.
A queue might be even more efficient, but there might be overhead to build it.

[benjub]

As I understand, there is no "stack" in Python, but lists can be used as stacks and pop/append happen at the end of the list (https://docs.python.org/3/tutorial/datastructures.html?highlight=stack#using-lists-as-stacks), hence the need to reverse it. It may not be worth importing Queue for that. Or maybe you had an intermediate solution in mind ?

[tirix]

Looking at it again, if we're looking for performance, I guess the most efficient would probably to use an iterator. That would be something like:

   self.tokbuf = line.split()
   return self.tokbuf.next()

and testing for the StopIteration exception.
This shall avoid reverting each line, I suppose there could be another small performance gain.

But no need to do this in this PR, though.

[tirix]

Aren't multiple $f statements for the same variable forbidden in the same scope?
In any case I think the standard, or readability, recommends that in case a floating variable is declared at several places, it shall always be with the same typecode.

[benjub]

You're right. I was trying too hard to justify the reverseds in the previous versions of the code.

(As for your second sentence, I would disagree for general mm databases. In many textbooks, it happens that, say, x denotes an element of an arbitrary group in one chapter, and then a real number in another chapter.)

[digama0]

Regardless of our opinions toward it, I'm pretty sure that the second sentence is part of the spec. From p.114:

A hypothesis is a $f or $e statement. The type declared by a $f statement for a given label is global even if the variable is not (e.g., a database may not have wff P in one local scope and class P in another).

[benjub]

@tirix : I hope this answers your remarks ?
Note that mmverify.py (old and new) allows local $v's and $f's (which to me is fine), and also local $c's (which should be changed to global $c's: I'm preparing a PR for that).

[benjub]

Regarding the latest (minor) commit: improve consistency: in floating hypotheses, the order is: first typecode, second variable, both in the database (e.g. $f set x $.) and in the internal data structure used by mmverify.py to store it.
This is opposite to the usual writing in type theory (e.g. x:set) but at least this is consistent internally, since the typecode comes first in all Metamath math expressions.

[benjub]

Note: 0999f6a introduced a bug. Investigating...

[tirix]

Looks good to me.
Interesting to know that len(saved_stmts) is less performant.

Thanks for taking my remarks into account, I'm glad I could contribute to a few percents performance improvement!

[benjub]

Interesting to know that len(saved_stmts) is less performant.

Well, it seemed a good idea since the length of that array is updated rarely compared to the number of times it is called, and the updates are only of the form "+1". The timings I did did not show significant differences (although they always gave a small advantage to my method). I'm seeing in https://stackoverflow.com/questions/699177/python-do-python-lists-keep-a-count-for-len-or-does-it-count-for-each-call that the length is actually stored (C source code: https://github.com/python/cpython/blob/2.5/Objects/listobject.c#L379). On the other hand, calling len makes a global lookup, which is expensive in Python (compared to using local variables)... All in all, is this optimization worth it ? For the moment, I leave it here.