Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)?

[David A. Wheeler]

Stefan O’Rear: Are you still around? Are you still maintaining the Metamath verifier smetamath-rs (smm3) written in Rust at <https://github.com/sorear/smetamath-rs>? Your verifier is amazingly fast, but it hasn’t been updated in a while & there are various things that need updating. I’d also like to add some small additions to its functionality (e.g., perhaps a C interface & definition checker).

In general I try to work with the original developer of a project & acknowledge them as lead. However, if they’ve abandoned the project, then I’ll fork the project & carry on. I sent an email earlier & didn’t hear anything, so I though posting to this mailing list might be the best next step. This will also help everyone else know that I’m interested in this.

--- David A. Wheeler

[Stef O'Rear]

On Wed, Nov 25, 2020 at 5:43 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> Stefan O’Rear: Are you still around?

You privately emailed me 60 hours before sending this list message, on
a major US holiday, on an email address I largely no longer use (my
current address can be found in any of my up-to-date github repos).

While I appreciate the enthusiasm, I ask for the tiniest bit of
patience here. (In my current jurisdiction, presumption of death
requires absence "for a continuous period of 5 years" which is "not
satisfactorily explained after diligent search or inquiry".)

> Are you still maintaining the Metamath verifier smetamath-rs (smm3) written in Rust at <https://github.com/sorear/smetamath-rs>? Your verifier is amazingly fast, but it hasn’t been updated in a while & there are various things that need updating. I’d also like to add some small additions to its functionality (e.g., perhaps a C interface & definition checker).

There ought to be nothing to update. Rust 1.0 and Metamath both
promised eternal forward compatibility.

Both smetamaths were designed around a DOM that could be expanded into
a proof assistant. A definition checker and a UI were intended
functions that I never completed.

> In general I try to work with the original developer of a project & acknowledge them as lead. However, if they’ve abandoned the project, then I’ll fork the project & carry on. I sent an email earlier & didn’t hear anything, so I though posting to this mailing list might be the best next step. This will also help everyone else know that I’m interested in this.

I would like to know more about the scope of your plans and am
potentially interested in joining, depending on time availability.

> --- David A. Wheeler

-s

[David A. Wheeler]

On Nov 27, 2020, at 6:28 AM, Stef O'Rear <sor...@gmail.com> wrote:

Are you still maintaining the Metamath verifier smetamath-rs (smm3) written in Rust at <https://github.com/sorear/smetamath-rs>? Your verifier is amazingly fast, but it hasn’t been updated in a while & there are various things that need updating. I’d also like to add some small additions to its functionality (e.g., perhaps a C interface & definition checker).

There ought to be nothing to update.  Rust 1.0 and Metamath both
promised eternal forward compatibility.

There are a *LOT* of warnings, which is concerning for a program intended to be trusted. For example it uses the deprecated try!(...) instead of the current ? operation. Switching to “?” does not change the functionality and it simplifies the source code. I had thought try!() wasn’t even mentioned in the Rust book; I went back and found that try! *is* briefly discussed, but it’s also explaining why using “?” Is recommended instead: https://doc.rust-lang.org/edition-guide/rust-2018/error-handling-and-panics/the-question-mark-operator-for-easier-error-handling.html

I think it’s wise to eliminate warnings where you can (as long as you verify that the change isn’t a regression). That increases the likelihood of detecting real problems. Yes, there was an Debian OpenSSL debacle, but that involved crypto key randomness which is notoriously hard to test. This code *should* be deterministic :-).

In addition, I think there are a number of little tweaks that could speed it further; clippy is finding a number of things that can be done more simply, and I doubt the compiler optimizes them all.

Both smetamaths were designed around a DOM that could be expanded into
a proof assistant.  A definition checker and a UI were intended
functions that I never completed.

I as thinking about adding a C/WASM interface & definition checker.

--- David A. Wheeler

[David A. Wheeler]

On Nov 27, 2020, at 11:47 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

Are you still maintaining the Metamath verifier smetamath-rs (smm3) written in Rust at <https://github.com/sorear/smetamath-rs>? Your verifier is amazingly fast, but it hasn’t been updated in a while & there are various things that need updating. I’d also like to add some small additions to its functionality (e.g., perhaps a C interface & definition checker).

On Nov 27, 2020, at 6:28 AM, Stef O'Rear <sor...@gmail.com> wrote:

There ought to be nothing to update.  Rust 1.0 and Metamath both
promised eternal forward compatibility.

Stephan O'Rear:
On re-reading your comments, it sounds like you don’t want smm3 to be significantly changed, instead depending on forward compatibility promises so it can be left basically as-is, with perhaps a few small changes. You have also (on GitHub) indicated disinterest in adding a CI pipeline.

And that’s perfectly fine! You have every right to do that on your project!!

However, I have a different aim. I’m interested in having an expanded Metamath verifier & related functionality in Rust, starting with eliminating all warnings & deprecations, along with adding a CI pipeline. I think that’s the first step. Then I want to make a number of changes to significantly expand its capabilities. For example, I want to add a bunch of C-level APIs & WASM support so that other languages can call its internals. I also want to get moving quickly & make a number of changes.

If our aims differ, as they appear to, then I think it makes more sense for me to create a “friendly fork” soon and start making changes on it. I will of course use a *different* name to prevent confusion. (Any suggestions? “metamathr” is one option.) I’ll make changes in small commits, and of course use the same license for my additions, so you can cherry-pick whatever you like.

Of course, I may have misunderstood you, let me know if so. Thanks!

--- David A. Wheeler

[ML]

On Sunday, November 29, 2020 at 2:40:48 PM UTC-5 David A. Wheeler wrote:

I will of course use a *different* name to prevent confusion. (Any suggestions? “metamathr” is one option.)

I suggest calling it "Rumm" :)

