What is the latest working (lean, mathlib) pair?

Stream: general

[Ching-Tsun Chou]

A pair of git commit ids would suffice.

Thanks!

[Simon Hudon]

I haven't had much success updating in the last couple of days so I'm using:

Lean: 07bb7d809b6be49f38ce4e427c54a82708ae281f
mathlib: f7977ff5a6bcf7e5c54eec908364ceb40dafc795

It's from about 10 days ago and it doesn't include the latest monad changes

[Ching-Tsun Chou]

Thanks! I'll give them a try.

I wonder if the maintainer of mathlib (Mario?) can keep a record of which mathlib git commit matches which lean commit. All that is needed is a lean commit id in the mathlib commit messages.

[Mario Carneiro]

I'm checking out the last nightly (28f414) and I'll revert mathlib to work with it instead of HEAD, at least until the issues on lean repo are fixed

[Simon Hudon]

It's a bit unusual for Lean and mathlib to be broken for this long. Normally, Mario keeps it working with the nightly build

[Ching-Tsun Chou]

It doesn't really matter how long they are broken. All we need is a record of which lean commit works with which mathlib commit. The user can compile lean him/herself. Thanks!

[Mario Carneiro]

I usually keep it working with HEAD, and it doesn't make a big difference from nightly after a day

[Mario Carneiro]

Usually leo is careful not to push a broken build, and certainly not leave it for several days like that

[Simon Hudon]

I think they might be preparing for Lean 4

[Ching-Tsun Chou]

Well, you guys would not have needed to spend the time to answer my questions if there is a record which I can look up myself.

[Mario Carneiro]

The record is the relative commit times

[Ching-Tsun Chou]

How do I find out what is the commit id of the latest lean nightly build? The lean-nightly at https://leanprover.github.io/download/ currently points to something that is 3 weeks old (d6d44a19947e ). The lean commit history does not say which commits are used in nightly builds.

[Mario Carneiro]

The nightly build process is soon to change, with a better record of all this, but currently you can go to https://github.com/leanprover/lean-nightly/tree/gh-pages and look at the commit that "bot botson" says in the commit message

[Mario Carneiro]

I pushed a version of mathlib that works with it, so hopefully we will see the travis :thumbs_up: soon

[Simon Hudon]

That latest commit is about making it work with the latest nightly instead of HEAD, is that correct?

[Mario Carneiro]

yes