[RFC] Roadmap

[jroesch]

I would like to start on the construction of a Roadmap for Lean.

At a high level I believe we should create issues for all current "accepted" wishlist features, properly categorize them and provide status and priorities for the features we have in the pipeline.

I think this is important for reducing the communication load on core developers, instead of continually explaining the status of these "wishlist" features we can point concretely and transparently at our priorities, and the status of major features in the system.

I think these issues should be tagged both in the GH issue tracker, in the heading, and listed on the roadmap.

My high level design for the Roadmap is just an ordered listing of important tracking issues or milestones with a small blurb, and pointer to the issue.

Ideally we will order these by a rough priority, and tag ones that would be easy to mentor or be implemented by non-core developers.

I know I have been pushing on these sorts of things the last few days but I would love to get a coherent story about our development priorities, release schedule, and upcoming features to ship with the website, and updated communication policies.

I will kick off the thread with some examples of features that should be on the roadmap:

• mutual keyword
• coinductive types
• build tool status (I know this one is almost ready 🥇)
• native compiler
• specific tactics
• arithmetic
• structure redesign
• pattern match compiler improvements

[gebner]

I'm not entirely clear on one point: do you propose to have a separate page on the website that contains a list of roadmap entries, which needs to manually kept in sync with the github issues? I'm not saying this is a bad idea, just that somebody would need to be responsible for it.

Just as important as getting a new roadmap out there is removing all the old ones, like this: https://github.com/leanprover/lean/blob/master/doc/todo.md

Here are two other features:

• Well-founded recursion
• Parser extensions

[jroesch]

@gebner I am open to either, we could rely on Github issues' tagging and milestones or maintain/generate a page on the website. I'm imagining if we maintain a separate page updates will be rare (when we propose new features) after we collect all of the current set.

[spl]

A roadmap would definitely be useful.

It would also be useful to clarify and document the issue/PR policy. For example, #392 (well-founded recursion) has been open for a long time, but #1441 (coinductive) was documented and closed with no plans to work on it. Other features have appeared as PRs without previous public discussions of those features.

All of this is not to say “don't do it” but rather to aim for consistency and transparency. 😄

(Sorry if I'm rehashing my recent email like a broken record. I just think it's important enough to emphasize.)

[leodemoura]

@jroesch I think new github tags + issues is probably the simplest solution. We can add links to them from the main page. @gebner raised an important issue, if we have a separate page, then someone would have to be responsible. This kind of page rots pretty quickly. BTW, I didn't even remember we had a "todo.md" file.

We can have "priority" tags. These tags would inform users about features that are being implemented in the near future.

[leodemoura]

@spl Well-founded recursion is on the TODO list, and it will be eventually implemented.
On the other hand, you should not hold your breath for coinductive datatypes. They will not happen in the following years, unless someone as strong as @gebner or @Kha shows up and decides to implement this feature.

The issue #1441 was created because @cmr was curious about it, @avigad documented the experiment that has been tried. The experiment was a feasibility test to show that coinductives can be added to Lean without extending the kernel. Nobody tried to implement this feature. I ask the issue to be closed because nobody in the current development team is planning to work on it.

Other features have appeared as PRs without previous public discussions of those features.

I don't think it is feasible to discuss every new feature publicly.
Some of them are implemented and merged without any discussion because they are clearly useful.

[spl]

@leodemoura:

Thanks for your response.

Well-founded recursion is on the TODO list, and it will be eventually implemented.
On the other hand, you should not hold your breath for coinductive datatypes.

In case it wasn't clear, I didn't mean to pick these out because I wanted to know about them. They were merely examples.

They will not happen in the following years, unless someone as strong as @gebner or @Kha shows up and decides to implement this feature.

The issue #1441 was created because @cmr was curious about it, @avigad documented the experiment that has been tried. The experiment was a feasibility test to show that coinductives can be added to Lean without extending the kernel. Nobody tried to implement this feature. I ask the issue to be closed because nobody in the current development team is planning to work on it.

You might consider this feature to be something in which you acknowledge that it is not a priority for core developers but are willing to accept a contribution. One common way to do this is by keeping an issue open and using it as an ongoing reference for possible future work. @avigad's writeup is a great description of the issue for anybody who wants to look into it. While you may close the issue because you and the core developers don't actively plan on implementing it, the fact that the issue is closed can look to others like there is no desire for the feature, even though there may be.

This is the kind of thing I was referring to in the issue/PR policy I mentioned. There are, I think, certain default expectations approaching issues, esp. on GitHub. You may find yourself following these expectations or not. Either way, you may want to document your policy as a reference for others. (By the way, descriptive GitHub labels are a good way to add semantics to issues.)

I don't think it is feasible to discuss every new feature publicly.
Some of them are implemented and merged without any discussion because they are clearly useful.

Fair enough. I grant you that it is more efficient on development time. However, it does lack the more-eyes-are-better perspective that a more open development model provides. But if your priority is on producing code, it's better to avoid too much discussion.

[leodemoura]

You might consider this feature to be something in which you acknowledge that it is not a priority for core developers but are willing to accept a contribution.

I really doubt we will ever receive a contribution for this. The implementation is much more complicated than it seems. If someone wants to work on this, s(he) will have to start small, and implement simpler things in the code base, and eventually build this one. Moreover, they will have to discuss many different issues and integration problems with the core developers. My point is I don't want to waste my time anymore.
When I started Lean, I imagined we would have many contributions of this kind. Unfortunately, this is not the case. The most common interaction is: potential contributor starts asking tons of questions; then suggesting half baked designs that do not work; and then gives up. I have wasted a lot of time in this kind of interaction. Note that, @gebner and @Kha are rare exceptions, they barely ask any question; propose great designs; and implement a lot of code.

One common way to do this is by keeping an issue open and using it as an ongoing reference for possible future work.

We have a wiki for it: https://github.com/leanprover/lean/wiki/Coinductive-Types

Either way, you may want to document your policy as a reference for others.

I will.

(By the way, descriptive GitHub labels are a good way to add semantics to issues.)

We will add more.

Fair enough. I grant you that it is more efficient on development time. However, it does lack the more-eyes-are-better perspective that a more open development model provides.

I don't believe "more-eyes-are-better". Or more precisely, I don't believe "more-(arbitrary)-eyes-are-better". Note that, we barely get any useful feedback for technical problems.

But if your priority is on producing code, it's better to avoid too much discussion.

The priority is not code, but impact. We need a set of capabilities to have the impact we want.

[leodemoura]

I added Rust-like labels, and we will use them to mark future features, priorities, etc.
The issue tab will be our "roadmap"