Zulip Chat Archive

Stream: general

Topic: olean-rs on Travis is verbose


view this post on Zulip 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?

view this post on Zulip Simon Hudon (May 02 2019 at 12:23):

Does it matter?

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 02 2019 at 12:30):

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

view this post on Zulip Johan Commelin (May 02 2019 at 12:49):

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

view this post on Zulip Simon Hudon (May 02 2019 at 12:50):

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

view this post on Zulip Simon Hudon (May 02 2019 at 17:39):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 03 2019 at 10:15):

I can confirm this works nicely now!

view this post on Zulip 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)

view this post on Zulip Scott Morrison (May 03 2019 at 11:02):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 03 2019 at 11:03):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 03 2019 at 11:31):

import optimization on every commit is silly

view this post on Zulip Patrick Massot (May 03 2019 at 11:32):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2019 at 11:34):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 11:35):

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

view this post on Zulip Johan Commelin (May 03 2019 at 11:35):

Should I try to do that?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 11:36):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 11:36):

stuff like indentation would be a better test

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2019 at 11:38):

#973

view this post on Zulip Johan Commelin (May 03 2019 at 11:38):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 11:39):

you should usually test travis changes first, let it run

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 03 2019 at 11:40):

Travis could feel we are rebelling, and reject the commit

view this post on Zulip Mario Carneiro (May 03 2019 at 11:40):

isn't it [ci-skip]?

view this post on Zulip Johan Commelin (May 03 2019 at 11:40):

Next time I'll add both (-;

view this post on Zulip Patrick Massot (May 03 2019 at 11:41):

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

view this post on Zulip Patrick Massot (May 03 2019 at 11:41):

no dash

view this post on Zulip Patrick Massot (May 03 2019 at 11:42):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2019 at 12:15):

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

view this post on Zulip Johan Commelin (May 03 2019 at 12:17):

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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 03 2019 at 16:29):

I'm not happy about disabling this check

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 03 2019 at 16:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 03 2019 at 17:07):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 03 2019 at 17:31):

Ok, I'll work on that

view this post on Zulip Johan Commelin (May 03 2019 at 17:31):

Thank you so much!

view this post on Zulip Simon Hudon (May 03 2019 at 17:38):

:+1:

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 21:26):

what about endpoint theorems? What is necessary by fiat?

view this post on Zulip Mario Carneiro (May 03 2019 at 21:26):

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

view this post on Zulip Simon Hudon (May 03 2019 at 21:39):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 21:50):

right, that's my point

view this post on Zulip Mario Carneiro (May 03 2019 at 21:50):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 03 2019 at 21:52):

What information would you get from that list?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 03 2019 at 21:55):

What difference did it make?

view this post on Zulip Mario Carneiro (May 03 2019 at 21:56):

Huh? No difference, lean doesn't care

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 03 2019 at 21:56):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 03 2019 at 21:57):

Ah ok

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 21:58):

we could pick that convention up again

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 03 2019 at 21:59):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 21:59):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 22:01):

I try to reliably name my actual lemmas *_aux

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 03 2019 at 22:04):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 03 2019 at 22:05):

I'm in the same boat.

view this post on Zulip Simon Hudon (May 03 2019 at 22:05):

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

view this post on Zulip Simon Hudon (May 03 2019 at 22:06):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 22:07):

I don't think it really does

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 22:09):

forget private

view this post on Zulip Simon Hudon (May 03 2019 at 22:09):

That's reasonable

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 22:10):

olean-rs should be able to do this much

view this post on Zulip Simon Hudon (May 03 2019 at 22:10):

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

view this post on Zulip Simon Hudon (May 03 2019 at 22:11):

To do how much?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2019 at 22:15):

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

view this post on Zulip Simon Hudon (May 03 2019 at 22:17):

How does that make things better?

view this post on Zulip 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