olean-rs on Travis is verbose

Stream: general

[Johan Commelin]

Currently the Travis log is very verbose when it starts checking that dependencies are minimal: https://travis-ci.org/leanprover-community/mathlib/jobs/527147591
Do we want this, or should we instruct the Makefile to be a bit more silent?

[Simon Hudon]

Does it matter?

[Johan Commelin]

Well... it means you have to scroll down a long time before you see the error. But I guess that's why there is an End key on my keyboard :sweat_smile:

[Johan Commelin]

Same topic, different question: @Simon Hudon can we make the output more helpful? https://travis-ci.org/leanprover-community/mathlib/jobs/527258584

[Johan Commelin]

Travis is complaining that the import is unused. But it is the only import, so I surely can't just remove it. Can the script explain what is the "correct" set of imports?

[Johan Commelin]

I feel like a lot of PRs are going to stumble over this new check, unless we provide people with the tools to quickly fix their imports to the required minimum.

[Simon Hudon]

I have that feature, it's not released yet but I can release it

[Johan Commelin]

@Simon Hudon Does releasing it mean that Travis automatically picks it up?

[Simon Hudon]

It does but I haven't tested it yet so I have to do that first

[Simon Hudon]

Check out https://travis-ci.org/leanprover-community/mathlib/jobs/527258584

[Simon Hudon]

If you install olean-rs locally, you can run the test before committing. I set it up to make it easier to check and recheck if you fix anything

[Scott Morrison]

I can confirm this works nicely now!

[Scott Morrison]

Actually, sometimes it suggests too much. e.g. https://travis-ci.org/leanprover-community/mathlib/jobs/527683532 told me

* unused imports for algebraic_geometry.presheaf
category_theory.natural_isomorphism
  - replace with
       import category_theory.functor_category
              category_theory.isomorphism
              tactic.simpa

but in fact none of those three was necessary (presumably because they are already implied by other existing imports)

[Scott Morrison]

I think overall I don't like this as a travis test.

[Scott Morrison]

The PR process is already soul-crushing, and having yet another potential hiccup in the hours long process of waiting until travis is happy is just unbearable.

[Scott Morrison]

I would prefer that we just run olean-rs every couple of months and make a single PR with lots of import fixing.

[Johan Commelin]

@Simon Hudon I think this one at least needs more testing. Can we disable it?

[Johan Commelin]

I would prefer that we just run olean-rs every couple of months and make a single PR with lots of import fixing.

This PR could potentially even be scriptable, right? :wink:

[Scott Morrison]

Yeah... I've just sat through a 45 minute build in order to see a second error message from olean-rs. This step in the PR process basically makes it compulsory for all PR authors to install a local copy of olean-rs, which is not okay.

[Mario Carneiro]

import optimization on every commit is silly

[Patrick Massot]

I wouldn't write "silly", but it certainly sounds like an unconvenient overkill

[Mario Carneiro]

Maybe it would be okay if it was an automatic cleanup, but travis just saying "you weren't optimal, so you lose" is a recipe for stress

[Johan Commelin]

@Mario Carneiro Do you know how to disable the test?

[Mario Carneiro]

just restore the travis.yml to what it was before Simon added the test?

[Johan Commelin]

Should I try to do that?

[Mario Carneiro]

There are other linter warnings we might want to run, but the import test is the only one that's implemented so far

[Mario Carneiro]

and it's not worth interrupting someone's workflow for that

[Mario Carneiro]

stuff like indentation would be a better test

[Johan Commelin]

I guess we need to remove these 4 lines https://github.com/leanprover-community/mathlib/blob/master/.travis.yml#L57-L60

[Johan Commelin]

#973

[Johan Commelin]

@Mario Carneiro should we just merge this? Or should this go through Travis + Mergify?

[Mario Carneiro]

you should usually test travis changes first, let it run

[Patrick Massot]

I would even had instructed Travis to keep away from this commit (using [ci skip] in the commit message)

[Patrick Massot]

Travis could feel we are rebelling, and reject the commit

[Mario Carneiro]

isn't it [ci-skip]?

[Johan Commelin]

Next time I'll add both (-;

[Patrick Massot]

https://docs.travis-ci.com/user/customizing-the-build/#skipping-a-build

[Patrick Massot]

no dash

[Patrick Massot]

Maybe you are confused because [travis-ci skip] is a thing

[Scott Morrison]

I also just got an error message that make unused took longer than 10 minutes: https://travis-ci.org/leanprover-community/mathlib/jobs/527719987

[Johan Commelin]

@Mario Carneiro Does Travis use the .travis.yml of the branch or of master?

[Johan Commelin]

It would be quite unsafe to use the config from the PR branch...

[Johan Commelin]

@Scott Morrison Your life should now be a bit easier again. I've disabled those checks on Travis.

[Simon Hudon]

I'm not happy about disabling this check

[Simon Hudon]

If you run olean-rs on your machine, you can catch those problems. If you don't run it, the back and forth with Travis should catch those issues.

[Simon Hudon]

Otherwise, it becomes someone's job to fix your messes

[Simon Hudon]

It's easy to fix the timeout issue. @Scott Morrison Would it make things better if the problem was reported as soon as the file was built? That's easy to do.

[Johan Commelin]

