> On Nov 22, 2020, at 5:35 PM, Mario Carneiro <[email protected]> wrote: > > 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;
In practice that doesn’t seem to be a problem. People tend to pay attention to spacing, after all, (g ab) is already different than (g a b) :-). Yes, it’s not the identical circumstance, but in my experience this mistake is uncommon in practice. I did some sampling of large swathes of Lisp code years ago, and it turns out that typing (f g(a b)) to mean (f g (a b)) is essentially non-existent in real code bases. I think most people see (f g(a b) c) as “ugly” even though most S-expression readers would quietly accept it. Since people don’t normally use that format, let’s give that format a more useful meaning :-). > and (2) it doesn't mesh well with the @ syntax for cutting down parens. My sweet-expressions notation implements those using Haskell’s “$” notation. E.g.: f $ g a ; Same as (f ( g a )) That isn’t part of the neoteric-expression definition, but the contstructs do work well together. > 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. Fair enough. But since I devised a system for exactly this kind of circumstance, it’d be useful to at least consider it as a possibility. > (Also, there is a precedence issue in (f ,g(a) b), does that mean (f (,g a) > b) or (f ,(g a) b)?) Details like that are defined in its SRFI. I’ll switch to ‘ to make its simpler to see: (f ‘g(a) b) <=> (f ‘(g a) b) If you want just g to be quoted, the obvious way is traditional S-expressions: (f (‘g a) b) > 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. In practice it’ll be a 2-way street. As long as we focus on trying to create an externally-callable library, many other things can be worked over time. > Your average set.mm <http://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. YES. I like that *MUCH* better. I’m sold. > ... > 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. Wow, that’s MUCH faster than I was expecting. However, I want to implement mechanisms that automate proofs that may take much much longer. That said, it should be trivial to cache that information somewhere (e.g., filename.mmcache) so that the calculation only has to be redone when its inputs change & the cached answer won’t work. > 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. Sounds reasonable, though I think the “bulk verifier” (smm3) should be accessible separately (e.g., for CI pipelines like ours). In addition, I’d like the tool to be as thin veneer as reasonably possible, with practically everything important in the callable library. That way anyone can just import the library from any language & have it “ready to go”. --- 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/06DE0E47-59BB-4E24-B8E7-182ABE2273AE%40dwheeler.com.
