Hi all, Last week, I've made a number of updates (dare I say improvements?) to my 'userscript' mm-calc2 (link <https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc2.user.js> to latest version, currently at version 7).
It still does essentially the same thing, namely display a calculation above any 'proof table' on metamath.org (and metamath.tirix.org), on every Unicode page (so not the GIF pages). It does not only work with GreaseMonkey <https://addons.mozilla.org/en-US/firefox/addon/greasemonkey/> which is Firefox-specific, but I've verified that it also works in Chrome with either Tampermonkey <https://chrome.google.com/webstore/detail/tampermonkey/dhdgffkkebhmkfjojejmpbldmpobfkfo> or Violentmonkey <https://chrome.google.com/webstore/detail/violentmonkey/jinjaccalgkegednnccohejagnlnfdag>, and probably it works in any modern userscript-supporting browser. The new version makes some changes that are probably not for everyone, but for me personally, it helps me tremendously to read metamath.org proofs. It might help others as well. Changes since version 3 of June 2018, most visible ones first: - The calculations are now 'up-side-down', starting with the goal. - Initially only the top-level calculation is shown, the rest can be expanded. (Yes!) - I now use two very crude heuristics to find which hypothesis to use as the next step in each calculation (see function guessMainSubproof()): - Take the hypothesis which is closest in length to the conclusion; - But avoiding if possible a 'reused' step. - Reorder the references in each 'hint', to make the 'key' step usually appear first and the 'auxiliary' steps last. - Bugfix: Now points correctly to 'reused' steps (although they can be hard find as they're usually initially inside hidden subproofs). Again, this script is by no means perfect, but for most proofs it really helps me understand the structure of the proof better, and it surprised me how effective the above simple heuristics are. Feedback welcome, but again, I have no idea when I'll again be able to spend significant time on this. Groetjes, <>< Marnix Op za 9 jun. 2018 om 09:35 schreef Marnix Klooster < [email protected]>: > Hi all, > > Yesterday I got tired of manipulating the existing HTML proof tables in my > Greasemonkey script, so I hacked up 'mm-calc2' which more directly renders > to the proof format I have in mind, leaving the original proof table > untouched. Get it at > https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc2.user.js. > Above each proof table, it renders a calculational equivalent of the > table. It currently also works on metamath.tirix.org. > > Try it, for example, on http://us.metamath.org/mpeuni/eulerth.html and > http://metamath.tirix.org/eulerth.html. Or on > http://us.metamath.org/mpeuni/ru.html and > http://metamath.tirix.org/ru.html. > > This initial version of mm-calc2 does not yet do collapse/expand, and it > just shows both formats at the same time. So it will look not look too > good on large proofs-- but I'd argue the table format is not easier to > understand for large proofs anyway. :-) > > Also, it has a bug in that it doesn't show reused steps correctly. (For > example, in http://us.metamath.org/mpeuni/pm5.54.html, the second > reference to step 2 / bicomd is missing.) > > But despite these restrictions, it already helps me read some proofs more > easily, especially with the formatting on metamath.tirix.org. > > And for the future this gives me a kind of 'test bed' to try different > orderings of the same calculation, e.g. using a chain of <== instead of > ==>, choosing not the first antecedent but a different one, or even using > set.mm operators like <-> and = in the left hand column, instead of just > the 'meta-implications' ==> and <==, and removing repetition by extracting > common contexts like this: > > In context β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β ...) we have > > (1...(Οβπ)) β {π β (0..^π) β£ (π gcd π) = 1} > β βusing sylib <http://us.metamath.org/mpeuni/sylib.html> 189 and bren > <http://us.metamath.org/mpeuni/bren.html> 7108β > βπ π:(1...(Οβπ))β1-1-ontoβ{π β (0..^π) β£ (π gcd π) = 1} > Again, no idea when I'll continue work on this, feedback welcome. > > Groetjes, > <>< > Marnix > > 2018-06-06 18:07 GMT+02:00 Marnix Klooster <[email protected]>: > >> *(Forgot to include the group...)* >> >> Hi Thierry, >> >> Thanks for including, and so quickly! :-) >> >> What that indentation algorithm does, is take a tree like >> >> 2: F >> 4: E >> 3: D >> 3: C >> 2: B >> 1: A >> >> and make it look like a calculation, by indenting the first >> parent/antecedent of a step the same as the step, the second one level >> deeper, etc.: >> >> 2: F >> 4: E >> 3: D >> 3: C >> 2: B >> 1: A >> >> This is intended to match the following calculational proof: >> >> F >> ==> "by sub-proof" >> >> E >> ==> >> D >> ==> "by C" >> B >> >> A >> >> I'm trying to update my Greasemonkey userscript to collapse/expand on the >> granularity of such calculations and sub-calculations, and to render proofs >> more and more in this form. >> >> Even with the current limited indentation form, with basically your >> (Thierry's) expand/collapse, a number of proofs start to be actually a bit >> readable to me. :-) >> >> And yes, a large proof will still indent quite a lot, and my indentation >> size might a bit too large-- but still for me it is an improvement on the >> standard metamath /html format. I think that my algorithm actually indents >> less than the original format... >> >> Groetjes, >> <>< >> Marnix >> >> 2018-06-06 16:34 GMT+02:00 Thierry Arnoux <[email protected]>: >> >>> Hi all, >>> >>> Because not everybody has Firefox and Greasemonkey, I've included >>> Marnixes scripts on my pages. >>> You can switch to this indentation by clicking the "M" on the top right >>> of the proof tables (you have to reload page to switch back to the original >>> display). >>> >>> Marnix, you did not provide much explanation, could you tell how it's >>> working? >>> >>> BR, >>> _ >>> Thierry >>> >>> >>> On 06/06/2018 04:10, Marnix Klooster wrote: >>> >>> Hi all, >>> >>> For quite a while I've been looking into different ways to render >>> Metamath proofs-- and Thierry's rendering experiments (which look great!) >>> inspired me to do some experiments in JavaScript. >>> >>> To allow me easy experimentation, I've chosen to use Greasemonkey on >>> Firefox. >>> >>> To use this, you need to install the Greasemonkey add-on ( >>> https://addons.mozilla.org/en-GB/firefox/addon/greasemonkey/), and then >>> open or install my script from >>> https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc.user.js >>> . (I think your Firefox Greasemonkey should auto-update when I change this >>> script the correct way, but I'm not sure yet.) >>> >>> (Caveat emptor: For any Greasemonkey script you run, make sure you get >>> it from a trusted source, and analyze the source code if you're not sure. >>> The above script runs with no special permissions.) >>> >>> The goal of this script is to make a proof look more like a >>> 'calculation', which (for me at least) usually makes them easier to >>> follow. For example, try it on http://us.metamath.org/mpeuni/ru.html >>> or http://metamath.tirix.org/ru.html (with all steps expanded). >>> >>> The current version of this script only re-indents the formulas in a way >>> that makes more sense to me than the usual tree structure. (Tested on >>> metamath.org Gif+Unicode and metamath.tirix.org.) >>> >>> I have ideas for other changes/improvements, but I have no idea whether >>> I will have the time... >>> >>> Anyway, feedback welcome, and enjoy! >>> >>> Groetjes, >>> <>< >>> Marnix >>> -- >>> Marnix Klooster >>> [email protected] >>> >>> >>> >> >> >> -- >> Marnix Klooster >> [email protected] >> >> >> >> -- >> Marnix Klooster >> [email protected] >> > > > > -- > Marnix Klooster > [email protected] > -- Marnix Klooster [email protected] -- 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/CAF7V2P8cJXnqH7OwSHQ0k12hQMMO3E6vtNfv5pWrw4JrnZZD8g%40mail.gmail.com.