[Stef O'Rear]

On Sun, Nov 29, 2020 at 2:40 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
>
>
> On Nov 27, 2020, at 11:47 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> Are you still maintaining the Metamath verifier smetamath-rs (smm3) written in Rust at <https://github.com/sorear/smetamath-rs>? Your verifier is amazingly fast, but it hasn’t been updated in a while & there are various things that need updating. I’d also like to add some small additions to its functionality (e.g., perhaps a C interface & definition checker).
>
>
>
> On Nov 27, 2020, at 6:28 AM, Stef O'Rear <sor...@gmail.com> wrote:
> There ought to be nothing to update. Rust 1.0 and Metamath both
> promised eternal forward compatibility.
>
>
>
> Stephan O'Rear:
> On re-reading your comments, it sounds like you don’t want smm3 to be significantly changed, instead depending on forward compatibility promises so it can be left basically as-is, with perhaps a few small changes. You have also (on GitHub) indicated disinterest in adding a CI pipeline.

There are definitely things I'd like to add (definition checking,
better grammar support, support for other environments, integrate with
a proof checking UI).

I do not want to see churn for churn's sake - if the code is going to
change, there need to be real bugfixes or feature improvements.

When we've had a chance to talk about a roadmap, incremental changes
are fine; but that hasn't happened yet.

My preferred model for testing is for programs to have test suites
that are quick, not very resource intensive, and can be run by
contributors prior to pushing changes. CI has a real maintenance cost
for the project (I'm old enough to remember half a dozen CI-for-FOSS
services be announced, widely adopted, and discontinued); I am also
very much not a fan of the modern approach of "push untested whatever
to master, wait for the build to fail, revert it later". Procedurally
speaking, I wouldn't mind setting up something with a CI-gated merge
like homu, but I'm dreading having to migrate it repeatedly to
different services.

This is a difficult period for me for various unrelated reasons. I
would like to continue to be involved, but I cannot guarantee
responses to everything within a day.

> And that’s perfectly fine! You have every right to do that on your project!!
>
> However, I have a different aim. I’m interested in having an expanded Metamath verifier & related functionality in Rust, starting with eliminating all warnings & deprecations, along with adding a CI pipeline

Neither of these benefit users in isolation. It may make sense as a
"first step" but I can't accept such a thing without a deeper view of
the roadmap.

> I think that’s the first step. Then I want to make a number of changes to significantly expand its capabilities. For example, I want to add a bunch of C-level APIs & WASM support so that other languages can call its internals. I also want to get moving quickly & make a number of changes.

+1 on WASM

>
> If our aims differ, as they appear to, then I think it makes more sense for me to create a “friendly fork” soon and start making changes on it. I will of course use a *different* name to prevent confusion. (Any suggestions? “metamathr” is one option.) I’ll make changes in small commits, and of course use the same license for my additions, so you can cherry-pick whatever you like.

I don't think our aims greatly differ; just our time availability and
versioning philosophy. So I kind of want to keep this as more of a
https://github.com/rust-lang/llvm-project situation.

It might help to set up a dedicated channel for this; the metamath
list is busy lately and I am many months behind reading everything.
It's not obvious what actually needs my input, and for the things that
are for me, it's hard to tell what the priority needs to be.

Thank you!

-s

> Of course, I may have misunderstood you, let me know if so. Thanks!
>
> --- David A. Wheeler
>

> --
> 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/3AFC3493-B5ED-43D1-BA50-ECD574EED0AA%40dwheeler.com.

[David A. Wheeler]

On Sun, Nov 29, 2020 at 2:40 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

Stephan O'Rear:
On re-reading your comments, it sounds like you don’t want smm3 to be significantly changed, instead depending on forward compatibility promises so it can be left basically as-is, with perhaps a few small changes. You have also (on GitHub) indicated disinterest in adding a CI pipeline.

On Dec 6, 2020, at 1:11 PM, Stef O'Rear <sor...@gmail.com> wrote:

There are definitely things I'd like to add (definition checking,
better grammar support, support for other environments, integrate with
a proof checking UI).

