calc mode UI in the infoview

Stream: general

[Nehal Patel]

In the infoview there a way to interact with a calc-mode proof by clicking on a part of the goal and using that to introduce the next step in the calc mode proof. I have seen folks demonstrate this "thing" but I cannot remember the details of how to use it or find infor about it by googling. Does anyone know of the name of this "thing" and where it is documented. (Apologies if this is not clear -- happy to try to elaborate) - thank you!

[Nehal Patel]

Found it -- "calc widget" https://www.imo.universite-paris-saclay.fr/~patrick.massot/calc_widget.webm

[Alex Kontorovich]

Wow! That's news to me! @Patrick Massot how does one set this up? @Jon Eugster, any chance this point and click functionality (and conv?) could be implemented in the game server??

[Alex Kontorovich]

Oh I see, there's nothing to set up; it already works. Amazing! (Learn something new every day...) My question for Jon remains... :)

[Chris Henson]

Yes, these are both provided via ProofWidgets. There is also one for gcongr?.

[Michael Rothgang]

And you start using it by typing calc?.

[Michael Rothgang]

Speaking of cool widgets: you know about rw??, right?

[Michael Rothgang]

Can we have a place to document all of these widgets? I didn't consciously know about conv?until now :-)

[Asei Inoue]

deleted

[Jon Eugster]

I have to admit I'm not that interested in getting calc mode working for games. It seems calc is fundamentally incompatible with the unstructured, single-line, step-by-step tactic proofs which are taught in lean4game.

Therefore it seems like it would require either a lot of hacky setup or a fundamentally different approach to get calc working in a usable way...

Ensuring that "Try this" links (rsp ProofWidgets) like the ones above are displayed clickable in the game's infoview should be comparatively easy. If they aren't already, that probably just broke at some point and needs to be fixed again.

[Patrick Massot]

This calc widget have been there forever. I created it before the port from Lean 3 was completed. But I know it’s easy to miss. I know it’s explained in GlimpseOfLean but I don’t even think we mention it in MIL. We have a lot to do on MIL in Lean anyway, there are too many powerful tactics that were created in the last two years and didn’t make it to MIL.

[Jovan Gerbscheid]

By the way, I'm working on some improvements to rw??. In particular I'm parallellizing the computation and making the widget show the results when some of the suggestions are available and others are still being computed. See also #general > Widget that reacts to Lean

[Kim Morrison]

I would love this mechanism to be sufficiently generic that we could also make use of it for try?!

[Jovan Gerbscheid]

The mechanism depends on a small amount of TypeScript, and I'm planning to make a PR for this to ProofWidgets soon. I'm not sure though how it would work to upstream that into core.

[Anand Rao Tadipatri]

It's possible to create a component directly using JavaScript, and that can be placed in core.

[Jovan Gerbscheid]

Yes, though there is still the problem that I'm using the type ProofWidgets.Html to represent the widget, which lives in ProofWidgets.

[Anand Rao Tadipatri]

Yes, I just realized -- there's probably no easy way around this then.

[Jovan Gerbscheid]

I think we can work around the lack of ProofWidgets.Html by creating all of the HTML on the JavaScript side. This would require writing a version of my JavaScript code, specialized to the particular use case. And I think that the try? interface is simple enough where this is reasonable to do.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I would advocate for putting this in ProofWidgets for now. In general, the idea is to prototype features there, and move them up to core when either a) there is no way to implement it out-of-core because some API is missing or b) it is widely used enough that moving it up makes sense.

[Kim Morrison]

Sounds good to me. These features are great, but potentially fragile and expensive to maintain. Please (authors and reviewers) do your utmost to write robust, safe, well-documented code. :-)