On Fri, Nov 20, 2020 at 10:22 PM Raph Levien <[email protected]> wrote:
> Regarding writing an editor. I agree it's a big task and hard to do right. > That said, it's also something I'm interested in. I know there's at least > one other editor project on Druid (not my own), and we also have interest > in unbundling our (Druid's) multiline text widget so it's possible to > integrate other functionality on top of it. > Yes, I'm aware of the Xi editor and my comment wasn't at all meant to throw shade on it! I think it's a cool project, and from the demos I've seen it looks pretty slick, if a bit raw (I don't know how much it has progressed in the meantime). But I'm sure you can attest that it's not a job for the faint-hearted! Of course if the *goal* is to build a good text editor then it's a feasible project, but building a good text editor and also a good proof assistant at the same time is probably a poor separation of concerns. If you want help on specifically the Druid parts, you might be able to come > by the #druid channel on xi.zulipchat.com and stir up some interest. > > Raph > > > On Fri, Nov 20, 2020 at 2:31 PM vvs <[email protected]> wrote: > >> Whoa! And I'm already spoiled by what Leo is doing with Lean 4. The so >> small core language and vastly extensible parser with an entire automation >> library for building and proving formal systems using incremental >> compilation with plans for interactive compiler guidance are mind blowing. >> That's taking aside your own exciting MM0 work. And I only have that much >> time to learn about lots of things. I'm torn already :( >> >> -- >> 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/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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/CADBEgNPr7K5F10F0A8OVjk%2BFvdaZL6w5Q4o5KzTZB%2B4oaVaCOQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CADBEgNPr7K5F10F0A8OVjk%2BFvdaZL6w5Q4o5KzTZB%2B4oaVaCOQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJStuC5-yQe-Wz4JAo0oNar0s241_su0bt8i7ViC2ybOAXg%40mail.gmail.com.
