std4#215 `Try these`

Stream: std4

[Thomas Murrills]

I'm finishing up std4#215, which adds a "Try these:" widget for lists of "Try this:" suggestions.

I was wondering: is it alright to use <span> instead of <a> for the links? The href field is not used; everything is handled by onclick. The built-in vs code a:hover style interferes with styling on hover in certain cases (causing an unsightly flash to blue). Does switching from a to span interfere with, say, accessibility via screen readers, though? Or anything else? Just trying to anticipate any issues.

[Wojciech Nawrocki]

Btw, this recent addition to ProofWidgets4 means that you should (I believe!) be able to write the entire PR in Lean with no JavaScript. It's understandable if you don't want to rewrite it though! For the clickable button you could use MakeEditLink which currently uses <a>. I observed no flashes with that component, though if you see any it could be switched to a <span>.

The accessibility story is pretty tragic in the infoview atm, but fwiw <a> (semantic tag) is better for that than <span> (styling tag).

[Thomas Murrills]

Oh wow, that's extremely cool! I'd definitely need to look into it though—I haven't written anything in RequestM yet, for example—and that would probably delay this PR even further. :)

Also, does MakeEditLink allow styling of the link? I couldn't see it in the fields or arguments, and that's a crucial part of this PR (for the LLMStep project). (That's the context in which using <a> is an issue: when you hover over it, it flashes back to blue.)

[Thomas Murrills]

So, seeing as this PR has been on the vine for a while, I think we ought to refactor it later, after merging (but we should definitely eventually refactor it)! :)

Btw, re: the PR itself: I noticed that a merge conflict label was added 3 days ago, and I've now cleared that. :)

[Wojciech Nawrocki]

Also, does MakeEditLink allow styling of the link?

Ah, no, but I can easily add that. Good idea!

[Mario Carneiro]

(Note that std does not depend on ProofWidgets, so any fanciness here would have to be inlined into std to be used in TryThis)

[Wojciech Nawrocki]

Oh, I misread this as a mathlib4 PR. In that case indeed, it may not use PW.

[Scott Morrison]

@Joe Hendrix, @Mario Carneiro, I hope std4#215 can be merged soon. @Thomas Murrills has just done some more updates, but it has been awaiting-review for over a month now, with a number of external users (LLMStep, LeanInfer, also loogle and the hint tactic) all eager to make use of it. :-)