## Stream: general

### Topic: please minimize tactic changes

#### 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...

#### Kenny Lau (Feb 01 2019 at 11:32):

particularly the file tactic.interactive

#### Kenny Lau (Feb 01 2019 at 11:32):

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

#### 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

#### Kenny Lau (Feb 01 2019 at 11:38):

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

#### 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

#### Kenny Lau (Feb 01 2019 at 11:42):

I said minimize, not avoid.

#### 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

#### 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

#### 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.

#### 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...

#### Kenny Lau (Feb 01 2019 at 11:44):

Have you clicked on the link above?

#### Mario Carneiro (Feb 01 2019 at 11:46):

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

#### 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

#### 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.

#### Mario Carneiro (Feb 01 2019 at 12:06):

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

#### Mario Carneiro (Feb 01 2019 at 12:07):

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

#### 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.

#### 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

#### 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

#### 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