search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 10 forks source link

grammar refactor: use one map #31

Closed digama0 closed 2 years ago

digama0 commented 2 years ago

I'm not sure whether this is better or worse than the current approach. During refactoring I found a lot more hashmap iterations than I expected, and iteration over just the constants or just the variables is worse in this implementation than with two maps. On the other hand, it decreases the memory footprint of each node in half, and there is less internal fragmentation in the maps. @tirix, could you test this to make sure it still works and performs alright?

This builds on #30, but I can rebase it if we want to separate these PRs.

digama0 commented 2 years ago

Ah, oops these reviews / edits should have probably gone on the other PR. Are you also okay with the "grammar refactor" commit, which is the point of this PR?

tirix commented 2 years ago

Yes! Everything looks good to me.

I must say I don't see a clear improvement in runtime, I suspect I shall have kept statistics to notice it, but space saving and simplicity are both great wins.

david-a-wheeler commented 2 years ago

Simplicity is always welcome!

I copied the version number as part of the fork. I think it'd be more confusing to make the version number go backwards. Let's improve it so it earns its number :-).

digama0 commented 2 years ago

Another option that I am okay with is to just ignore semver for the time being. But I don't think that "making the version number go backwards" is a huge problem at this point, since no one is using mm-knife yet. The smetamath-rs project is stable on version 3 or so, but this is a separate project which has its own path of evolution, and I think the best solution is to just have an unrelated version number. If you like we can do like java and change the version to 0.3 and work from there, but it's better to do it sooner rather than later, in order to minimize the problems associated with going back on the versioning.

(Assuming you haven't seen it, read https://semver.org/ . It is quite clear about what version numbers mean, and 3.0.0 is only appropriate for a project that has a stable user base or otherwise has strong backward compatibility guarantees. We can bump the major version on API changes, but we will very quickly end up at version 15.0.0 that way.)

tirix commented 2 years ago

I'd be fine with 0.3.x.

Stefan's SMM was on crate.io with version 3.0.0. I think David and I bumped the version when doing changes.

As for API users, I've been using metamath-knife with a few toy projects. One of them I called rumm and is an attempt at a proof assistant with tactics. Right now I'm still pointing to metamath-knife with a relative path, but a crate would be nice.