build cycle detected

Stream: general

[Kevin Buzzard]

Turns out that

stderr:
error: build cycle detected:
  +Game.Levels.Tutorial:lean.precompileImports
  +Game.Levels.Tutorial:lean.precompileImports

actually means "you can't import a file whose name starts with a numeral". This came about because I was changing a bunch of names of files from Level_01.lean, Level_02.lean.. into names like add_comm.lean and add_assoc.lean, and a passing computer scientist said "add the numbers at the front so they'll be sorted correctly in VS Code". I'm now going for L04add_comm.lean.

[Scott Morrison]

Mathematics in Lean uses the same solution.

[Eric Wieser]

Does import «01-add_comm» not work?

[Kevin Buzzard]

Do I need to put the package name in front of that?

[Scott Morrison]

I would strongly prefer we avoid french quotes in import statements, even to the point of proposing to disallow them. Whatever gain you think you're getting locally is outweighed by the suffering of the ecosystem having to cope with weird names.

[Jon Eugster]

something like L02_AddComm.lean sounds like the right thing to do

[Mac Malone]

Kevin Buzzard said:

"you can't import a file whose name starts with a numeral"

That sounds like a bug in import parsing, it should give a much cleaner error than that.

[Mac Malone]

Scott Morrison said:

Whatever gain you think you're getting locally is outweighed by the suffering of the ecosystem having to cope with weird names.

While I agree in spirit, we already permit a number of complexities in the import header -- line comments and nested block comments (in arbitrary locations), unicode, and special import keywords (e.g., prelude, runtime) -- that the parser is not trivial anyway. Thus, accounting for french quotes likely adds little complexity.

[Scott Morrison]

Ugh, but it's needless complexity, verging on complexity for its own sake. Life is better if french quotes are not allowed in imports.

[Mario Carneiro]

the complexity isn't needless, this came up in mathport in fact

[Mario Carneiro]

also consider that files may be written by tools, not humans, and there may be reasons to use weird characters and/or handle whatever the user provides

[Scott Morrison]

But the correct fix is to rename your files, as they did in MIL. (Note some of the MIL authors above agreeing with this. :-)

[Mac Malone]

Lake also uses French quotes imports for generating projects, but it could instead follow whatever rules exist.

[Mario Carneiro]

I think that having french-quote-free names is a fine project naming convention, but it doesn't belong in lake

[Mac Malone]

The interesting thing about the Lake use case is it does demonstrate that the lack of French quotes would increase the complexity of project generation code, rather than decrease it. This connects to @Mario Carneiro's point that tools generate Lean code may like it even if tools consuming Lean code do not. So, there is question of where does the burden belong.

[Mac Malone]

Given the already existing complexity of the import header parser, I would be inclined to put the burden there.

[Mac Malone]

Mac Malone said:

That sounds like a bug in import parsing, it should give a much cleaner error than that.

Looking at the parse code the problem is that encountering import A.0X is parsed as import A and then the .0X as the beginning of the code block. This is fine within the Lean code as it will still produce an error, but for the parse import in Lake, this hides the error (as Lake does not parse the rest of the file until is built) and produces a build loop on A. I will take a look at potentially solving this within the import parser code.