Zulip Chat Archive

Stream: general

Topic: Error in pull request


Sara Díaz Real (Jul 15 2021 at 18:31):

Hello! I have tried to make a pull request and I have found this problem:x-special/nautilus-clipboard
copy
Captura-de-pantalla-de-2021-07-15-20-30-24.png

Can someone help me?

Bryan Gin-ge Chen (Jul 15 2021 at 18:33):

Sure! If you click on the "Files changed" tab, you'll see a popup which points out the error: "Files in mathlib cannot import the entire tactic folder". So you should see if you can import just the tactics that you use.

Bryan Gin-ge Chen (Jul 15 2021 at 18:36):

It looks to me like replacing the import tactic line with

import tactic.linarith
import tactic.ring

may work. I've added this as a suggestion on your PR.

Sara Díaz Real (Jul 15 2021 at 18:46):

Oh, thank you very much! I have accepted your suggestion. It looks like that it is ok. I hope so. Thanks very much, again


Last updated: Dec 20 2023 at 11:08 UTC