Lean Community Fork

Stream: general

[Mario Carneiro]

The fork leanprover-community/lean was recently created. Before we go crazy on it, I would like to have a public discussion on the pros and cons: A list of things we want to do with it, problems that can arise from moving mathlib to compiling on a fork (should we maintain compatibility to 3.4.2?), the possibility of having to give these changes up when lean 4 comes around, and so on. Some of this might involve dredging up old closed PRs from the lean repo for re-evaluation.

We considered and rejected a proposal for a fork last year, when development on 3.4.0 was still ongoing, and we decided that tracking changes in lean would be too difficult if a community fork diverged too much. I think the situation is quite different now, since lean 3 is essentially abandoned while official development (read Leo + Sebastian) has continued on lean 4 in private. My current thoughts are to use a community fork to continue support and development on lean 3, with the understanding that lean 4 may change everything when it eventually comes. I would propose to have mathlib maintain an experimental lean 4 branch during the initial stage after the release, without much serious porting except for proof of concepts, until we are all comfortable enough with it that we think we can leave lean 3, and the fork, behind for good. (We may also want to fork lean 4 but that's a bit far off to plan at this point.)

I think we should probably minimize changes to lean, but I also think that it will be difficult to impossible to maintain compatibility with two lean versions simultaneously - even moving a single theorem from mathlib to core or vice versa causes a mismatch that will cause an error either way around. Pure additions to the C++ code might allow backwards compatibility, but something like a bugfix that we want to take advantage of in mathlib would be prevented by attempts at backward compatibility.

If we decide against using the fork for mathlib, it can still be used as an experimental testing grounds for changes to lean, but in this case backward compatibility would be a bigger problem (unless one is okay with using the experimental branch on its own without mathlib).

Plans are not finalized yet, but I'm hoping that having the fork available for use now will help spark the conversation.

[Edward Ayers]

I can PR my fork of Lean with docstrings.

[Patrick Massot]

I think I won't be really enthusiastic about this before I see a compelling list of things we could do using this fork. Right now it looks like the inconvenience and energy dispersion would be more visible than the benefits. I would rather like to see more maths going into mathlib. And I would really like to see Leo writing that he is happy, or at least doesn't care at all. Having a happy Leo is much more important for the future of Lean than unlocking a couple of definitions that we currently can't change because they are in core Lean.

[Rob Lewis]

I generally agree with Patrick. What's the extent of the changes you'd expect to make on the fork? Small bug fixes (e.g. to some of the tactics we have primed versions of) and name changes wouldn't be so disruptive, but to me there's nothing that's worth the cost of forking.

I think it would be futile to try to maintain backwards compatibility. If we move mathlib to a fork, the temptation to start changing little annoying things in the core library will be too great.

We'd also have to find a better way to synchronize mathlib with forked-Lean releases. Updating to the most recent changes to Lean didn't go 100% smoothly, and presumably there would be more activity on the fork if it happens. I've really enjoyed the stability of Lean versions compared to a few years ago.

It's not possible to handle versions of forked Lean smoothly in elan, is it?

[Reid Barton]

Some suggestions: ignore .olean files without corresponding .lean files; make lean --deps work again; implement #where reliably/without hacks; maybe fix the elaborator bug that affects universes in category theory.

[Reid Barton]

I agree that forking for the purpose of making changes to the core library is not that compelling and probably would cause more headaches than it's worth.

[Scott Morrison]

It's actually very easy to handle forked versions of Lean via elan. "It just works." My student Keeley Hoek provided the patches for elan last year, as he had forked Lean so we could make native calls to libsvm.

[Scott Morrison]

In particular, instead of writing lean_version = "3.4.2" you just write lean_version = "khoek/klean:3.4.4"

[Mario Carneiro]

I think I won't be really enthusiastic about this before I see a compelling list of things we could do using this fork.

Yes, that's partly the reason for this thread.

I would rather like to see more maths going into mathlib.

I am not planning on sinking major time into work on lean core. But I want to provide an outlet for people for whom the inconvenience of a bug or missing feature is sufficiently higher than the inconvenience of learning how to write and test a PR for lean.

And I would really like to see Leo writing that he is happy, or at least doesn't care at all.

My understanding of the recent move of mathlib away from the leanprover account is that Leo doesn't care at all, or more precisely he wants mathlib to be our problem and not his. It's an independent project, and if it is better for us to run a forked version of lean then that's our prerogative. He has also sent clear signals that he doesn't want to be bothered by user problems or be involved in reviewing PRs or what have you, and a fork is the easiest way to achieve both goals (leaving Leo alone and respecting issues and PRs from the community).

What's the extent of the changes you'd expect to make on the fork? Small bug fixes (e.g. to some of the tactics we have primed versions of) and name changes wouldn't be so disruptive, but to me there's nothing that's worth the cost of forking.

Small bug fixes, like incorporating primed versions of tactics, is an easy thing. Another major class of changes involves increasing the API surface area in order to make certain things that are currently impossible possible in lean. So rather than putting #where in lean C++, we add enough hooks so that a lean #where can ask all the questions it needs to ask.

We'd also have to find a better way to synchronize mathlib with forked-Lean releases. Updating to the most recent changes to Lean didn't go 100% smoothly, and presumably there would be more activity on the fork if it happens. I've really enjoyed the stability of Lean versions compared to a few years ago.

This is true. We were clearly out of practice for lean updates and 3.4.2 didn't go as smoothly as expected. We would need to get better at that. Back in the day, mathlib ran on nightly lean releases, until Leo closed up shop. I don't recall there being much problem with that, but I think the community was smaller back then and there weren't so many mathematicians; we need to make sure the tooling is available to make this pain-free or it will only be an inconvenience, like Patrick says.

The line between "stable" and "abandoned" is thin. Of course lean is much more stable now than it was back when Leo made commits to lean repo. But it came at exactly the cost I was worried about back then: monkey patches, workarounds, and rejecting issues with "sorry, you're out of luck".

Some suggestions, based on previous conversations:

• VM overrides. This would require its own thread to discuss in detail, but the basic idea is that you can mark a definition @[vm_override bar] def foo and then the VM will call bar instead of foo. This can be used to make existing VM overrides manifest in the code (they aren't visible right now, which leads to nonlocality of definition where you see a lean definition and it isn't being used and the code says nothing to indicate this), and can also be used to support definitions that compute efficiently in both the kernel and the VM. (I have a ton of applications of this.)
• cached A: maybe the name needs work, I think mutable A might be better. It's a wrapper for trunc A that allows mutation of the contained element. Type theory mumbo jumbo ensures that you can't observe the change of representation.
• User computation rules. The kernel already has support for normalizer_extensions, this is just providing an interface for it. "You could break consistency!" Yes, it's an axiom-like thing. It is not intended for general use but there are some applications where it is necessary.
• Hook for the equation compiler: Using custom recursors in the equation compiler, and providing a way to use equation syntax with a custom equation compiler.
• More tactic API: more pexpr functions, pattern matching on macro_def, custom parser hooks, more direct manipulation of the type context.
• Tracing and timing for #reduce
• Additions and fixes for leanpkg: allow tracking master branch, add extra commands like init-travis for setting up a travis.yml file for your project, probably some other things I've forgotten.
• Bug fixes all around

As you can see it's mostly hooks - I want to minimize the stuff that goes into lean repo and instead just set up the minimum necessary to allow building actual tools in mathlib. Of course each of these needs its own issue / RFC and PR, and we should keep in mind the disruptive effect of each of them when considering whether to merge them, and for many of these no code has been written yet so someone would have to feel strongly enough about them to implement them to get the process started. But at least now we can have the conversation.

In the core library, I am more torn, because of the issues with moving things around and references in dependent projects.

• One of the projects I got most of the way to completion, before leo closed up shop and I quietly dropped it, was a change of discrete_field -> field and eliminating the field class.
• Proof changes should be less disruptive, for example removing AC from the proof that int is a ring.
• Removing notations that aren't used and are blocking better uses, i.e. |> <| >=> and I'm sure you all have some other examples.

[Kenny Lau]

>=> looks like a fish

[Mario Carneiro]

thank haskell for that one

[Edward Ayers]

Does anyone know how to run Lean's unit tests?

[Mario Carneiro]

I think ninja test works

[Edward Ayers]

Works for me:

# in lean dir
mkdir -p build/release
cd build/release
cmake ../../src -G Ninja
ninja
ninja test

[Edward Ayers]

Would there be any interest in adding meta constant float : Type to this fork?

[Mario Carneiro]

Yes please

[Mario Carneiro]

I actually finally have a plan for how to model float in the right way. It will require your meta implementation as a prerequisite, so it's a good starting point

[Edward Ayers]

@Rob Lewis also has an implementation so I'll mention him.

[Rob Lewis]

It's here: https://github.com/robertylewis/lean/tree/floats But as you can see, there's not much to it.

[Simon Hudon]

We now have the first nightly for the community fork: https://github.com/leanprover-community/lean-nightly/releases. There's no version for Windows yet as I'm still figuring out the AppVeyor sorcery.

[Simon Hudon]

It has a couple of fixes (revert, get_cwd, repeated instances in init/algebra/field), improved doc strings for tactics and a few new features:

191a237 feat(tactic/interactive): generalize custom tactic monads in begin ... end blocks (#10)
5f5dcc1 feat(io/serial): add expr serialization/deserialization functions (#6)
00b3161 feat(meta/environment): add_ginductive (#3)

[Keeley Hoek]

there is a lot of added docstring text, thanks @Edward Ayers

[Johan Commelin]

Is there some sort of README or HOWTO for newbies that have no idea how to switch to this Lean version? I guess for new projects you can just feed the correct pointer to elan and it should "just work", right? Is it possible to run mathlib with the new Lean version? What are the expectations that I should have?

[Simon Hudon]

I haven't tested with mathlib yet but I don't think anything will break. As for the README, my next step is making it usable. I'd like to hook it into elan but I'm not sure how yet

[Kevin Buzzard]

Will it have a more succinct name than "the community fork"? Are you allowed to call it "Lean 3.5 (unofficial)", abbreviated to "Lean 3.5"?

[Kevin Buzzard]

Or would this be frowned upon?

[Mario Carneiro]

I think the plan was to add a "c" at the end of the version name

[Simon Hudon]

I was thinking of 3.4.3c (c of community)

[Simon Hudon]

Maybe we should jump up to 3.5c though

[Mario Carneiro]

I think 3.5c is deserved

[Keeley Hoek]

@Johan Commelin literally all you need to do to try it out if you use elan is change your lean_version = ... to lean_version = "leanprover-community/lean:nightly-2019-04-20" in leanpkg.toml, and restart lean in vscode.

[Simon Hudon]

You can also do:

$ elan toolchain install leanprover-community/lean:nightly
$ elan override set nightly

[Simon Hudon]

As of an hour ago, the nightly build is available for Windows

[Kevin Buzzard]

it's 4-20 Lean

[Kevin Buzzard]

Lean plus some extra magic

[Simon Hudon]

Are you insinuating that we were doing drugs while making those changes?

[Kevin Buzzard]

only when you pushed them

[Simon Hudon]

Oh ... much better ... ?

[Kevin Buzzard]

So now there is a risk that future tactics will only work with the fork, right?

[Simon Hudon]

My plan is to keep mathlib working with both versions for a while

[Kevin Buzzard]

So then if I want to run the perfectoid repo off that fork, for some reason (say we run into a bug in lean and you can fix it), I guess I would have to learn the new incantation for making this happen -- this just involves some simple edit to leanpkg.toml right?

[Kevin Buzzard]

And then elan does the rest?

[Simon Hudon]

But at the same time, eventually, I'd like to bring in the new data type package into mathlib and we'll definitely need 3.5 for that to work

[Kevin Buzzard]

o_O

[Simon Hudon]

Yes, that's right

[Kevin Buzzard]

Now there will be a risk that there will be a Lean 3.6 and a Lean 4.0 which are incompatible?

[Kevin Buzzard]

You're talking about this qpf stuff which I don't understand properly?

[Kevin Buzzard]

Will it help me make a perfectoid space?

[Simon Hudon]

There's no question that Lean 4 will be incompatible with what we did with Lean 3

[Simon Hudon]

I don't understand perfectoid spaces so I can't say

[Kevin Buzzard]

What if Leo just decided to troll us and release Lean 4 which was exactly the same as Lean 3.4.2 except for a sexier parser. Oh -- even better -- make it exactly the same except that type class inference is done in a super-cool new way and we have a sexier parser. And they accept PR's. We'd want to upgrade to 4.0 right?

[Simon Hudon]

I'm pretty sure they're passed that now. They've been working on a compiler as well as a parser. That should be substantial

[Kevin Buzzard]

And then we made bug reports and they all got fixed in Lean 4.1

[Kevin Buzzard]

and mathlib 3.4.2 compiled on it.

[Simon Hudon]

No one has made the claim that this is likely and many times, the developers have asserted the opposite.

[Simon Hudon]

Lean 4 will break a lot of things

[Simon Hudon]

it will take a while to port mathlib to Lean 4 and we have to get comfortable with Lean 3 in the meantime. I don't know if we're going to need to support both Lean 3 and Lean 4 for a time or if it's even a possibility

[Kevin Buzzard]

That's crazy. We have a fork. The ramifications are just sinking in. Is Leo OK with this? Presumably there's some licensing issue restrictions on what we can do with the fork. Presumably we can't delete all reference to Leo, for example.

[Keeley Hoek]

It's my feeling that a bunch of the features which have been proposed so far are intended for Lean 4 anyway, like https://github.com/leanprover-community/lean/pull/19, and the bugfixes

[Keeley Hoek]

With respect to licensing the code is under Apache License 2.0 https://github.com/leanprover/lean/blob/master/LICENSE, and we of course must obey its terms (which are really very permissive)

[Simon Hudon]

I have talked to @Sebastian Ullrich about and he seems relieved that we'll handle the bugs from now on.

[Simon Hudon]

Btw, I have arranged a build that checks mathlib with that latest version of Lean: https://travis-ci.org/leanprover-community/mathlib/builds/522599987. For now, it's allowed to fail but I'm making sure to keep a measure of when Lean 3.5 breaks mathlib