Hi All, I've just put the finishing touches on the mm0-rs HTML generator, which makes pages such as https://digama0.github.io/mm0/peano/thms/addass.html . As should be pretty obvious, it's based on the metamath web page display, but I would like to make it a bit more interactive, possibly involving doing more verification work directly in JS. What do people want to see from a more "live" version of the web pages? Search seems like an important one, and step folding is also an option although I don't know how to make that not annoying. Another thing that is somewhat important for MM0 is "expr-folding", where subexpressions that are used in many contiguous steps (like the proof context) are abbreviated. MM/MM0 like to work with such expressions as they can be unified in constant time, but the standard metamath proof display format makes this look very repetitive (and it is also expensive to print), suggesting that somehow the print isn't capturing "the essence of the proof" because it appears to be more repetitive than is.
Also, the web pages could benefit from some design work (I did my best but it's not my forte), and it also probably lacks some essential components like a nav bar or something like it. The current design is pleasantly minimalistic but maybe some important elements are missing, so some votes on the most pressing issues would help. Mario On Wed, Nov 25, 2020 at 11:09 AM Mario Carneiro <[email protected]> wrote: > > > On Wed, Nov 25, 2020 at 8:58 AM Glauco <[email protected]> wrote: > >> Hi Mario, >> >> here >> https://groups.google.com/g/metamath/c/raGj9fO6U2I/m/2tQseJ3CBwAJ >> you show peano.mm1 in VSCode and you write >> "The basic idea is that MM1 is a scripting language for assembling MM0 >> proofs and statements. It's untrusted, and functions as the IDE for MM0" >> >> Looking at one of your presentations I've seen you've also completely >> translated set.mm to mm0, isn't it? >> >> Would it be possible, for you, to video-record a session in which you >> proof a simple new theorem (starting from the mm0 translation of set.mm) >> ? >> > > There is actually quite some work before this becomes a really usable > workflow. The problem with the translated set.mm is that there are *no* > notations. Everything is s-expressions which makes it pretty difficult to > read. > > Most of my MM0 work has been inside peano.mm1, which is a set.mm style > axiomatization of peano arithmetic with all the niceties that MM0 brings to > bear. It wouldn't be so hard to demo a new theorem there as there is a > pretty decent library of supporting theorems. Alternatively, I could use > set.mm0, which is a kind of half baked hand translation of the set.mm > axioms into MM0, including notations. I never finished the proof of set.mm1 > because I needed a library of basic logic, but I could probably port the > peano.mm1 library at this point (since the first part of peano.mm1, on > basic logic, would be the same as set.mm). > > More long term solutions for supporting set.mm would include > auto-translating most notations into MM0 style, identifying the > constructions that need some new notation, and making some hard decisions > for those. MM0 has the requirement that every notation uses a distinct > initial constant (or for infix notations, the first constant after the > initial variable should be distinctive), which means that a lot of mixfix > notations from set.mm like F : A --> B are probably not going to survive. > > >> No audio is needed, and there's no need to make the video available on >> youtube to everybody. Just a short session to show us how it would be the >> workflow: >> load available axioms/definitions/terms/theorems > create new theorem> >> write/verify proof > save created proof (add to the pre-existing "stuff") >> > > Especially if you mean the end to end MM workflow, a lot of this is still > very much a dream/plan/roadmap and not a current reality. What I can show > you now with mm0-rs is the use of MM1 to construct a .mmb binary proof file > that can be verified by external MM0 verifiers like mm0-c. I can probably > declare a few notations and do the same thing starting from set.mm.mm0, but > the result will still be an MM0 proof, not an MM proof. That's what the > plan is all about. > > 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/CAFXXJSvqnBXGQSTJWQbHn1XKx%3Deg0ZTdo_dPC6SrVwYs283KLw%40mail.gmail.com.
