Regarding slapping an UI/Ide over Metamath/MM0 The current format of set.mm doesn't prevent slapping an UI on metamath (you can just parse the whole file and throw away what you don't want) But, for sure, some things can be done (or have already been done and I'm just not aware of them) to make the process easier
There are a few ongoing attemps to do so mmpp (Giovanni) mm0, mm1 and the visual studio plugin (Mario) mmj2 metamath solitaire ? metamath programm ? ... a few other that I don't know about I'm also going at it too with Mephistolus (closed source, free to use without crap forever, but sadly only available for me at this point (I'm working to make it usefull and available)) I have a different take on the subject as most ui/ide want the user to write a source and a destination metamath statement and fill the gaps automatically (unification), with some hints Basically, the software has to compute the way to go from source to target (it is really hard, with a lot of combinatorial computations) It requires a lot of mathematical skills as you have to be able to write where you want to end up In Mephistolus, the user starts from some metamath statement and slowly modifies it with theorems/operations (associativity, commutativity, computation reduction, tacticts...) to reach a goal Basically, the human gives the directions and the computer does all it can to avoid him the hassle of proving trivial/not too hard stuff It doesn't require math skills as it could be as simple as clicking (or touching) a part of an equation, and then selecting the desired change, in a window that appears (the computer computes all possible results available on applying an operation on this part of the statement) I believe that it solves what fl has spoken of : with the right UI, Mephistolus would make a 12 years old able to use metamath powered maths Now, slapping a GOOD UI over Metamath is not as easy as it sounds : The coding a screen with drag and drop, touch/gestures support, windows is quite doable in a few weeks. But what happens when you click a button, or drag something isn't. The UI has to apply transformations on the metamath statements and execute some proof steps and this is what is really hard : you might have a shiny UI but you still have to make it do metamath magic. So the backend library is what really important. If you don't have one, it is useless to start coding an UI (which is why I haven't even tryied to do it yet, I'm focusing on the math api first) Other point to consider would be, on what platform do you want your metamath UI ? Android phones/tablet/ios phone/tablets,windows/mac/linux/unix/native code/the jvm/the web (browser ?) Mephistolus is aiming at all those targets BUT it needs all it's components to be available for those targets metamath core library : available (it only requires strings/trees) parsing metamath statements : soon (or already) available as there is a work in progress to make mutli-platform kotlin be a target for antlr : https://github.com/ftomassetti/antlr-kotlin database/indexing : ouch, here it hurts. Be it graph database (JanusGraph) or indexing libraries (lucene), none of them are available on all platforms, the one I know work on the java virtual machine (JVM) which means taht they are available on the JVM/android but I'm waiting for them to be ported to kotlin (I expect, at one point in time, that all usefull libraries will be ported to kotlin). OR alternative would have to be plugged and maintained for all targets UI : ouch,it hurts here too : be it Jetpack Compose/Flutter/JavaFx there is no single UI Library available for all targets (waiting for something good, in this space too) Regarding metamath for metamath experts, something can already be done today (you just need the jvm target, and everything needed is already there today) In the next months, I'll try to completely prove in metamaths all Mephistolus that I have been using to this day (I have done most of the work already, but now I'm starting to encounter harder stuff (fsumshift ^^)). Which will make mephistolus usefull for Metamath experts as it will be able to export to metamath all proofs done in mephistolus And I'll release a raw programm (just text input, no fancy UI) that will enable you to do usefull work in metamath with it It remains to be seen if you'll like the metamath proofs it produces (you want short, right :) ). But who knows, what value Mephistolus could bring you ? (I have hopes but I don't know before I try :) ) So, still working on backend stuff for the next months/years before coding an UI. :) Le jeudi 31 octobre 2019 18:38:28 UTC+1, ookami a écrit : > > Now that Christmas is approaching, I would love to come up with my personal > wish list, that I slowly gathered over the past years. Okay, I am not > going to > command others here to fulfil my needs. But maybe, one or the other point > has > been silently pondered by others as well. So lets see whether this > results in a > discussion, or even, finally, something more. > > 1. The user interface > > It is common practice nowadays to separate the UI from the so called > backend. > The backend is responsible for carrying out commands issued by the user. > The > UI should present the user with an overview of his/her options, and perhaps > allow focussing on particular fields of interest. > > Why do you want to have these separated? There are people fantastic at > creating > intuitive interfaces. Others are more into abstract thinking, and can > provide > fast and reliable libraries. Or incorporate third-party software like > search > engines. > > The current structure of set.mm has UI elements (in form of htmldef > entries), > theorem signatures (i.e hypotheses and statement), and proofs in one single > document, which I consider not optimal. > > Here's an existing example, where a separation has been successfully > carried out: > chess! See http://www.playwitharena.de/ for a screen shot of an UI. To > really play > a game you still need an engine like https://stockfishchess.org/. Both UI > and > engine are exchangeable. > > If we want to go into this direction, we need to standardize the interface > between > frontend and backend. And before we can do that, we need to get an > overview of > what capabilities are requested by the users -- that are you! > > 2. Proof templates > > At least in the area where I have worked so far, I more than once > encountered a > situation, where I needed a specific instance out of a theorem family, that > wasn't provided. The usual action to get around this deficiency was by > looking out for a nearby solution and introduce otherwise unnecessary > administrative proof steps. A good example is the > deduction/immediate/closed form > of a theorem. Wouldn't it be nice to have these forms at hand without > much ado? > > Apart from this convenience aspect, I would really love to extend parts of > FOL to > arbitrary dimensions, as applies to substitution [ z / x ] [ w / y ]... , > for example. > The current Metamath language has no means of expressing a proof concept, > or template, > that contains instructions how to create a proof for a concrete theorem > instance. > I really miss such an abstraction layer. > > There are some pitfalls here to note: One should keep a compiled form of a > theorem > database, where all these abstract notions are collapsed into instances as > needed, > instead of interpreting them over and over again. C++ is an example of a > computer > language that follows this idea. The executable is stripped of any helper > constructs > the programer might have employed in his working process. > > Anyway, is there an idea of how to create a meta language/grammar that > fits into this > field? > > 3. Specialization > > The gource video from DAW shows in how many different fields of mathematics > set.mm has put its foot into. These are only the traditional fields, > others might > want to use ZFC in future to create abstract graph structures like trees, > maps. I am > pretty sure, there is much more than that conceivable. > > For me it is time to break set.mm up into dedicated subunits. Creating a > complete > HTML site of all theorems is already a matter of an hour or so on my > computer. > Should't there be some support of specialization? Don't get me wrong > here. I think > this is difficult, as it needs some sort of linking process, with all > kinds of > conflicts lurking (link against classic or intuitionistic logic? Use > theorem A or > B out of different units, one using the axiom of choice, the other not?). > > I would love to hear from you how you see the future here. > > Kind regards > > Wolf > -- 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/e0ab1fc5-d076-42eb-b067-92604eb2e1c6%40googlegroups.com.
