Website Changes

I wanted to kick off a discussion about updating the website.

I was talking to Leo about this at work last week but I would like to make a couple concerted changes to our web presence.

First I think we should improve our exposure online in general, we have built impressive, state-of-the-art infrastructure but haven't done much to publicize this to others. There are many under-documented features that even current users are unaware of.

Landing Page Update

Update the landing page of the website to bring it more inline with
other programming languages.
* We should provide clear examples of how to use Lean for proving, programming, etc
* Demonstrate what programs written in Lean look like, and sign post to downloads,
documentation, and primary chat platforms. See examples such as
https://www.python.org/, https://www.ruby-lang.org/en/, https://www.haskell.org/,
and https://www.rust-lang.org/en-US/.

Lean Technical Blog

Start a Lean technical blog which we update at semi-regular intervals. The posts need
not be long, ideally we could try for brief posts that act as sign posts for new features, or
developments. For example we could write one for new algebra decision procedures,
the new IO subsystem, the state of the native compiler, how to implement something like
super or the z3 tactic, how interactive parsers work, the new structure command, and so
on. I think even if we just spent a small amount of time synthesizing all of our current chats,
issues, and personal thoughts it would be awesome, also see Roadmap.

Communication mediums

At a high level I want to revisit and clarify where communication happens.
I think the current private Slack is a great for internal development chatter, and priorities.
We should discuss updating or clarifying external communication mediums, right now
all kinds of communication (bug reports, language design, help, Q&A) occur via email, Slack, Google Groups, and issues.

Having clearer distinctions about where each type of communication happens, will help us as we continue to acquire new users.

For example if we want to try Gitter out we should make a concerted effort to channel Lean users there. This allows us to form policies around new user problems, such as false bug reports, which we can easily close and direct users to the correct forum. Another example is possibly using Discourse over Google Groups.

We also have quite a few expert users who are not on Slack, and I think it would be good to create a single public (and easily joinable) place for new users to seek help, where both the development team and expert users will be.

Roadmap

My final proposal is a Roadmap for the project as a whole. Currently there are multiple large changes happening each week to Lean, and we should provide a way for users and the development team to sync on the status of various initiatives. This is also a boon to users, new and old, right now we just tell people that a feature is "coming" at some point in the future, but we spend a lot of time and energy communicating the priorities, and that "yes, that feature is planned".

We could just compile a link of RFCs and supporting issues for example, or do something more complicated. I think part of this is ensuring that we publish release notes on each release.

Thoughts would be much appreciated.

No files or tests are named. Start by reviewing the current website structure and the referenced landing pages, then separate the proposal into landing-page, blog, communication, and roadmap work; completion would require defined scope and acceptance criteria for each area.