Leanprover-community: getting rid of underlining

Stream: general

[Benedikt Ahrens]

Hi,
I am using https://leanprover-community.github.io/lean-web-editor/ for teaching. I have to increase the font size to about 200% to make it readable in the classroom.
The web interface has the habit of underlining #check commands in green. This underlining becomes extremely disturbing with increased font. I use the #check command extensively in teaching, since I find it very useful for exploring. Hence I would really be very happy if the underlining could be deactivated.
Can this be done?
Thanks,
Benedikt
ps. The non-community web interface has less aggressive underlining, but has the inconvenience of showing all the output, not just the output of the line the cursor is located at. Not sure what is the lesser evil...

[Kevin Buzzard]

I have had this same problem, and that is why I switched to VS Code. Another option you should take seriously @Benedikt Ahrens is CoCalc. @William Stein has been telling me to buy a subscription for ages and I finally listened. If you buy one too for something like $14 then you can be showing them Lean in cocalc and they will be able to go to a website and join in. Students will be able to actually write code as answers to questions. It expires after one month. Students can also collaborate on projects without all the faff of GitHub (it's just like Google docs and I've seen it get quite funny with six people editing code at once)

[Kevin Buzzard]

William is also super-responsive when I bring up issues, and I no longer being up issues because it's working fine for me

[William Stein]

@Benedikt Ahrens -- if you have any questions or requests regarding CoCalc+Lean let me know. A critical thing regarding using the web interface and zooming is that you should click the +/- magnifying glass icons in each panel to adjust their fonts, rather than just zooming the whole browser. It's much more likely to work well. For better (or worse) CoCalc doesn't underline anything, since you won't hit the same issue with #check when using CoCalc. Also, with CoCalc, you can re-arrange the panels however you want by closing/splitting/changing modes (in the upper right), much like with Emacs.

pasted image

[Benedikt Ahrens]

Dear @Kevin Buzzard and @William Stein
I have just got a subscription to Cocalc.
I like the mode where I have just the editor window, not the windows on the right-hand side. I use the feedback "info" buttons on the left of the editor window to read off Lean's answers: they pop up upon mouse-over. Unfortunately, the pop-ups are not increased in size when increasing the font size using the magnifying glass icons, it seems. But it does work when increasing the font size in the browser, so all is fine.
Thanks a lot for your advice.

[William Stein]

Many thanks for supporting CoCalc by purchasing a subscription!

"Unfortunately, the pop-ups are not increased in size when increasing the font size using the magnifying glass icons, it seems."

That sounds like a reasonable bug. I can definitely change this. I view the font size as something that should be very easy to adjust locally, e.g., when ones eyes get tired, and it would be reasonable to make the bubbles have a consistent font size with the text. I've made a Github issue for this https://github.com/sagemathinc/cocalc/issues/4392. It probably won't get prioritized highly unless you ping me again though, since I have a lot of priorities right now...

Note also that there is a fullscreen toggle in the upper right, which eliminates all the noise at the top. Also an undocumented feature is you can shift+click on the tab for any file in CoCalc and it'll pop up just that file in a separate pop-window in fullscreen "kiosk" mode, which might be useful for a lecture (not sure).

[Kevin Buzzard]

Please feed back in #Lean for teaching , we would love to hear what goes well and what goes badly

[Kevin Buzzard]

@Benedikt Ahrens

[Bryan Gin-ge Chen]

@Benedikt Ahrens Thanks for bringing this up. I've just added an option to the leanprover-community web editor which lets you disable the squiggly underlines entirely. Click on the (?) button to open the modal and scroll down to the "Decorate code with squiggly underlines for errors / warnings / info" checkbox. The option is a bit of a hack and won't be saved between refreshes, unfortunately.

[Benedikt Ahrens]

@Bryan Gin-ge Chen : Thanks a lot for implementing this - it is a huge improvement for me, and is helping me a lot.