> On Nov 27, 2020, at 11:47 AM, David A. Wheeler <[email protected]> wrote: >>> Are you still maintaining the Metamath verifier smetamath-rs (smm3) written >>> in Rust at <https://github.com/sorear/smetamath-rs >>> <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 <[email protected] >> <mailto:[email protected]>> 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 -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3AFC3493-B5ED-43D1-BA50-ECD574EED0AA%40dwheeler.com.
