Closed madvorak closed 1 year ago
Is the main problem the following?
Adhere to the guidelines: The style guide for contributors. The explanation of naming conventions. The documentation guidelines.
Yeah, I think it doesn't make sense to update a page on the website in a piecemeal fashion. Any page that gets updated should be subject to a complete overhaul (even if much of the information ends up being similar). For instance, this page still makes mention of leanproject
in several places that are not changed, and I'm not sure we even want to suggest forking anymore since we never use it due to our CI setup. There's probably a lot that needs to be revisited.
As for the style guide, I actually have that mostly rewritten already. I'll try to get a PR up tonight or tomorrow for that.
I don't want to work on a complete overhaul. Should I close this PR? Somebody else will hopefully do it in an organized manner.
Ok, let's close it for now.
Thanks Martin. I am a bit worried that this would create a web page that is updated to Lean 4 but crucially linked to the style page that is still completely Lean 3. Do you think you could work on this one?
I'm also pinging @j-loreaux who updated the naming page.