> On Nov 21, 2020, at 6:22 PM, Mario Carneiro <[email protected]> wrote: > If there is enough interest from others that I'm not the only one on the > project, I don't mind taking the lead here. If it incorporates common code > from mm0-rs then that will be a good excuse for me to split it off to a new > project (the MM0 monorepo is getting pretty hefty) and maybe also expose a > library (depending on whether this new verifier is literally mm0-rs under > some settings or a separate executable that just links against a library with > common code from mm0-rs).
I’m definitely interested. If there’s a way I can help, I’ll help. My math chops are nowhere near yours, but I can sling code. > Since most of my experience in this area is coming from MM1 and the mm0-rs > implementation, that would be my default answer to such questions, unless > others object. You interact through vscode or another LSP-enabled editor, > with a relatively small file (not set.mm <http://set.mm/>) containing "code" > in some TBD language that I will assume looks like MM1 :) . The server runs > in the background and provides point info and diagnostics. By typing > directives in a do block you can use it like a REPL. At the top of the file > is likely "import "set.mm <http://set.mm/>";" which says to preload set.mm > <http://set.mm/> and base the current development on it. (Perhaps it should > instead be something like "altering "set.mm <http://set.mm/>";" if the goal > of the file is to construct an alteration to set.mm <http://set.mm/> that may > involve inserting theorems in places, renaming things and other such stuff.) I think it should be like “import set.mm [[before|after] NAME]”, so you know what’s allowed & what is not. > The user can add lines to adjust set.mm <http://set.mm/> notation to their > preference, and the language can come with some presets that can be included > so that we can collect an approved set of alterations for set.mm > <http://set.mm/>. > > If you want to add a new theorem, you can declare one in the file, with a > notation like MM1's but possibly with some modifications to support DV > conditions that are not expressible in MM0 (for example if two set variables > are not necessarily disjoint). You can write a literal expression if the > proof is simple enough, or you can call a tactic, or you can pop open a > (focus) block as in MM1 to enter tactic mode where you evolve a goal state > through the use of imperative commands like applying theorems, switching > between goals, calling automation and so on. > > At the end of the day, you get a file that represents an alteration to set.mm > <http://set.mm/>, or a new .mm file. This doesn’t seem very interactive. Can this be made fast enough to provide rapid feedback so someone can see what is (or is not) working? Is there a variant that would be easily interactive? Maybe we can cache results so that “if nothing has changed here’s the answer” to make this fast? One thing I appreciate about mmj2 is its interactivity. One thing I do *not* like about mmj2 is extremely weak & inflexible automation. I’d like both interactivity & automation. --- 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/E05C0DA9-9B90-4C4A-B60A-FB8E11EA1532%40dwheeler.com.