@Simon Hudon We will need better instructions for PR authors. Most of them haven't even heard of olean-rs. Also... Scott reported false positives by olean-rs. I think that justifies disabling the checks for now. Moreover, if olean-rs could output a sed-script that will automatically fix all my imports, than it's really easy to use. The manual-iterative process is not a good thing.

[Johan Commelin]

The back-and-forth with Travis takes >40 minutes per cycle. That isn't realistically workable.

[Simon Hudon]

I could get script/setup-dev-scripts.py to install olean-rs (and maybe we could rename it to leant)

[Simon Hudon]

As for automatically applying the changes, we're not there yet. It would be an improvement but it is not necessary

[Simon Hudon]

What we can do is get the errors to reported earlier in the build. With travis caching the build, the first file it compiles should be one you changed and we should check it right away so that the build fails quickly if you messed up

[Simon Hudon]

If you don't want to wait for travis to do it, you can do it on your own machine and we can make it easy to install

[Johan Commelin]

We first need to make it easy to install and use. And we need Travis to fail fast. After that, we can enable the check. Currently the community wasn't ready for this check yet.

[Simon Hudon]

Ok, I'll work on that

[Johan Commelin]

Thank you so much!

[Simon Hudon]

:+1:

[Simon Hudon]

How do you guys feel about having olean-rs identify unused lemmas? I'm thinking of having options to declare that some theorems or lemmas are necessary or even whole files

[Mario Carneiro]

what about endpoint theorems? What is necessary by fiat?

[Mario Carneiro]

mathlib has a lot of endpoint theorems because it's a library

[Simon Hudon]

For sure. And there may be a concise way of specifying them

[Mario Carneiro]

that sounds like a lot of labeling. Almost all theorems in mathlib are endpoint theorems, to the extent that you will end up transferring the work to management of the annotations

[Simon Hudon]

Are you sure? When you set off to prove a theorem, do you mostly use the other big theorems that you or other people proved before or the tiny lemmas that surround the definitions that you're using? I feel like the latter is the case

[Mario Carneiro]

right, that's my point

[Mario Carneiro]

the tiny lemmas are just as important if not moreso than the big theorems

[Mario Carneiro]

It might be good to have a list of theorems that are never referenced, but I don't think we will need to do anything about most of them

[Simon Hudon]

What information would you get from that list?

[Mario Carneiro]

you could look at the list and find things that really are internal lemmas, but they don't stick out in any particular way

[Mario Carneiro]

Way back at the start of mathlib I tried to institute the convention that all theorems are called theorems, but then all the mathematicians got involved and want to call these tiny theorems lemmas instead

[Simon Hudon]

What difference did it make?

[Mario Carneiro]

Huh? No difference, lean doesn't care

[Mario Carneiro]

but I don't like meaningless distinctions and there is a bit of information there that is going to waste

[Simon Hudon]

But presumably, you had a reason to want to adopt that convention

[Mario Carneiro]

The rule was that everything is a theorem, unless it is private then it is a lemma

[Simon Hudon]

Ah ok

[Mario Carneiro]

It was my attempt at labeling endpoint theorems, like I said, everything is an endpoint theorem in mathlib

[Mario Carneiro]

we could pick that convention up again

[Simon Hudon]

Would you go so far as to say that there's no such thing as dead code in mathlib?

[Mario Carneiro]

Since lean does not provide any facilities to hide stuff, anything in mathlib is observable

[Mario Carneiro]

But mathlib changes often and some things are more stable than others

[Mario Carneiro]

I try to reliably name my actual lemmas *_aux

[Mario Carneiro]

In principle I should mark them private too but because lean kernel has no built in support for privacy lean elaborator has to do tricks with namespaces that sometimes leak

[Simon Hudon]

I don't suppose finding unused _aux definitions / lemmas is that useful for code review

[Mario Carneiro]

However, marking a theorem or def private is a drastic measure, and many times I have found that I want to access that private thing later, so I tend to err on the side of making everything public these days

[Simon Hudon]

I'm in the same boat.

[Simon Hudon]

I never find that something should be private and often find that they shouldn't be

[Simon Hudon]

Actually, I'd be perfectly fine if Lean didn't have a private mechanism

[Mario Carneiro]

I don't think it really does

[Simon Hudon]

It does not hide things completely but it does end up that we don't use private stuff from other modules.

[Mario Carneiro]

How about this: marking something as lemma means it is eligible for cleanup if nothing references it

[Mario Carneiro]

forget private

[Simon Hudon]

That's reasonable

[Simon Hudon]

The problem for automation is that lemma vs theorem does not make it to olean files. I think I have to start looking at the lean files to find issues with PRs

[Mario Carneiro]

olean-rs should be able to do this much

[Simon Hudon]

Actually, maybe I can use the olean files to enforce naming policies

[Simon Hudon]

To do how much?

[Mario Carneiro]

the experimental lean parser doesn't know that much but it knows command keywords so it can tell what the lemmas are

[Mario Carneiro]

But this also has to be paired with some community norm changes re: random use of lemma vs theorem

[Simon Hudon]

That makes sense. We can also couple this kind of check with looking for definitions that are not referenced by other definitions or theorems / lemmas

[Mario Carneiro]

Definitions are harder to clean up. Again, almost every def is expected to be used possibly outside mathlib

[Mario Carneiro]

I don't think there is a better option than checking for use of *_aux

[Simon Hudon]

How does that make things better?

[Simon Hudon]

We could consider definitions to be end-points and report errors if they don't have specifications