Update Lean version, host doc-gen results for CW Lean version

[Voileexperiments]

Last time CW Lean version was updated was from #2, and that version of Lean is over 1 year ago.

Many useful lemmas, theorems and namespaces are either changed or outright missing. Meanwhile, Mathlib docs is only available for the current version, so there is no way to know what is available on the (severely outdated) version of CW, creating artificial barriers to Lean katas.

Things to do:

• Update CW Lean version from v3.20.0 to current (or close to current) version
• Host a copy of doc-gen generated documentation somewhere on CW that always match the most up-to-date version of Lean used by CW. It's all static files so there should not be much concern about hosting.
• Devise a schedule (annually? biannually?) to regularly update Lean version: Lean keeps making big changes all the time like Swift, and many people have asked about keeping Swift edition up to date in the past. It's just that there are like only 10 people who uses Lean on CW, so this is much less noticable.

[monadius]

I would like to update all Lean kata to 3.20.0 before introducing a new Lean version. If a new version is added, somebody needs to update many existing kata. I hope that this list of kata to update is complete. I still need to solve 2 remaining kata (I am almost done with the first).

[kazk]

I'm not adding a new version until 3.18.4 is gone. https://github.com/codewars/content-issues/wiki/List-of-Lean-Kata-to-Update

Host a copy of doc-gen generated documentation somewhere on CW that always match the most up-to-date version of Lean used by CW

We can create a repo like https://github.com/leanprover-community/mathlib_docs and link from the docs.

Devise a schedule (annually? biannually?)

I won't update without a request, and I won't update too frequently, considering the number of users. Biannually should be fine. I also won't support more than 2 versions, so all the kata needs to be updated to the newer version first.

[monadius]

@Voileexperiments do you want to prepare docs for the current CW version and create a pull request in the CW docs repository (or is it better to create a separate repository)? If you don't have time, I will try to prepare these docs during the weekend.

[kazk]

A separate repository is preferred because it's not small, and it might be tricky to make it work within the docs site.

I can create a blank repo and accept a PR.

[kazk]

@monadius I gave you the Write permission for https://github.com/codewars/mathlib_docs so you can push directly when ready.

[monadius]

@kazk I pushed the docs for mathlib (da66bb8, Lean 3.20.0) to the mathlib_docs repository. Please activate GitHub pages for this repository.

[kazk]

@monadius Thanks. I deployed the pages, but CSS is not found.

Can you regenerate with

./gen_docs -w 'https://codewars.github.io/mathlib_docs/'

[monadius]

I updated my local version of documents. git is very slow for this repository (it took more than 10 hours to commit and push yesterday). I will push all changes overnight.

[kazk]

That's terrible. How many files are there?

Maybe we can generate in GitHub Actions just before publishing. I guess we can have a file specifying the version of mathlib, and trigger a job to build and publish when that changes.

[monadius]

More than 250,000 files. Most files are in the directory find (it contains a separate file for each definition). We are not going to update docs too often. So I don't think that slow git is a serious issue.

[kazk]

How long does it take to generate? 10 hours to commit and push a static site is dumb. This will get worse as we update too unless we overwrite the history each time.

I don't think automation based on a version file will be difficult, but another way is to commit a compressed tarball and extract it before building the pages.

[monadius]

It is pretty fast to generate the docs (about 20 minutes). The official documentation site uses GitHub Actions for building and uploading docs and the docs are updated several times a day. Probably, we can use the existing actions and scripts from the doc-gen repository (https://github.com/leanprover-community/doc-gen/blob/master/deploy_docs.sh and https://github.com/leanprover-community/doc-gen/tree/master/.github/workflows).

[monadius]

I updated the documentation site (https://codewars.github.io/mathlib_docs) and it is usable now.