## Stream: general

### Topic: olean-rs on Travis is verbose

#### Johan Commelin (May 02 2019 at 08:13):

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?

Does it matter?

#### Johan Commelin (May 02 2019 at 12:26):

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 (May 02 2019 at 12:28):

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

#### Johan Commelin (May 02 2019 at 12:29):

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 (May 02 2019 at 12:30):

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 (May 02 2019 at 12:30):

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

#### Johan Commelin (May 02 2019 at 12:49):

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

#### Simon Hudon (May 02 2019 at 12:50):

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

#### Simon Hudon (May 02 2019 at 17:40):

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 (May 03 2019 at 10:15):

I can confirm this works nicely now!

#### Scott Morrison (May 03 2019 at 11:00):

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 (May 03 2019 at 11:02):

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

#### Scott Morrison (May 03 2019 at 11:02):

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 (May 03 2019 at 11:03):

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 (May 03 2019 at 11:03):

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

#### Johan Commelin (May 03 2019 at 11:04):

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 (May 03 2019 at 11:22):

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 (May 03 2019 at 11:31):

import optimization on every commit is silly

#### Patrick Massot (May 03 2019 at 11:32):

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

#### Mario Carneiro (May 03 2019 at 11:33):

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 (May 03 2019 at 11:34):

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

#### Mario Carneiro (May 03 2019 at 11:35):

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

#### Johan Commelin (May 03 2019 at 11:35):

Should I try to do that?

#### Mario Carneiro (May 03 2019 at 11:36):

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 (May 03 2019 at 11:36):

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

#### Mario Carneiro (May 03 2019 at 11:36):

stuff like indentation would be a better test

#### Johan Commelin (May 03 2019 at 11:37):

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

#973

#### Johan Commelin (May 03 2019 at 11:38):

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

#### Mario Carneiro (May 03 2019 at 11:39):

you should usually test travis changes first, let it run

#### Patrick Massot (May 03 2019 at 11:39):

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

#### Patrick Massot (May 03 2019 at 11:40):

Travis could feel we are rebelling, and reject the commit

#### Mario Carneiro (May 03 2019 at 11:40):

isn't it [ci-skip]?

#### Johan Commelin (May 03 2019 at 11:40):

Next time I'll add both (-;

#### Patrick Massot (May 03 2019 at 11:41):

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

no dash

#### Patrick Massot (May 03 2019 at 11:42):

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

#### Scott Morrison (May 03 2019 at 11:47):

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 (May 03 2019 at 12:15):

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

#### Johan Commelin (May 03 2019 at 12:17):

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

#### Johan Commelin (May 03 2019 at 13:25):

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

#### Simon Hudon (May 03 2019 at 16:29):

I'm not happy about disabling this check

#### Simon Hudon (May 03 2019 at 16:30):

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 (May 03 2019 at 16:30):

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

#### Simon Hudon (May 03 2019 at 16:53):

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 (May 03 2019 at 17:06):

@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 (May 03 2019 at 17:07):

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

#### Simon Hudon (May 03 2019 at 17:20):

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

#### Simon Hudon (May 03 2019 at 17:20):

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

#### Simon Hudon (May 03 2019 at 17:22):

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 (May 03 2019 at 17:23):

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 (May 03 2019 at 17:27):

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 (May 03 2019 at 17:31):

Ok, I'll work on that

#### Johan Commelin (May 03 2019 at 17:31):

Thank you so much!

:+1:

#### Simon Hudon (May 03 2019 at 21:20):

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 (May 03 2019 at 21:26):

what about endpoint theorems? What is necessary by fiat?

#### Mario Carneiro (May 03 2019 at 21:26):

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

#### Simon Hudon (May 03 2019 at 21:39):

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

#### Mario Carneiro (May 03 2019 at 21:44):

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 (May 03 2019 at 21:49):

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 (May 03 2019 at 21:50):

right, that's my point

#### Mario Carneiro (May 03 2019 at 21:50):

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

#### Mario Carneiro (May 03 2019 at 21:52):

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 (May 03 2019 at 21:52):

What information would you get from that list?

#### Mario Carneiro (May 03 2019 at 21:53):

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 (May 03 2019 at 21:54):

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 (May 03 2019 at 21:55):

What difference did it make?

#### Mario Carneiro (May 03 2019 at 21:56):

Huh? No difference, lean doesn't care

#### Mario Carneiro (May 03 2019 at 21:56):

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

#### Simon Hudon (May 03 2019 at 21:56):

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

#### Mario Carneiro (May 03 2019 at 21:57):

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

Ah ok

#### Mario Carneiro (May 03 2019 at 21:57):

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

#### Mario Carneiro (May 03 2019 at 21:58):

we could pick that convention up again

#### Simon Hudon (May 03 2019 at 21:58):

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

#### Mario Carneiro (May 03 2019 at 21:59):

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

#### Mario Carneiro (May 03 2019 at 21:59):

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

#### Mario Carneiro (May 03 2019 at 22:01):

I try to reliably name my actual lemmas *_aux

#### Mario Carneiro (May 03 2019 at 22:02):

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 (May 03 2019 at 22:04):

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

#### Mario Carneiro (May 03 2019 at 22:04):

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 (May 03 2019 at 22:05):

I'm in the same boat.

#### Simon Hudon (May 03 2019 at 22:05):

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

#### Simon Hudon (May 03 2019 at 22:06):

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

#### Mario Carneiro (May 03 2019 at 22:07):

I don't think it really does

#### Simon Hudon (May 03 2019 at 22:08):

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

#### Mario Carneiro (May 03 2019 at 22:09):

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

#### Mario Carneiro (May 03 2019 at 22:09):

forget private

#### Simon Hudon (May 03 2019 at 22:09):

That's reasonable

#### Simon Hudon (May 03 2019 at 22:10):

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 (May 03 2019 at 22:10):

olean-rs should be able to do this much

#### Simon Hudon (May 03 2019 at 22:10):

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

To do how much?

#### Mario Carneiro (May 03 2019 at 22:11):

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

#### Mario Carneiro (May 03 2019 at 22:12):

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

#### Simon Hudon (May 03 2019 at 22:13):

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 (May 03 2019 at 22:15):

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

#### Mario Carneiro (May 03 2019 at 22:15):

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

#### Simon Hudon (May 03 2019 at 22:17):

How does that make things better?

#### Simon Hudon (May 03 2019 at 22:23):

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

Last updated: May 11 2021 at 22:14 UTC