Optional dependencies

Stream: lean4

[Henrik Böving]

I got another feature question for Lake @Mac I don't know whether this is a thing yet so: With the new facets thing I'm implementing for doc-gen4 the libraries that want to build their docs using this facet have to declare doc-gen as a dependency right? I see two issues with this:

1. Not everyone that wants to compiler mathlib also wants (or even can, I'm not sure whether this works under windows) compile doc-gen
2. When mathlib wants to update its nightly they would now also have to take account doc-gen into potential breaking changes, and wait for me to fix it, that's not desirable either.

Does Lake have a feature or a way to emulate something similar to Rust's dev-dependencies that can be built optionally if required? Otherwise I don't really see how to get a productive integration of doc-gen with LeanInk backlinks going that wont slow down Mathlib development speed/make me the critical path in it.

[Mac]

See lake#80 for the current semi-support for optional dependencies.