> On Sun, Nov 29, 2020 at 2:40 PM David A. Wheeler <[email protected] > <mailto:[email protected]>> 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 <[email protected]> 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 > <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 -- 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/445552A6-56D8-4966-AB38-A0D91B79668D%40dwheeler.com.
