tests for conv? widget

Stream: mathlib4

[Bryan Gin-ge Chen]

I noticed that we don't have tests for some of our widgets, including the conv? widget which has an open PR #25889 by @Aaron Liu (see also #mathlib4 > bug in `conv?`) (at least none appear to have been added when they were merged in #7260).

I believe it would be good to make sure that the issues that Aaron has fixed this time remain fixed going forward. However, this is far from my area of expertise, so let me ask here: does anyone have any ideas on how we might add tests?

[Julian Berman]

(I don't think it will satisfy the need, not least of which given that the implementation is not fully the same, but FWIW, I have a baseline test for conv? in lean.nvim https://github.com/Julian/lean.nvim/blob/main/spec/widgets/mathlib_spec.lua which at least will fail if it totally breaks.)

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

Lean itself has a number of interactive tests which come with a custom runner that starts the Lean server. Then the LSP packets sent by the server in response to specified requests are compared against the expected baseline. With conv?, though, the initial packets are mostly uninteresting since they only contain the JS sources. The more interesting ones come from invoking insertEnter. I would suggest having tests which invoke that directly and inspect the output; this avoids the need to run a Lean server or worse, to run/render JS in tests.

[Aaron Liu]

Good news, I've added tests