> I'd say make more space or make the containers scrollable for formulas that don't fit. Thanks, it's fixed now -- not perfect but good enough.
> its setting "Appearance -> Font Size" is set to "Very Large" Thanks, I fixed it and this works fine now [email protected] schrieb am Freitag, 7. Juni 2024 um 08:59:06 UTC+2: > > Do you have any suggestions for improvement or feature ideas? > > > Apparently, you have already fixed the overlays by just cutting formulas > off. > > I'd say make more space or make the containers scrollable for formulas > that don't fit. > ------------------------------ > *Von:* [email protected] <[email protected]> im Auftrag von > Matthias Vogt <[email protected]> > *Gesendet:* Donnerstag, 6. Juni 2024 23:54:11 > *An:* Metamath > > *Betreff:* Re: [Metamath] Metamath proof visualizer with graphs > Thanks everyone for the compliments c: > > > I did find a minor problem with the graph display - the bottom part of > the text > > labels gets cut off. E.g., in "eqtr4i" you can't tell it's a "q" because > the bottom > > tail is cut off. I suspect a minor tweak would fix it. > I can't reproduce this in chrome or Firefox unfortunately, what browser > are you using? > > > For printing LaTeX or Unicode for the terms in the substitutions, maybe > there could be some web service serving the HTML version, whenever provided > with ASCII ? > That would work, or if https://expln.github.io had support for this, that > would also work > > > Nice! did you use https://reactflow.dev/ ? > Thanks for the recommendation, It's just vanilla javascript and d3.js but > for a rewrite I would use react. > > > the visualizer looks somewhat hilarious / messy for proofs with large > formulas: https://vo.gt/mm/mpeuni/retbwax1#triv1733 > Fixed, thx > > Do you have any suggestions for improvement or feature ideas? > [email protected] schrieb am Donnerstag, 6. Juni 2024 um > 01:52:18 UTC+2: > >> This looks really damn cool. >> Though the visualizer looks somewhat hilarious / messy for proofs with >> large formulas: https://vo.gt/mm/mpeuni/retbwax1#triv1733 >> ------------------------------ >> *Von:* [email protected] <[email protected]> im Auftrag >> von Johnathan Mercer <[email protected]> >> *Gesendet:* Dienstag, 4. Juni 2024 01:46:42 >> *An:* [email protected] >> *Betreff:* Re: [Metamath] Metamath proof visualizer with graphs >> >> Hi Mattias, >> Nice! did you use https://reactflow.dev/ ? >> >> On Mon, Jun 3, 2024 at 6:31 PM Mario Carneiro <[email protected]> wrote: >> >>> This is amazing and super awesome, and I will be using it in all my >>> talks from now on. :) It makes me more excited for getting that site >>> rewrite project moving forward... >>> >>> On Tue, Jun 4, 2024 at 12:27 AM Matthias Vogt <[email protected]> >>> wrote: >>> >>>> Hi everyone, >>>> I wrote a cool visualizer for metamath proofs :3 >>>> >>>> [image: Screenshot from 2024-06-03 20-54-43.png] >>>> It can... >>>> >>>> - Show the proof steps as an interactive graph >>>> - Show the proof as interactive nested proof blocks, from >>>> conclusion to premises >>>> - Summarize proofs and explain proof steps (I only hand-wrote >>>> explanation-functions for a few theorems, e.g. "by transitivity..." >>>> below) >>>> - Hide proof steps that you consider trivial, i.e. have a theorem >>>> number less than x >>>> >>>> You can view it (please use desktop) at https://vo.gt/mm/mpeuni/2p2e4 >>>> or add it as a tampermonkey extension <https://vo.gt/mm/extension.js>. >>>> You can replace "2p2e4" in the URL with any theorem you like. >>>> >>>> This is at the moment a super slow and hacky proof of concept and there >>>> are likely many bugs. The site above mirrors metamath.tirix.org (if it >>>> is not OK that I am mirroring math.tirix.org, please tell me and I >>>> will of course take down this demo site. It is not indexed by search >>>> engines or linked anywhere except here.). It also makes lots of requests >>>> to >>>> metamath.org to get the theorem numbers. Moreover, it runs the >>>> expln.github.io <https://expln.github.io/metamath/asrt/2p2e4.html> >>>> react code to get the substitutions that show us how theorems are used in >>>> proof steps. The code is basically an unmaintainable fever dream :p If >>>> there is interest, I might rewrite it in react at some point in the >>>> future. >>>> But I hope you like it anyway :) >>>> >>>> The basic idea for summarizing proofs is that smaller theorem numbers >>>> correspond to logic glue, so we can just not mention these theorems >>>> explicitly in the proof. Instead, when we have a non-trivial step, we just >>>> silently add the application of the trivial theorem to the resulting >>>> expression. The threshold for what is trivial customizable with the >>>> slider. >>>> Swallowing logic glue helps for readability, but still, in reality, I >>>> think >>>> what part of a proof is verbose is more of a stylistic decision by the >>>> author. >>>> >>>> What would make the visualizer even better is if there was a way to get >>>> LaTeX or Unicode output for the terms in the substitutions. But I don't >>>> know how to do this. If expln.github.io >>>> <https://expln.github.io/metamath/asrt/2p2e4.html> had LaTeX/Unicode >>>> support, that could be used for the visualizer for example. >>>> >>>> Best >>>> Matthias >>>> >>>> -- >>>> 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/6fd3b538-ac91-431f-a476-9d79e4754b14n%40googlegroups.com >>>> >>>> <https://groups.google.com/d/msgid/metamath/6fd3b538-ac91-431f-a476-9d79e4754b14n%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> -- >>> 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/CAFXXJStDO%2BphLRPGV63VGHzrc18vjej-72y2sfME8_QEMerCUw%40mail.gmail.com >>> >>> <https://groups.google.com/d/msgid/metamath/CAFXXJStDO%2BphLRPGV63VGHzrc18vjej-72y2sfME8_QEMerCUw%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- >> 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/CAHvyvqqG5_dH%2Bwr_1V0TPNjUryXyXVVMYSAifUHFRn-9QGNSxw%40mail.gmail.com >> >> <https://groups.google.com/d/msgid/metamath/CAHvyvqqG5_dH%2Bwr_1V0TPNjUryXyXVVMYSAifUHFRn-9QGNSxw%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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/f6027a4f-9fb9-4102-b31c-e560fb80de6en%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/f6027a4f-9fb9-4102-b31c-e560fb80de6en%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/162f37dc-6e40-4959-8a05-6bf30f3ab0c3n%40googlegroups.com.
