> On Nov 27, 2020, at 6:28 AM, Stef O'Rear <[email protected]> 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 <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 -- 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/2CBE2334-9C61-43E0-AE10-AE7E8276D12B%40dwheeler.com.
