*>the .mm parser is REALLY fast.* *>Does it also do validation?* *>How is it implemented? Server side? Javascript? Webassembly?*
Thanks Glauco. Yes, the parser validates syntax and some other rules like no duplications of labels, a symbol declared as a constant cannot be redeclared as a variable, expressions must begin with a constant, and so on. If you try to load an invalid mm file you'll probably get an error message. I cannot state that I implemented all the possible validations but I tried to do as much as I could following the Metamath book. If you mean validation of proofs, then no, the parser doesn't validate proofs. However, there is a function to validate proofs, but it is used only in tests to check if a proof generated by the proof assistant is successfully verified by the standard verification algorithm. Parsing is implemented in a very straightforward way. Entire mm file content gets stored in a string variable. Then I use local int variables to store indexes of some important parts like last char read, begin and end of current token, etc. The main idea is to make necessary decisions and checks using only indexes and then "substring" only required parts of mm file content (labels, math symbols etc.) , and do not "substring" what is not actually required. I think Mario also mentioned similar approach in one thread with discussion of performance of proof verifiers. Everything runs in a browser. This proof assistant doesn't have server side. It runs only in JavaScript. To be honest I am also impressed how fast it parses. I think, besides that approach with indexes, modern JS engines make very good optimizations. Also I don't exclude that ReScript compiler when generating JS code may do some optimizations. But I have not analyzed generated JS code, so I cannot say much on that. You also may notice that the proof assistant runs in two threads in a browser, but this is done not for performance. One thread is actually doing some task and another renders UI. This is done to make UI responsive when executing long running tasks and also to have ability to terminate such tasks if they become too long. Here are some references to parser and proof verifier implementations: Parser, which builds AST (abstract syntax tree) - https://github.com/expln/metamath-proof-assistant/blob/32d904911228f69a716a4f328a525acfd4e31d9b/src/metamath/mm-utils/MM_parser.res#L44 (parseMmFile function in MM_parser.res). Parser, second part (well, actually not parser, but it does further processing after building AST) - https://github.com/expln/metamath-proof-assistant/blob/32d904911228f69a716a4f328a525acfd4e31d9b/src/metamath/mm-utils/MM_context.res#L1004 (loadContext function in MM_context.res). Proof verifier - https://github.com/expln/metamath-proof-assistant/blob/32d904911228f69a716a4f328a525acfd4e31d9b/src/metamath/mm-utils/MM_proof_verifier.res#L255 (verifyProof function in MM_proof_verifier.res) Thanks David and Jim for useful ideas. I have what to reply to each suggestion/idea, but unfortunately I don't have enough time to do this in this email. I will partly reply here, and I will reply for remaining part in my next email. *>As I said, I'd delay #1 (that is likely to be *hard* unless you really back off on your plans).* *>I will say that even modest improvements here would be helpful* I would agree with Jim that some hints from the program explaining why something doesn't work as expected would be helpful. Moreover, this is one of the most interesting parts to implement for me :) I have an idea what I can try to do. In few words, I will try to create a dialog similar to proving bottom-up with different parameters. For example don't verify disjoins, verify disjoints but skip this ones, and so on. So a user can switch them on and off to find out when unification stops working. Also I may try to record everything interesting what happens during unification and then present this info to a user in some readable format so the user should be able to find the place when things don't go the way he/she wants. I also will check if I can detect particular cases and notify a user about them as Jim suggested. In general, I will not stop implementing other useful things, but I cannot delay working on that part with hints for users because this is very interesting for me :) *>One broad suggestion: Could you give it a short & less generic name,* *since there are other Metamath proof assistants?* Sure. I will come up with some short name. And also I will shortly move it to another URL - https://expln.github.io/... *>Regarding user improvements, most people will want to load the current set.mm <http://set.mm/> & iset.mm <http://iset.mm/>,>so making that easier would be helpful. If there was an easy way to download it straight>from the web, that might make getting started easier. I could easily configure>us.metamath.org <http://us.metamath.org/>'s CORS settings so the script could always download .mm files from us.metamath.org <http://us.metamath.org/>>no matter where it started from.* That's a good idea. I saw in another thread you've already configured CORS. Thanks for that. I will implement loading of set.mm and iset.mm from us.metamath.org I will reply to the remaining items a bit later :) Thanks for the feedback and new ideas! Best regards, Igor On Saturday, February 11, 2023 at 6:46:09 PM UTC+1 [email protected] wrote: > On 2/11/23 07:39, David A. Wheeler wrote: > > > 1) I think one of the "key" missing things is ability to help a user > > to understand why a statement doesn't unify. > > I have only an approximate idea of whether this is easy or hard, but I > will say that even modest improvements here would be helpful. For > example, it may be easier to detect particular cases than every possible > "way" a statement can't unify. One of the more time consuming things > that happens to me when using mmj2 is that a unification which I > expected to happen doesn't, and then I need to look at (sometimes long) > expressions to figure out what parts don't match. > > > -- 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/d5307998-5ab2-44b8-b6c1-0c88360edde8n%40googlegroups.com.
