leanprover
RFC: Presentation / Demo mode
Proposal
Provide a "Presentation / Demo" mode that would toggle on / off some useful options for using vscode-lean4 when doing talks, demos, or congress presentations.
-
User Experience: How does this feature improve the user experience?
As of today, users have to enable / disable the features one by one, which is cumbersome
-
Beneficiaries: Which Lean users and projects benefit most from this feature/change?
Everyone doing presentations / demos with Lean4 / VSCode
-
Maintainability: Will this change streamline code maintenance or simplify its structure?
Should not have a large impact, main change is to store the previous values in some record. Determining the set of options affected could be complex tho.
Community Feedback
This was discussed in person at the Big Proof workshop 3, INI, Cambridge. I'll be happy to move the discussion to Zulip if needed.
I cc @PatrickMassot who originally suggested the presenters to use a different set of options for more feedback on this issue (Patrick please edit this issue as you see fit)
I'd be curious which settings you'd expect to be set here. Is it just the automatic hover settings for the editor and the InfoView?
I think so, thanks!
But I'll let @PatrickMassot answer as he has a much better idea on what needs to be done. I'm also taking the freedom to cc: @JovanGerb
Yes, @PatrickMassot suggested to me after my presentation to change some settings. I think the changes include
- turn off pop-up suggestions when typing.
- turn off hovers in the infoview (which is currently set in lean web).
But as a person presenting, I think the most important thing is to have a pointer to what I should change and how. It taking a couple extra clicks isn't a big deal.
In fact, I was trying to turn off the typing pop-up suggestions before the talk, but couldn't figure out on time how to do it.
@JovanGerb , a possibility would be to add a pair of VSCode commands "Lean: Start talk mode" and "Lean: Stop talk mode" (maybe "Presentation mode"?)
The documentation of the commands could mention the settings affected, and store them for restore. What do you think?
In my neovim presentation command I also change the colorscheme and font to get maximal contrast and bolder text. But this has nothing to do with Lean.
