Here are my main goals for Mephistolus Milestone 7 :
1) build a pure kotlin metamath antlr parser and build a Mephistolus App with the Kotlin/Js target, so that we can use it in a browser (that way, it would be easier for you to test it) 2) improve the UI and the user workflow, a) save and load a proof (this requires choosing a serialization format for representing the proof state) b) filter/order/fix the action menu to make it fun/great to use c) fold previous steps to concentrate on the last step d) experiment with a custom user variable name -> mephistolus var name, to completely hide internal mephistolus names e) research : Method (or tactic ?) groups : the user should be able to say : I want to prove an induction, or I want to prove an <-> through 2 x -> and then Mephistolus should display places where the user would prove sub-aim and let Mephistolus write the annoying and repetitive glue to get the final statement 3) research enhancements to the back-end a) when doing an index change, you should just give the translation : use explicit mephistolus theorem instead of implicit ones, to remove the need for the user to input too many substitutions for example, instead of using this "sum_ ∨1s e. ( ∨2c ... ∨3c ) ∨4c = sum_ ∨5s e. ( ( ∨2c + ∨6c ) ... ( ∨3c + ∨6c ) ) ∨7c", "∨2c e. ZZ", "∨3c e. ZZ", "∨6c e. ZZ", "( ∨1s e. ( ∨2c ... ∨3c ) -> ∨4c e. CC )", "( ∨1s = ( ∨5s - ∨6c ) -> ∨4c = ∨7c )" I should probably use something like : "sum_ ∨1s e. ( ∨2c ... ∨3c ) ∨4c = sum_ ∨1s e. ( ( ∨2c + ∨5c ) ... ( ∨3c + ∨5c ) ) [ ∨1s - ∨5c / ∨1s ] ∨4c", That way, Mephistolus only has to ask for v5c and then, let it reduce the [ ∨1s - ∨5c / ∨1s ] ∨4c part, it is good at that b) research unification, from infered parts and rthe result of substitution hypotheses for example, an hypothesis like ( ∨1s = ∨4s -> ∨3c = ∨5c ) should allow us to infer from v1s, v4s and v3c what v5c should be c) out of the 30000+ metamath theorem, migrate all those who can to mephistolus theorems 4) fix bugs 5) Mm0 a) get a file for set.mm0 (set.mm translated to mm0) Mario, I'm looking at you... b) parse set.mm0 c) extract a list of all mm0 ids d) write a parser for mm0 statements e) make the mephistolus Statement able to be build on mm0 stuff Well, that should keep me busy and happy for the next months. Le mercredi 22 janvier 2020 11:18:40 UTC+1, Oliv ier Binda a écrit : > > > Il 22/01/20 11:00, OlivierBinda ha scritto: > > Obviously, making the action menu resizable and dragable was a big > mistake : next time, it'll be anchored at the right side of the window > and will resize automatically automatically > > Yes, it's quite clear that the action menu is still rather awkward to > use. And, to be honest, I don't think it is easy to find the right way > to lay it down. It seems to be quite a UX challenge. > > Yes, I'll try my best (and take advices) > > Also, in the next release, I am planning to filter/order display in a > better way the actions in this menu (because it is a mess at the moment). > It is very hard to do so(it requires human smarts), but I'll probably be > able to do a decent job (with computer smarts). > > Another thing I noticed is that the variable name that you write are > different from those that appear in the pretty printed formula. For > example, you write "v1c" and "X" appears in the formula. This is quite > counterintuitive, I believe. > > Yes, you are right about that > Internally, Mephistolus uses names like v2s, v8c, v3w > for setvar, classvar and wffvar > > > But as It is aimed at the general public, my goal is to allow people to > use the variable names they like > x, k,n or it might be stuff like 平 or ひ , etc... > > At the moment, I am able to display custom variable names. > But I haven't implemented yet, the translation process to convert a user > variable name like x, to the right variable set/class/wff type > > I still have to figure out how to do it. I'll probably try first to infer > if it should be a wff var or not, > go with class var by default and fallback to setvar if it is necessary. > > Hopefully, that will work out nicely (or I'll have to think further about > it :) ) > > > ps : sorry for the double mail, I'll probably get it soon ^^ > > -- 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/d43d5049-b64e-4f8c-afaf-46cddcdae3bb%40googlegroups.com.
