please minimize tactic changes

Stream: general

[Kenny Lau]

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]

particularly the file tactic.interactive

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

I said minimize, not avoid.

[Kenny Lau]

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]

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]

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]

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]

Have you clicked on the link above?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Joe Hendrix]

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]

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]

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

[Simon Hudon]

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