I do not want to see churn for churn's sake - if the code is going to
change, there need to be real bugfixes or feature improvements.

I agree. But we have a disagreement on what “real” bug fixes are.

For example, I think a compilation shouldn’t be producing warnings in normal circumstances.

When we've had a chance to talk about a roadmap, incremental changes
are fine; but that hasn't happened yet.

Starting roadmap is listed above. Fix the many warnings, add more tests, add CI,

add definition checker, C API, probably WASM.

My preferred model for testing is for programs to have test suites
that are quick, not very resource intensive, and can be run by
contributors prior to pushing changes.  CI has a real maintenance cost
for the project (I'm old enough to remember half a dozen CI-for-FOSS
services be announced, widely adopted, and discontinued); I am also
very much not a fan of the modern approach of "push untested whatever
to master, wait for the build to fail, revert it later".  Procedurally
speaking, I wouldn't mind setting up something with a CI-gated merge
like homu, but I'm dreading having to migrate it repeatedly to
different services.

Lack of CI also has a maintenance cost: the risk of unnoticed errors.

For example, without CI the tests only check for a single environment.

My CI tests on multiple platforms including Ubuntu 16, 18, 20, Windows, and MacOS.

In theory it doesn’t matter, but theory sometimes differs from practice.

I agree with you that “revert it later” is not great, but typically what happens

In projects is that the branches get changes, and only get merged after they pass the tests.

You can even enforce that with a config option on GitHub.

However, I have a different aim. I’m interested in having an expanded Metamath verifier & related functionality in Rust, starting with eliminating all warnings & deprecations, along with adding a CI pipeline

Neither of these benefit users in isolation.  It may make sense as a
"first step" but I can't accept such a thing without a deeper view of
the roadmap.

To me that’s the necessary first step. I’m not even going to *attempt* adding a definition checker until I eliminate warnings, add more tests, address the many Clippy warnings, and so on. I want to have confidence that the resulting code works.

For example, the current code uses the deprecated “try!” macro. Current Rust compiler & documentation urge use of the easier “?” construct, and I expect “try!” to stop being supported (“try” is becoming a keyword with different semantics). Using a construct that is going to be eliminated is *very* user-visible, especially once it stops compiling :-). I want the code to compile on recent versions of Rust compilers; newer compilers tend to produce faster code.

The current code does a lot of unnecessary clone() calls, hurting performance. I think performance *does* benefit users.

I think that’s the first step. Then I want to make a number of changes to significantly expand its capabilities. For example, I want to add a bunch of C-level APIs & WASM support so that other languages can call its internals. I also want to get moving quickly & make a number of changes.

+1 on WASM

If our aims differ, as they appear to, then I think it makes more sense for me to create a “friendly fork” soon and start making changes on it. I will of course use a *different* name to prevent confusion. (Any suggestions? “metamathr” is one option.) I’ll make changes in small commits, and of course use the same license for my additions, so you can cherry-pick whatever you like.

I completely understand. For the next week I’m going to be overwhelmed (I teach 2 graduate classes), but after that I hope to spend some time on this & on doing more with Mario’s tool suite.

I don't think our aims greatly differ; just our time availability and
versioning philosophy.  So I kind of want to keep this as more of a
https://github.com/rust-lang/llvm-project situation.

It might help to set up a dedicated channel for this; the metamath
list is busy lately and I am many months behind reading everything.
It's not obvious what actually needs my input, and for the things that
are for me, it's hard to tell what the priority needs to be.

I think our aims don’t differ, but our tactics appear to. I’m very big on static & dynamic testing. I’m confident that humans make mistakes, so I put automated systems in place to maximally detect problems, and make sure they’re always run so that people don’t need to remember to do it.

I’ve just started creating my friendly fork, here:

  https://github.com/david-a-wheeler/metamath-knife

It currently fixes a bunch of warnings & adds some added proof format support.

I might set up a dedicated channel later, it’s not a bad idea. For the moment, specific comments to the issues, general Metamath discussions here.

--- David A. Wheeler

[Mario Carneiro]

On Tue, Dec 8, 2020 at 10:51 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

For example, the current code uses the deprecated “try!” macro. Current Rust compiler & documentation urge use of the easier “?” construct, and I expect “try!” to stop being supported (“try” is becoming a keyword with different semantics). Using a construct that is going to be eliminated is *very* user-visible, especially once it stops compiling :-). I want the code to compile on recent versions of Rust compilers; newer compilers tend to produce faster code.

Just for reference, the way rust works, it won't ever stop compiling, but it is instead tied to an "edition", probably the 2015 edition for this code, and upgrading the edition is the only time deprecated features can be turned into errors or repurposed. The reason for this design is exactly so that you don't have this bargain to make: you can keep upgrading the compiler, get faster code, but signal that you want 2015 semantics by setting the edition, and try! will keep working as is.

Mario