Zulip Chat Archive

Stream: general

Topic: please minimize tactic changes


view this post on Zulip Kenny Lau (Feb 01 2019 at 11:31):

Please minimize tactic changes as it requires the recompiling of essentially the whole mathlib, so the cache is essentially useless, which would cause quite some inconvenience...

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:32):

particularly the file tactic.interactive

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:32):

AFAICT it takes travis ~ 1 hour to compile the whole mathlib

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:38):

@Rob Lewis What are L349 and L480 doing here? https://github.com/leanprover-community/mathlib/commit/c9e4f8edc30da76ffa740000957e26aaf79cc31e

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:38):

(no, don't add another commit to delete those lines, just keep them there)

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:41):

Kenny, I'm not sure what your goal is here. Some things invalidate the cache, it's a fact of life. The solution is to make caching better or more precise, not to avoid improvements

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:42):

I said minimize, not avoid.

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:43):

So for example we can discuss the details before making changes in order to not generate a situation where A made changes and B is unhappy and then make more changes and then C comes along and make 10 more changes

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:43):

sure, but tactic changes require some iteration to get right anyway. I assume it's in a branch, so that's the right place for it

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:44):

And also we can double check the changes before pushing it to mathlib to make sure that it doesn't contain extra lines.

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:44):

sure, but tactic changes require some iteration to get right anyway. I assume it's in a branch, so that's the right place for it

it's in the master branch...

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:44):

Have you clicked on the link above?

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:46):

there are obviously some commented trace lines that were added. They can be removed

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:49):

but it's absolutely the wrong idea to change commit or PR habits for worry of recompilation. Problems that need fixing should be fixed

view this post on Zulip Kevin Buzzard (Feb 01 2019 at 12:04):

I am the anti-Kenny on this one. What is the hurry? Who cares if something takes an hour to compile? It will take less than an hour next year. Kenny just needs a better computer, that's the real problem. We can't change our behaviour to work around the fact that Kenny needs a better computer.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 12:06):

also it's an hour of Travis's time, not mine

view this post on Zulip Mario Carneiro (Feb 01 2019 at 12:07):

(thanks travis for your donation of significant computing time to FOSS projects)

view this post on Zulip Joe Hendrix (Feb 02 2019 at 03:33):

I definitely consider imports and impact of frequent changes on compilation in developing Haskell. Like I'll think about partitioning a module if part of it changes frequently, but modules that import it tend to only need the stable parts.
That said, you shouldn't hold off deleting dead code just to avoid recompiling a module.

view this post on Zulip Simon Hudon (Feb 02 2019 at 03:49):

mathlib could definitely stand to be divided more finely and its dependencies need to be disentangled. But we don't have a warning on spurious imports. We need to build a tool for that

view this post on Zulip Kenny Lau (Feb 02 2019 at 03:51):

I think someone can produce an import graph... I don't know enough programming to do that

view this post on Zulip Simon Hudon (Feb 02 2019 at 03:53):

Mario wrote a parser for olean files. I think that will be a good starting point. It's on my todo list


Last updated: May 10 2021 at 19:16 UTC