> On Nov 22, 2020, at 8:58 AM, Thierry Arnoux <[email protected]> wrote: > > Hi all, > > This all sounds very interesting! > > From the different posts, here is a possible breakdown I see:
In principle I think that’s right, at least in the sense that there would be multiple crates, each one focused on different tasks & building up on others. There will probably be changes in the details as we flesh it out. I think that, for speed, there will probably need to be a separate crate for “bulk verification of a file’s contents”. This is a role performed by smm3. There are optimization tricks for a bulk verifier, and we verify whole files often enough that it makes sense to do that. Also, I think a PA may only accept grammatical databases, while the bulk verifier might be designed to handle non-grammatical ones too. I’d like to see smm3 modified so that it’s easily called as a library, with parameters/hooks so that it can do “bulk verification” of in-memory long strings. But I expect that wouldn’t be too hard to do. --- 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/50018122-CB9B-4E33-A0F1-AE4AB1EF368C%40dwheeler.com.
