Hiding values of `let` declarations in Verso

[0art0]

CC: @anshula

Thanks for developing Verso! We were wondering — it seems sometimes set_option flags work within Verso, e.g.

set_option linter.unusedVariables false

But it seems that let-values still show in the tactic proof state even if we have

set_option pp.showLetValues false

We found that disabling the option in the lakefile does not seem to help.

Is this a bug, or is there some other avenue to accomplish this?

Thanks!

[david-christiansen]

Thanks for checking! What you're looking for should absolutely be possible, but Verso is a fairly flexible piece of software with multiple ways to include Lean code and proofs.

Can you make an MWE that demonstrates the issue? That is, a small document/website that has just one proof state with an unwanted let in it that's ignoring the option?

[david-christiansen]

Actually, on further thought, I think I know what's up. The rendering of goals doesn't presently consult this option at all.

Is this option the way you want to control the display? Or would you rather have a different place to control how proof states show up in your document (e.g. part of the document itself rather than part of the code being documented)?

Perhaps you can describe the project you're working on and how it's set up?

[anshula]

cc: @0art0

@david-christiansen Thanks for your help!

Perhaps it could be nice if the set_option could be part of the document itself (i.e. if we could put that line just below import VersoBlog, for example). But -- as for the setup of the project -- it's a VersoBlog with multiple pages, so it could be nice if there was some global flag. Still, if it's easier to implement as part of the code being documented, that's also fine, since we could include a snippet setting these options with the flag show:=false.

Currently, we're working on a project where the proofs of the hypotheses are quite long, but they have to be let rather than have statements since we modify the proofs at later times.

Does that address the question?

[david-christiansen]

Yes, that's helpful!

I'm pretty sure this can be made to a parameter of the main function, which would make a setting that could be overridden on a per code block basis. It doesn't have to go through the set_option interface, though it could be made to do so.

How urgent is this?

[anshula]

Oh wonderful. It's not necessarily urgent -- the documentation we have is already live online, so the sooner we can put out the update, the better, but it is serving its function as-is :)