On Sat, Nov 28, 2020 at 4:04 AM savask <[email protected]> wrote: > I'm a bit late to the discussion, but do I understand correctly that this > new community verifier is supposed to be a spin-off to MM0/MM1 project? In > particular, MM1 code base will be the starting point, proofs won't look > like mmj2's proof sheets, and most of tactics/automation will be written in > a custom language (as I understood, MM1 uses a scheme-like language)? Also > as far as I understand this new verifier should be able to replace an > ensemble of tools we use now for CI (or is this a separate project which > will include support for ungrammatical databases?). >
That all sounds about right. To support ungrammatical databases, the CI verifier would need a standard verifier embedded in it, or alternatively we could just use another verifier for that part. It's possible to detect this condition on the fly, too. By the way, there is another possibility for tactics, which is as rust crates that get linked (statically or dynamically) into mm0-rs (or even in another language if that's your thing). This is probably a better choice for really big tactics because the scripting language, while good for on the spot ad-hoc tactics and simple pattern matching, gets somewhat unmaintainable at large scale because it's not typed and uses only s-exprs for structured data, and it's also interpreted so there is a speed penalty associated with that. > When I first read this thread, I imagined the project roughly as depicted > on Thierry's diagram (a universal core library agnostic of grammar, tactic > language etc + PA program using that lib to imitate mmj2 or imitate MM1 and > so on), but on the second reading I got the impression that the underlying > idea was to base it of MM1 from the beginning. I'm not sure if this is a > source of confusion for others, but it is definitely for me, so it would be > nice if the intended connection between MM0/MM1 and the new verifier could > be clarified. > That's fair. I wasn't intending it to be based on MM1 from the beginning, but writing a verifier from scratch is an endeavor and especially if it's mostly me leading the charge I will want to share code with mm0-rs because it is currently under active development. However the aim here is not to transition to MM0 the formal system, or at least that's not my current proposal; rather it is to adapt mm0-rs so that it can also work with metamath as the foundation instead of MM0, which requires replacing a few foundational types but not nearly as much as you might expect, because the basic structure of terms is similar to MM. David points out to me that even this is quite some work, and suggests translating to and from MM0 if the goal is simply to be able to use mm0-rs as a MM proof assistant. There is a bit more manual work involved in that, because library theorems will be somewhat mangled by the roundtrip and there are some limitations on what you can prove especially in early pred calc where non-distinct setvars play a role, but mostly I think this will work at the small scale. Probably we will want both eventually. Mario -- 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/CAFXXJSvHWuQyUJoZEw%3D7RjsVHAxiAEgXYPeYv30grqmfjdWpog%40mail.gmail.com.
