Zulip Chat Archive

Stream: new members

Topic: import Mathlib.Tactic issues

Newell Jensen (Dec 20 2023 at 00:57):

When I put import Mathlib.Tactic at the top of Mathlib.Algebra.Order.Field.Basic I am getting errors where virtually all of the files contents are saying 'BLAH' has already been declared/aligned. I haven't been able to figure out why this is causing issues and wondering if there are some files in Mathlib that you just can't use import Mathlib.Tactic? I suspect it might be some sort of import cycle issue? If so, how does one verify that this is the case?

I am on commit ea02b9e2f48c3b5d2d9bd8208f25276ad4af7915.

Kevin Buzzard (Dec 20 2023 at 01:08):

Indeed I think that in all files in mathlib you can't put import Mathlib.Tactic, with the one exception being Mathlib.lean. The point of that file is to make teaching and writing other projects easier. If there is any tactic which uses ordered fields then it will definitely cause an inport loop.

Newell Jensen (Dec 20 2023 at 01:10):

So how does one get the tactics like rw? and apply? in this file? Reason I even put import Mathlib.Tactic at the top was because these showed up as unknown tactic when trying to use them. Usually within Mathlib I have access to the main tactics but I noticed in this file I don't.

Kevin Buzzard (Dec 20 2023 at 01:11):

You don't want those tactics imported in that file because you can't use those tactics in mathlib files.

Kevin Buzzard (Dec 20 2023 at 01:12):

Just make a scratch file, import whatever you like there, finish your proofs and then move them into the mathlib file.

Patrick Massot (Dec 20 2023 at 01:13):

You can also import the file defining the tactics.

Kevin Buzzard (Dec 20 2023 at 01:13):

But you might want to remove the import when you're done, if you do it that way. Right click on the tactic in a scratch file to find out where it's defined.

Newell Jensen (Dec 20 2023 at 01:19):

I am able to access tactics such as apply? in other Mathlib files and was surprised not to see them in this file, which led to the import attempt. How is it that this file doesn't have apply? but say Mathlib.GroupTheory.PresentedGroup does? I would suspect that this is set somewhere.

Richard Copley (Dec 20 2023 at 01:41):

Take a look at Mathlib.Tactic.Common, and the comment at the top near the bottom of it.

Patrick Massot (Dec 20 2023 at 02:38):

You can go to a file where a tactic work and Ctrl-click the tactic name.

Last updated: Dec 20 2023 at 11:08 UTC