Zulip Chat Archive

Stream: general

Topic: New lean release?

Yury G. Kudryashov (Oct 28 2021 at 19:30):

It would be nice to have a new Lean release. I want to review docs#stream API, and the first step is moving it to mathlib, see #9988.

Johan Commelin (Oct 28 2021 at 19:33):

cc @Gabriel Ebner

Bryan Gin-ge Chen (Oct 28 2021 at 19:54):

I can also make a release later tonight if Gabriel isn't already working on one.

Bryan Gin-ge Chen (Oct 28 2021 at 22:57):

I'm starting to put together Lean 3.35.0c now...

Bryan Gin-ge Chen (Oct 28 2021 at 23:59):

@Yury G. Kudryashov The linux build of Lean 3.35.0c just appeared, so you should be able to use it in mathlib CI now. (The other binaries should appear shortly.)

Yury G. Kudryashov (Oct 29 2021 at 00:13):

Should I resurrect rbtree/rbmap files in mathlib?

Yury G. Kudryashov (Oct 29 2021 at 00:15):

@Scott Morrison :up:

Yury G. Kudryashov (Oct 29 2021 at 02:43):

(in progress)

Scott Morrison (Oct 29 2021 at 06:41):

Sorry, I was away from the computer today. I can help with the mathlib PR for the next release starting in +13 hours.

Yury G. Kudryashov (Oct 29 2021 at 08:34):

It builds but there are many lint errors. I think that we should just add lines to nolints and fix new lint errors later. E.g., this way the changes will be visible in the git history.

Yury G. Kudryashov (Oct 29 2021 at 15:23):

I've opened #10036 for lint fixes.

Yury G. Kudryashov (Oct 29 2021 at 15:24):

Feel free to fix more lint issues. Please don't make larger changes in the same branch.

Eric Wieser (Oct 29 2021 at 15:55):

DO you still intend to just nolints.txt everything in #9988 so that we can merge it?

Yury G. Kudryashov (Oct 29 2021 at 15:57):

Yes. I started lean --run scripts/lint_mathlib.lean locally. It is silent for more than an hour. Is it OK or I'm doing something wrong?

Eric Wieser (Oct 29 2021 at 15:58):

I would just copy the lint output in manually, probably

Yury G. Kudryashov (Oct 29 2021 at 15:59):

htop says that this process uses 370% CPU, so let's wait.

Eric Wieser (Oct 29 2021 at 16:02):

Perhaps github CI should upload the nolints file on failure?

Bryan Gin-ge Chen (Oct 29 2021 at 16:12):

Not a bad idea!

Rob Lewis (Oct 29 2021 at 16:54):

@Floris van Doorn needed to do this a little while back and posted directions in the maintainer stream. Here's his post, slightly cropped:

The CI already generates the nolints.txt file, so you only have to tell it to upload the result. To do this, in the file .github/workflows/build.yml.in add the following:

      - name: upload nolints.txt
        if: always()
        uses: actions/upload-artifact@v2
        with:
          name: nolints.txt
          path: nolints.txt

Add this under the following existing lines (on line 130, currently):

      - name: lint
        run: |
          ./scripts/mk_all.sh
          lean --run scripts/lint_mathlib.lean

Then run .github/workflows/mk_build_yml.sh and commit & push the result.
After CI is done, you can download the file from the CI summary page (e.g. https://github.com/leanprover-community/mathlib/actions/runs/1142305734)

Eric Wieser (Oct 29 2021 at 17:10):

You can do slightly better than always() and only do it if the linting fails; I think I did something like that on the highlightjs-lean repo.

Floris van Doorn (Oct 29 2021 at 18:09):

I think it makes sense to permanently change the CI so that it always uploads the nolints.txt if the linter has run but fails, as Eric said.

Yury G. Kudryashov (Oct 29 2021 at 20:04):

#9988 is ready for review (most of it is a code copied from lean core).

Yury G. Kudryashov (Oct 29 2021 at 20:31):

And CI is happy (since I've added all new errors to nolints).

Eric Wieser (Oct 29 2021 at 21:56):

LGTM, would just like to see some comment about the choice of init.lean as a filename

Yaël Dillies (Oct 29 2021 at 21:59):

Oh yeah I don't like the filenames.

Eric Wieser (Oct 29 2021 at 22:00):

I think they're fine if associated with a TODO or explanation

Eric Wieser (Oct 29 2021 at 22:00):

Just in order to get lean bumped

Yaël Dillies (Oct 29 2021 at 22:00):

YEah sure, I'm just gonna dump my ideas here and you do whatever you want with it.

Yaël Dillies (Oct 29 2021 at 22:01):

I would rename data.rbmap.default, data.rbtree.init,data.rbtree.main and data.stream.init because they are very non descriptive names and .default is reserved to contentless files.

Yaël Dillies (Oct 29 2021 at 22:04):

And I think we could merge data.rbtree.default_lt with any basic order file or something

Yaël Dillies (Oct 29 2021 at 22:05):

Also sad that style_exceptions is getting back up :sad:

Yury G. Kudryashov (Oct 30 2021 at 02:00):

I'm fixing most of lint issues (all but "docs missing") in another PR.

Yury G. Kudryashov (Oct 30 2021 at 02:01):

About file renames and merges: I think that we should do it in separate PRs after we move files to mathlib.

Last updated: Dec 20 2023 at 11:08 UTC