[Merged by Bors] - chore(*): reduce imports #3235

semorrison · 2020-06-30T03:02:57Z

The RFC pull request simply removes some import tactic or import tactic.basic, and then makes the necessary changes in later files to import things as needed.

I'm not sure if it's useful or not --- the reason I did it was to try to make life a bit easier while working on tactics/ files, to reduce the recompilation load. On the other hand, maybe people like the simplicity of always having import tactic.basic done as early as possible, even if it is a slight bottleneck in compilation.

I have a slight preference to make changes in this direction, but am happy to be overrruled.

urkud · 2020-06-30T03:46:22Z

You can always use the new --old argument.

jcommelin · 2020-06-30T03:52:46Z

@semorrison I understand where you are coming from, but as user I would rather have import tactic available asap, so that I can forget about it.
I guess we need to find a balance (-;
(The same is true to some extent for other "regular" library imports, of course.)

semorrison · 2020-06-30T04:40:32Z

Nothing of course is preventing you using import tactic.basic and import tactic in any new file (or adding it to any file you're working on).

Certainly import tactic has not generally already been imported in mathlib --- I think I actually removed the only two or three instances here, which were already off in leaves of mathlib. So the question is whether to import tactic.basic early or not.

PatrickMassot · 2020-06-30T10:06:16Z

If this makes the life of tactic writers easier then I vote yes, despite the inconvenience of breaking the flow of working on some file when you suddenly need to go up and add a tactic import.

gebner · 2020-06-30T10:23:05Z

I'm not sure if it's useful or not --- the reason I did it was to try to make life a bit easier while working on tactics/ files, to reduce the recompilation load. On the other hand, maybe people like the simplicity of always having import tactic.basic done as early as possible, even if it is a slight bottleneck in compilation.

For this particular use case, you can also add --old as an extra command-line argument. (Then you can also comfortably hack on tactic.core.)

semorrison · 2020-06-30T10:32:13Z

I guess --old hasn't really done it for me; I like just being able to work in VSCode, and I'm hesitant to modify the path settings there.

gebner · 2020-06-30T10:35:56Z

You need to set it under Lean: Extra Options in the settings. And yes, it just works in vscode.

test/library_search/ordered_ring.lean

robertylewis · 2020-06-30T12:17:44Z

I have a slight preference to make changes in this direction, but am happy to be overrruled.

I think this sums up my preferences too. import tactic is fine if you're using mathlib as a dependency. For library development, there are (minor) gains in having a more refined import hierarchy.

robertylewis · 2020-06-30T12:20:02Z

Regarding --old, I find myself in this position sometimes: I'm editing a tactic early in the hierarchy, and it fails in a file high in the hierarchy, in a way that's hard to minimize/decouple from the imports. If I change the tactic and want to see the results, I need to recompile everything in between. --old doesn't help me here, right? But a refined import hierarchy would, if the tactic were imported by less in between it and the failing proof.

gebner · 2020-06-30T13:42:39Z

If I change the tactic and want to see the results, I need to recompile everything in between. --old doesn't help me here, right?

This is exactly the use case that --old addresses. For example, I just added a trace message to simpa and could immediately* see it in mfderiv.lean.

*Lean had to recompile mfderiv.lean, but nothing else.

robertylewis · 2020-06-30T13:47:54Z

Then I misunderstood what --old did, and it's more wonderful than I imagined!

PatrickMassot · 2020-06-30T22:37:15Z

It indeed sounds wonderful! Where can we find documentation about that?

semorrison · 2020-06-30T23:46:27Z

--old is indeed awesome. Thanks!

Nevertheless, there's another reason to shrink the import hierarchy (particularly for import tactic and import tactic.basic) which is just that when working on PRs very often one has to merge master during the late stages of development. (Especially if you try to reduce the load on reviewers by making multiple small PRs.) Merging master very often changes the tactic imports, and in this case --old doesn't save you anything. (Of course you can wait for olean from CI, but 🤺 isn't always a good solution.)

test/library_search/ordered_ring.lean

robertylewis · 2020-07-02T11:16:16Z

bors merge

The RFC pull request simply removes some `import tactic` or `import tactic.basic`, and then makes the necessary changes in later files to import things as needed. I'm not sure if it's useful or not Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2020-07-02T12:23:05Z

Build failed (retrying...):

Build mathlib

The RFC pull request simply removes some `import tactic` or `import tactic.basic`, and then makes the necessary changes in later files to import things as needed. I'm not sure if it's useful or not Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2020-07-02T13:05:09Z

Build failed:

Build mathlib

semorrison · 2020-07-03T00:58:17Z

bors merge

The RFC pull request simply removes some `import tactic` or `import tactic.basic`, and then makes the necessary changes in later files to import things as needed. I'm not sure if it's useful or not Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

bors · 2020-07-03T02:21:20Z

Pull request successfully merged into master.

Build succeeded:

Following on from #3256 and #3235, this slices a little out of `data.fintype.basic`, and reduces imports, mostly in the vicinity of `data.fintype.basic`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

#3333) As discussed on [zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/import.20refactor.20and.20library_search), #3235 had the unfortunate effect of making `library_search` and `#where` and various other things unavailable in many places in mathlib. This PR makes an effort to import `tactic.basic` as early as possible, while otherwise reducing unnecessary imports. 1. import `tactic.basic` "as early as possible" (i.e. in any file that `tactic.basic` doesn't depend on, and which imports any tactic strictly between `tactic.core` and `tactic.basic`, just `import tactic.basic` itself 2. add `tactic.finish`, `tactic.tauto` and `tactic.norm_cast` to tactic.basic (doesn't requires adding any dependencies) 3. delete various unnecessary imports Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

The RFC pull request simply removes some `import tactic` or `import tactic.basic`, and then makes the necessary changes in later files to import things as needed. I'm not sure if it's useful or not Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

…unity#3319) Following on from leanprover-community#3256 and leanprover-community#3235, this slices a little out of `data.fintype.basic`, and reduces imports, mostly in the vicinity of `data.fintype.basic`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

leanprover-community#3333) As discussed on [zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/import.20refactor.20and.20library_search), leanprover-community#3235 had the unfortunate effect of making `library_search` and `#where` and various other things unavailable in many places in mathlib. This PR makes an effort to import `tactic.basic` as early as possible, while otherwise reducing unnecessary imports. 1. import `tactic.basic` "as early as possible" (i.e. in any file that `tactic.basic` doesn't depend on, and which imports any tactic strictly between `tactic.core` and `tactic.basic`, just `import tactic.basic` itself 2. add `tactic.finish`, `tactic.tauto` and `tactic.norm_cast` to tactic.basic (doesn't requires adding any dependencies) 3. delete various unnecessary imports Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

chore(*): reduce imports

a7f5c17

semorrison added the RFC Request for comment label Jun 30, 2020

semorrison added 3 commits June 30, 2020 14:42

fix tests

7412267

merge

71f8fbf

fix

6861902

fix tests

061557b

robertylewis reviewed Jun 30, 2020

View reviewed changes

test/library_search/ordered_ring.lean Outdated Show resolved Hide resolved

semorrison commented Jun 30, 2020

View reviewed changes

test/library_search/ordered_ring.lean Outdated Show resolved Hide resolved

semorrison added 2 commits July 1, 2020 09:47

Update test/library_search/ordered_ring.lean

0d0054f

merge

5179058

semorrison added awaiting-review The author would like community review of the PR and removed RFC Request for comment labels Jul 1, 2020

semorrison added 3 commits July 2, 2020 12:04

fix

9f7c707

Merge remote-tracking branch 'origin/master' into reduce_imports

ba6298b

fix

436a81c

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 2, 2020

github-actions bot removed the awaiting-review The author would like community review of the PR label Jul 2, 2020

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Jul 2, 2020

robertylewis and others added 2 commits July 2, 2020 16:40

Merge branch 'master' into reduce_imports

3b41a10

fix

275c7de

semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 3, 2020

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 3, 2020

bors bot changed the title ~~chore(*): reduce imports~~ [Merged by Bors] - chore(*): reduce imports Jul 3, 2020

bors bot closed this Jul 3, 2020

bors bot deleted the reduce_imports branch July 3, 2020 02:21

semorrison mentioned this pull request Jul 8, 2020

[Merged by Bors] - chore(data/fintype/basic): split, and reduce imports #3319

Closed

semorrison mentioned this pull request Jul 9, 2020

[Merged by Bors] - chore(*): import tactic.basic as early as possible, and reduce imports #3333

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(*): reduce imports #3235

[Merged by Bors] - chore(*): reduce imports #3235

semorrison commented Jun 30, 2020

urkud commented Jun 30, 2020

jcommelin commented Jun 30, 2020

semorrison commented Jun 30, 2020

PatrickMassot commented Jun 30, 2020

gebner commented Jun 30, 2020

semorrison commented Jun 30, 2020

gebner commented Jun 30, 2020

robertylewis commented Jun 30, 2020

robertylewis commented Jun 30, 2020

gebner commented Jun 30, 2020 •

edited

Loading

robertylewis commented Jun 30, 2020

PatrickMassot commented Jun 30, 2020

semorrison commented Jun 30, 2020

robertylewis commented Jul 2, 2020

bors bot commented Jul 2, 2020

bors bot commented Jul 2, 2020

semorrison commented Jul 3, 2020

bors bot commented Jul 3, 2020

[Merged by Bors] - chore(*): reduce imports #3235

[Merged by Bors] - chore(*): reduce imports #3235

Conversation

semorrison commented Jun 30, 2020

urkud commented Jun 30, 2020

jcommelin commented Jun 30, 2020

semorrison commented Jun 30, 2020

PatrickMassot commented Jun 30, 2020

gebner commented Jun 30, 2020

semorrison commented Jun 30, 2020

gebner commented Jun 30, 2020

robertylewis commented Jun 30, 2020

robertylewis commented Jun 30, 2020

gebner commented Jun 30, 2020 • edited Loading

robertylewis commented Jun 30, 2020

PatrickMassot commented Jun 30, 2020

semorrison commented Jun 30, 2020

robertylewis commented Jul 2, 2020

bors bot commented Jul 2, 2020

bors bot commented Jul 2, 2020

semorrison commented Jul 3, 2020

bors bot commented Jul 3, 2020

gebner commented Jun 30, 2020 •

edited

Loading