website GHA CI recommendation

Stream: mathlib4

[Josha Dekker]

Yesterday I made a project that depends on Mathlib, where I copied the lean_build.yml and upgrade_lean.yml files from the community website. However, I get an error that these are deprecated and I should update to Node.js 20... How do I do that? The first file looks like this:

on:
    push:

jobs:
    update_lean_xyz_branch_and_build:
        runs-on: ubuntu-latest
        name: Update lean-x.y.z branch and build project
        steps:

        - name: checkout project
          uses: actions/checkout@v2
          with:
            fetch-depth: 0

        - name: update branch
          if: github.ref == 'refs/heads/master'
          uses: leanprover-contrib/update-versions-action@master

        - name: build project
          uses: leanprover-contrib/lean-build-action@master

[Patrick Massot]

I think those are both obsolete tools from the Lean 3 era. Where did you find mentions of those?

[Mario Carneiro]

Do we have .yml suggestions for projects depending on mathlib4?

[Josha Dekker]

This page : https://leanprover-community.github.io/install/project.html has a header "Hosting your project on GitHub"
which leads me to https://leanprover-community.github.io/ci.html, where I found the scripts. What is the correct tooling now? (I'm interested in keeping Mathlib up to date in https://github.com/JADekker/PiBaseTracking, as the sole purpose of the repository is to keep track of progress of Mathlib for topology results.

[Patrick Massot]

Thanks Josha, I will nuke the second web page (note it starts with a big banner saying it is obsolete). And I will remove the corresponding sentence of the first page.

[Patrick Massot]

The answer to you question is that we don’t have replacement tools for Lean 4 yet. I guess this is meant to be part of the the reservoir project (see Mac Malone’s Lean Together talk).

[Josha Dekker]

Patrick Massot said:

Thanks Josha, I will nuke the second web page (note it starts with a big banner saying it is obsolete). And I will remove the corresponding sentence of the first page.

Yes, I saw the banner, but I couldn't find similar tools, so I figured I'd copy them and try them anyway. Thank you!

[Ruben Van de Velde]

The banner could perhaps be clearer that actually this specific page is out of date

[Mario Carneiro]

I think we don't need replacement tools exactly, we just need someone to create a template github actions file based on any of the existing lean 4 projects that use CI

[Mario Carneiro]

wrapping it up as a github action like https://github.com/leanprover-contrib/lean-build-action would be nice but IMO is not required for the purposes of the website, since it suggests a complete .yml file anyway

[Mario Carneiro]

ideally this is something lake new itself would be doing, although I'm not sure how tied to github it wants to be

[Patrick Massot]

I just removed three pages. It would be really nice to try to port more pages. For instance I didn’t remove the page about simp because it used to be the most complete resource about it. One day the Lean reference manual will replace this, but in the mean time updating that webpage would be really nice.

[Yaël Dillies]

(deleted)

[Ruben Van de Velde]

Is there a list of pages that need porting? Maybe that would help moving it forward

[Mario Carneiro]

Removing the file with the .yml in it is not sufficient since if people look for one they will find one, and not the one you want them to find

[Notification Bot]

15 messages were moved here from #mathlib4 > Deprecated Node.js actions by Mario Carneiro.

[Patrick Massot]

Ruben:

leanprover-community.github.io$ rg -l transitional
templates/extras/conv.md
templates/extras/calc.md
templates/extras/well_founded_recursion.md
templates/extras/tactic_writing.md
templates/extras/simp.md
templates/glossary.md
templates/theories/category_theory.md
templates/theories/linear_algebra.md
templates/theories/sets.md
templates/theories/naturals.md
templates/theories/topology.md
templates/lean_projects.html
templates/theories.md

[Patrick Massot]

I see there are more candidates for immediate removal.

[Mario Carneiro]

I don't think any pages should be removed unless there is really no equivalent for them

[Patrick Massot]

The well founded recursion page for instance. I don’t see how to update it without copy-pasting Joachim’s blog post.

[Patrick Massot]

And the theories files are probably super obsolete and a much nicer solution is to make sure their content is covered in MIL.

[Mario Carneiro]

Patrick Massot said:

The well founded recursion page for instance. I don’t see how to update it without copy-pasting Joachim’s blog post.

from what I can see you can literally just recapitalize things and fix syntax and that page is still correct, except for the last section (which actually is also just a syntax change)

[Patrick Massot]

https://leanprover-community.github.io/lean_projects.html may be already completely superseded by reservoir, even in its current state.

[Jireh Loreaux]

#mil also has the advantage that it will likely be updated more frequently than the website.

[Patrick Massot]

Mario Carneiro said:

Patrick Massot said:

The well founded recursion page for instance. I don’t see how to update it without copy-pasting Joachim’s blog post.

from what I can see you can literally just recapitalize things and fix syntax and that page is still correct, except for the last section (which actually is also just a syntax change)

But would this be better than Joachim’s blog post?

[Patrick Massot]

Anyway, anyone is welcome to update this page. I cannot do it because I never used well-founded recursion.

[Eric Wieser]

Mario Carneiro said:

wrapping it up as a github action like https://github.com/leanprover-contrib/lean-build-action would be nice but IMO is not required for the purposes of the website, since it suggests a complete .yml file anyway

I think @Julian Berman's https://github.com/Julian/setup-lean either fits the bill, or can be adapted to

[Julian Berman]

(I am of course quite happy to make tweaks to that, or of course to merge any -- it's obviously completely simple and yet still useful.)

[Eric Wieser]

I guess the main question is whether we want to have the lean3 shim inside it any more

[Eric Wieser]

If we drop that, presumably we can also drop the python step?

[Julian Berman]

Yeah that's trivial to remove, it's there essentially because lean.nvim still has (frozen) support for Lean 3 but I can fix that there.

[Eric Wieser]

Or maybe just have a branch/tag of the action with lean3 support