On Sun, Nov 22, 2020 at 5:00 PM David A. Wheeler <[email protected]> wrote:
> > > On Nov 21, 2020, at 10:15 PM, Mario Carneiro <[email protected]> wrote: > > > > On Sat, Nov 21, 2020 at 8:42 PM David A. Wheeler <[email protected]> > wrote: > >> Providing a Scheme-like interface is a reasonable approach. It’s easy to >> implement & provides a lot of flexibility. The big problem is that MANY >> people hate their syntax, e.g., “lots of irritating silly parentheses”. As >> you know, I think it’d be *much* better if it supported neoteric syntax (at >> least), so that you can use syntax like f(5) and {2 + 3}, as that >> eliminates the main complaint about Lisps while retaining all their >> benefits. >> > > I'm inclined not to spend much time on this complaint. Better to spend > some time with it, get a sense for the way things are put together, and > *then* propose improvements. Alternate syntax is not out of the question > but it needs to fit within the other design constraints of the language. In > particular, MM1 is in many ways an MVP for a metamath based proof > assistant, enough to help me prove my big theorems and not much more. If > this is to become some big flagship product then I don't mind investing > more to make it convenient, but only after the more pressing problems are > dealt with. > > > This is something I can easily do. I’ve implemented neoteric expressions > in Scheme, Common Lisp, and Java. It turns out to be very short, *AND* > they’re totally optional for use. That is, you can always say (foo bar bar) > if you prefer it over foo(bar baz). > In MM1, I think it wouldn't be so great, because (1) it's way too easy to misspell (f g (a b) c) as (f g(a b) c), particularly when typing quickly; and (2) it doesn't mesh well with the @ syntax for cutting down parens. I call it scheme-like but it's sufficiently different that it is its own language with its own idioms, which is why I emphasize that you should try using it before proposing changes. (Also, there is a precedence issue in (f ,g(a) b), does that mean (f (,g a) b) or (f ,(g a) b)?) I actually meant something more like switching to a completely different not lispy syntax. Maybe haskelly? Since not all of the language is lispy, it is useful to see at a glance where the "code" is and where the math expressions are in a visually distinctive way. I think this needs to be a separate discussion though; this is really a v2 problem. To be fair, some SMT solvers *do* have proof producing mechanisms (e.g., > CVC4 and Z3). For comparisons, see: > http://homepage.divms.uiowa.edu/~viswanathn/qual.pdf > Aye, they have proof producing mechanisms, but the proof format has no spec, are unstandardized, and can't really be checked externally. My colleague Seul Baek has been working on an alternative: http://paar2020.gforge.inria.fr/papers/PAAR_2020_paper_17.pdf Careful consideration is important, agreed. But I think we want to make > sure that a lot of things are (eventually) accessible by a library call. If > the library can be imported from (say) Python & JavaScript, and the library > is eventually rich, then a whole lot of re-implementation does *not* need > to happen. > Of course we want to avoid reimplementation of core components as much as possible. My plan is to wait for the dependent program to start existing, and then use its requirements to help determine what needs to be public. On Sun, Nov 22, 2020 at 5:11 PM David A. Wheeler <[email protected]> wrote: > 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. > Great, I was worried it was all mathematicians and no coders in here. When building a proof assistant it's important to have a balance of both types of users. > 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) 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";" which says to preload set.mm and base the current > development on it. (Perhaps it should instead be something like "altering " > set.mm";" if the goal of the file is to construct an alteration to 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. > Your average set.mm modification, especially a maintenance change, may touch many theorems in many places. So I wouldn't want to require that they all fit in some contiguous block. Perhaps (before/after NAME) can be a freestanding command to change the context, or it can be a modifier on the theorem command to affect where an individual theorem goes. > The user can add lines to adjust 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. > > 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, 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? > It's quite interactive. The script is executed continuously every time you type a character in the editor, so you don't have to press a command or anything to make it go. Peano.mm1 is starting to have noticeable slowdown (maybe .7 seconds) but it's already 6500 lines and almost 2000 theorems, and you can always speed it up by moving a prefix of the file to another file. (I'm planning to support more checkpointing within a file so that it's fast even if you are editing in the middle, but currently it just reads and executes the whole file.) I think that's more than fast enough for the average metamath proof. Honestly it's an order of magnitude faster than mmj2. On Sun, Nov 22, 2020 at 5:25 PM David A. Wheeler <[email protected]> wrote: > 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. > Yes, that's the "CI verifier" that started this discussion. I find it easier for maintenance purposes to support all the modes in one tool, using subcommands in the command line like "mm0-rs server" and "mm0-rs compile foo.mm1", although you can compile out the tools separately if one of them requires more dependencies or has too much code in it. 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/CAFXXJSv7%3DMP5hVSE3BgZkJqjUo-9NN9WBMoaajYYDq3sNY6Hvw%40mail.gmail.com.
