Congrats, a new verifier is always a good news!
And Typescript is a very relevant language.
Interestingly enough, Raph Levien (& al)'s Python verifier
has the exact same "trick" with reversing
the token buffer, then popping from it. This had me wonder.
What's the current running time?
In any case I would suggest adding it to our set.mm CI!
_
Thierry
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BD5uC0tesStx%2Bj-bJe1Zmw4bkx1pqG-puoHpAWosX7k0Q%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/af9b7cfc-19eb-fbd1-65a6-10494e7e6dd4%40gmx.net.
> Congrats, a new verifier is always a good news!
Thanks! :-)
> What's the current running time?
It should be respectable. It's verifying set.mm for me in about eight seconds on the MacBook Pro I'm using. Unfortunately XCode is currently broken on said device so I'm unable to build other verifiers in order to provide a fair comparison, other than to make the obvious statement that this is not, and never will be, a competitor for metamath-knife.
Mario's suggestion could potentially shave off maybe a couple of seconds from that, but I won't know until I try.
Best regards,
Antony
Eight seconds is respectable, we should try to add this new
verifier to our set.mm CI.
Mario's suggestion is actually the way metamath-knife works: this
avoids both to allocate and to copy each token. However,
Typescript seems to create a new String every time even a
substring or a slice is taken, so if you want to get this kind of
speedup in TS, you'd probably need to use shared
array buffers, which `slice` method, I believe, does not
copy. That structure shall also allow use in multi-threading,
which is another way to get speedup.
_
Thierry
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BBeKYGRpg9S__TUKb9f6B0u97EpTaDut55VCKDtCApF5Q%40mail.gmail.com.
Eight seconds is respectable, we should try to add this new verifier to our set.mm CI.
Mario's suggestion is actually the way metamath-knife works: this avoids both to allocate and to copy each token. However, Typescript seems to create a new String every time even a substring or a slice is taken, so if you want to get this kind of speedup in TS, you'd probably need to use shared array buffers, which `slice` method, I believe, does not copy. That structure shall also allow use in multi-threading, which is another way to get speedup.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4770daf0-39e2-a32f-f04e-34e8a6d9a2fb%40gmx.net.
On Mon, May 16, 2022 at 7:41 PM Mario Carneiro <di....@gmail.com> wrote:The pop/reverse does seem unnecessary. I would just keep track of the position in the array, possibly using a little structure containing the array and the current position with some functions to get the current token and move to the next. In fact, you can use this interface to parse the next token on demand, so that you don't need to precalculate the array of tokens (which involves millions of tiny allocations); you just hold on to the input string and pull off tokens as you need.
On 17/05/2022 16:16, Antony Bartlett wrote:
It's verifying set.mm for me in about eight seconds on the MacBook Pro I'm using. [...]
Mario's suggestion could potentially shave off maybe a couple of seconds from that, but I won't know until I try.
On Monday, August 29, 2022 at 9:07:53 PM UTC+2 David A. Wheeler wrote:Let me know of any objections to adding it to our test suite.