lake "build cycle detected"

Stream: lean4

[Heather Macbeth]

Can anyone suggest how to solve a "build cycle detected" lake error? It looks like this:

% lake build
error: build cycle detected:
  +Foo:lean.precompileImports
  +Foo:bin
  Foo/Foo:leanLib.lean
  +Foo:lean.precompileImports

[Mario Carneiro]

that usually means there is an import cycle

[Heather Macbeth]

If relevant, it's a new project and I've never successfully built it before; I've been tinkering with the lakefile and directory structure; so there may be artifacts of some kind that I need to delete.

[Heather Macbeth]

But I don't think there's an import cycle: there's only one import in the main Foo.lean file.

[Mario Carneiro]

this one looks a bit weird though, I think it is saying that Foo depends on itself

[Mario Carneiro]

what does the lakefile look like

[Heather Macbeth]

Ah ... I think I have narrowed it down. There are folders in my intended directory structure whose names start with numbers. Is this illegal? It seems to be fixed when I change this.

[Mario Carneiro]

I don't think so?

[Mario Carneiro]

it sounds like a bug if so

[Heather Macbeth]

It really seems to have fixed it so :shrug:

[Mario Carneiro]

can you make a MWE?

[Heather Macbeth]

Yes -- not now but I'll do it in a few days.

[Moritz Firsching]

I was running into the same problem, and while creating a Mwe, I noticed that it can be solved by adding weird quotes
so in the initial commit in
https://github.com/mo271/mwe
I get

> lake build
error: build cycle detected:
  +Mwe:lean.precompileImports
  +Mwe:bin
  mwe/Mwe:leanLib.lean
  +Mwe:lean.precompileImports

The diff that fixes is looks like this:

diff --git a/Mwe.lean b/Mwe.lean
index 005f72b..c6ce100 100644
--- a/Mwe.lean
+++ b/Mwe.lean
@@ -1,2 +1,2 @@
 import Mwe.Test
-import Mwe.1_starts_with_number
+import Mwe.«1_starts_with_number»

What works no matter if the weird quotes are added in the Mwe.lean or not is

> lake build Mwe.1_starts_with_number

But the following never worked for me:

> lake build Mwe.«1_starts_with_number»
error: no such file or directory (error code: 2)
  file: ./././Mwe/«1_starts_with_number».lean

[Moritz Firsching]

oh, forgot to say:
I got the idea to try the quotes, because the output of the lake build command included them:

> lake build Mwe.1_starts_with_number
Building Mwe.«1_starts_with_number»

[Mario Carneiro]

I'm surprised import Mwe.1_starts_with_number works in the first place, name components can't start with numbers afaik

[Mario Carneiro]

the guillemets are used to quote name components containing illegal characters that make them not legal identifiers or keywords

[Mac Malone]

(deleted)

[Sebastian Ullrich]

This could be considered a bug in ParseImportsFast, it shouldn't succeed to parse that line as import Mwe

[Filippo A. E. Nuccio]

I am having the same problem with

error : dependency cycle detected:
mathlib
mathlib

[Filippo A. E. Nuccio]

The strange (?) thing is that if I do lake new something math everything seems to work, but if I try lake new Mathlib math, I get the above error.

[Mac Malone]

Filippo A. E. Nuccio said:

The strange (?) thing is that if I do lake new something math everything seems to work, but if I try lake new Mathlib math, I get the above error.

Well this creates a new library called 'Mathlib' that depends on 'Mathlib', which is a cyclic self-reference.

[Filippo A. E. Nuccio]

Ok, so I *should not * call my new library mathlib. So I tried

lake new test math
cd test
lake update

and indeed I have a working mathlib4project.

[Filippo A. E. Nuccio]

But I wanted to run the script ./scripts/start_port.sh Mathlib/X/Y/Z.lean (for suitable X, Y, Z of course) and it cannot find it: bash: ./scripts/start_port.sh: No such file or directory. Am I missing something in the porting procedure?

[Mario Carneiro]

it is of course not in ./scripts since that would be in your project, not in mathlib

[Filippo A. E. Nuccio]

Ah right, it makes sense.

[Mario Carneiro]

you could use lake-packages/mathlib/scripts/start_port.sh but does this even work outside mathlib?

[Mario Carneiro]

start_port.sh is for creating new mathlib files

[Filippo A. E. Nuccio]

Yes, this is what I would like to do.

[Filippo A. E. Nuccio]

I thought (wrongly, afaiu) that I should start a project and then work from there.

[Mario Carneiro]

I mean even if you call it I would just expect it to make a mess of things

[Mario Carneiro]

pretty sure most porters are working inside mathlib itself

[Filippo A. E. Nuccio]

And how should I proceed, rather? I am simply willing to (try to) port ring_theory/localization/submodule.lean that seems ready to be ported.

[Kevin Buzzard]

Filippo, if you are proposing to join the porting effort then you should be cloning mathlib, not making a new project.

[Filippo A. E. Nuccio]

Oh good: and by cloningyou mean the old good nice git clone?

[Filippo A. E. Nuccio]

WOW, I was drowning myself for the sake of it...

[Filippo A. E. Nuccio]

Thanks

[Kevin Buzzard]

git clone git@github.com:leanprover-community/mathlib4.git
cd mathlib4
lake exe cache get

(the last command is the analogue of leanproject get-cache)

[Kevin Buzzard]

Then lake build (the analogue of leanproject build) should return quickly because everything is built, and you can now start following the very clear instructions on the porting wiki.

[Filippo A. E. Nuccio]

Thanks! I though that there was a lake command that would create a copy of mathlib+cache, but now I see that the easiest way is the right one.

[Mario Carneiro]

the command lake new myproj math is for creating a fresh project of your own which depends on mathlib (I don't think it knows about the cache, but you can follow up with lake exe cache get)

[Filippo A. E. Nuccio]

Oh, I see. I thought that math meant that it would have been mathlib, whereas it just adds mathlib as dependency. Thank you!

[Filippo A. E. Nuccio]

I will try the port later, hoping to get somewhere! :pray: