Per-folder leanOptions

Stream: lean4

[Yaël Dillies]

Over at formal-conjectures in FC#1507, I am trying to disable warn.sorry in the conjecture files (which are full of them because, well , conjectures), while keeping it on in the prerequisite files (which are meant to move towards mathlib mid-term). What is the preferred way to achieve this?

[Yaël Dillies]

My current approach is to declare a new Prereqs library in the lakefile:

[[lean_lib]]
name = "Prereqs"
reservoir = false

However, @Eric Wieser pointed out that this was possibly claiming the name Prereqs too widely.

[Kim Morrison]

So just name it FormalConjecturesPrereqs?

[Eric Wieser]

Adding reservoir = false seems harmful here, since reservoir tracks packages not libraries anyway

[Yaël Dillies]

May I take the opportunity to complain that the valid leanOptions are not documented where the lakefile formats are?

[Kim Morrison]

Could you open an issue against the reference manual (or wherever you were expecting to see such docs)?

[Yaël Dillies]

leanprover/reference-manual#743