Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

Website Changes

Abierto
  • ¿Algo no está bien?
#66 1 comentario 3 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
15/100
Tipo de issue
Nueva funcionalidad
Claridad
Necesita aclaración
Estado de actividad
Estancado
Stack tecnológico
html
Área
content, documentation, web-dev

Línea de trabajo

No se mencionan archivos ni pruebas. Empieza revisando la estructura actual del sitio web y las landing pages referenciadas, y después separa la propuesta en trabajo de landing page, blog, comunicación y roadmap; para completar el trabajo será necesario definir el alcance y los criterios de aceptación de cada área.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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.

Lenguaje dominante
HTML
Estrellas
17
Forks
25
Sin PR fusionados en 30 d

Preparar el entorno

Este proyecto no incluye contenedor de desarrollo, Dockerfile ni guía de contribución, así que la configuración corre por tu cuenta: empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de leanprover/leanprover.github.io

Todos los issues de leanprover/leanprover.github.io

Issues similares

Más issues de Content

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.