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/405c8e78-7405-4455-b375-86c609b27f69n%40googlegroups.com.
