search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
232 stars 95 forks source link

chore: remove 'meta if' from lakefile #869

Closed semorrison closed 2 months ago

semorrison commented 2 months ago

As far as I understand, no human or automation ever runs doc-gen on Batteries. Instead documentation is generated as part of Mathlib's documentation.

If that is the case, I would like to remove the doc-gen dependency from the lakefile.

(This is on the path to moving to a lakefile.toml, and eventually possibly deprecating meta if in lakefile.lean.)

digama0 commented 2 months ago

(This is on the path to moving to a lakefile.toml, and eventually possibly deprecating meta if in lakefile.lean.)

I think we should discourage meta if but not deprecate it, certainly not before getting conditional dependencies in lakefile.lean and/or .toml, but possibly even after because I'm sure there are OS dependent projects and other things that need to script their lakefiles at configure time. It just needs to become a niche feature and disappear from the main big lean projects.