That looks great. Congratulations! Benoît
On Saturday, December 19, 2020 at 9:05:07 PM UTC+1 [email protected] wrote: > Hello Norm, > > I’ve prepared a final version of my proof visualizations which you may add > links to on the main site. URLs of pages have a form of > https://expln.github.io/metamath/asrt/label.html Where “label” should be > replaced with the actual label of an assertion. (“asrt” stands for > “assertion” and it is a constant part of the URL) For example: > https://expln.github.io/metamath/asrt/sqrt2irr.html > > I spent some time investigating if I can implement unicode representation > but it appeared complicated because each symbol is represented as raw html > code. And it is not trivial to embed it into SVG visualization. > > Please let me know if everything is ok and you can add links to this > version. > > Best regards, > Igor > вторник, 8 декабря 2020 г. в 20:17:37 UTC+1, Igor Ieskov: > >> Yeah, that would be an honour for me to make a contribution to Metamath. >> Sure, I want to solve few technical issues, test them during some time and >> then you can add links. >> >> I also thought regarding unicode symbols. I will spend some time to try >> to add possibility to show both ascii and unicode symbols (but I don't >> promise to do it fast enough because of lack of time :) ) >> >> Actually I've just figured out that I can use this feature of >> metamath.exe to verify what my program generates. This is not >> straightforward though but possible. >> >> I will write a message when I think this my visualisation is stable >> enough so we can start adding links. >> >> Best regards, >> Igor >> >> вторник, 8 декабря 2020 г. в 17:13:15 UTC+1, Norman Megill: >> >>> When this becomes stable, I can add a link to your version on each >>> theorem page of the main site, like the link that now says "Structured >>> version" for Thierry's pages. This will let you have direct control over >>> your content. (To start with, your base URL would be hard-coded in >>> metamath.exe, but later I can add a keyword to the $t statement in >>> set.mm so the URL can be maintained there.) >>> >>> I don't know your long term plans, but I'll mention that personally >>> (although I may be in the minority) I don't mind the ASCII notation in the >>> proofs. It shows a beginner the direct relationship to the set.mm >>> source and allows easy copy/paste. The user can also see the direct >>> relationship between the ASCII and the Unicode rendering by switching >>> between your page and the standard page, without having to consult >>> set.mm or the awkward "ASCII Symbol Equivalents" page. >>> >>> BTW although of course it's not as convenient as your pages, some people >>> might not know that metamath.exe can show the substitutions made in a step: >>> >>> MM> show proof 2p2e4 /detailed_step 18 >>> Proof step 18: eqtr4i.1=oveq2i $p |- ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ) >>> This step assigns source "oveq2i" ($p) to target "eqtr4i.1" ($e). The >>> source >>> assertion requires the hypotheses "cA" ($f, step 13), "cB" ($f, step >>> 14), "cC" >>> ($f, step 15), "cF" ($f, step 16), and "oveq1i.1" ($e, step 17). The >>> parent >>> assertion of the target hypothesis is "eqtr4i" ($p, step 47). >>> The source assertion before substitution was: >>> oveq2i $p |- ( C F A ) = ( C F B ) >>> The following substitutions were made to the source assertion: >>> Variable Substituted with >>> C 2 >>> F + >>> A 2 >>> B ( 1 + 1 ) >>> The target hypothesis before substitution was: >>> eqtr4i.1 $e |- A = B >>> The following substitutions were made to the target hypothesis: >>> Variable Substituted with >>> A ( 2 + 2 ) >>> B ( 2 + ( 1 + 1 ) ) >>> >>> Norm >>> >>> >>> On Tuesday, December 8, 2020 at 9:27:57 AM UTC-5 [email protected] >>> wrote: >>> >>>> Norm, Jim, thanks for your feedback! >>>> >>>> I updated the proof visualisation - all steps are collapsed by default >>>> and a [+] button will expand selected node. Examples: >>>> http://metamath.d4-e5.de/v2/data/2p/2e/2p2e4.html >>>> http://metamath.d4-e5.de/v2/data/sq/rt/2i/sqrt2irr.html >>>> http://metamath.d4-e5.de/index.html >>>> >>>> Also offline version may be found here >>>> https://drive.google.com/drive/folders/1na2UM270rsCd85BQCmaJJSnak8HywfL8?usp=sharing >>>> (its >>>> size is 500M when unarchived). >>>> >>>> At the moment, step numbers in my proof visualisation don't correspond >>>> to step numbers on http://us.metamath.org in many cases. This is >>>> because of duplicate steps in my visualisation. I will fix this. >>>> >>>> Best regards, >>>> Igor >>>> >>>> вторник, 1 декабря 2020 г. в 03:22:00 UTC+1, [email protected]: >>>> >>>>> On 11/30/20 6:03 PM, Paul Chapman wrote: >>>>> >>>>> > I may be getting too old/lazy to code. Thirty years ago I’d’ve >>>>> written >>>>> > a knockout replacement for mmj2. ;) >>>>> >>>>> Haha I'll let you be the judge of whether you are too old/lazy to >>>>> code. >>>>> >>>>> But if you are just disinclined to shave all the yaks required to get >>>>> a >>>>> smalltalk compatible with that experiment running again, hey that >>>>> strikes me as quite understandable quite aside from age. Quite a saga. >>>>> >>>>> >>>>> -- 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/019bbe17-5724-4b9d-87f4-b49550fb25f2n%40googlegroups.com.
