Build Fails Only on Ubuntu

Stream: general

[Asei Inoue]

In the repository I maintain, https://github.com/lean-ja/lean-by-example, the GitHub Actions build is currently failing on Ubuntu, while it passes without issue on Windows. I have no idea why this is happening. If anyone has any insights into the cause, I would appreciate your help.

[Asei Inoue]

log is here:

  ✖ [3247/3308] Running Playground.Monkey.Ast.Ast
  error: no such file or directory (error code: 2)
    file: /home/runner/work/lean-by-example/lean-by-example/Playground/Monkey/Ast/Ast.lean
  ✖ [3248/3308] Running Playground.Monkey.Parser.Parser
  error: /home/runner/work/lean-by-example/lean-by-example/Playground/Monkey/Parser/Parser.lean: bad import 'Playground.Monkey.Ast.Ast'
  ✖ [3249/3308] Running Playground.Monkey.Parser.ParserTest
  error: /home/runner/work/lean-by-example/lean-by-example/Playground/Monkey/Parser/ParserTest.lean: bad import 'Playground.Monkey.Parser.Parser'
  ✔ [3303/3308] Built Playground.Monkey.Token.Token
  ✔ [3304/3308] Built Playground.Monkey.Lexer.Lexer
  ✔ [3305/3308] Built Playground.Monkey.AST.Ast
  ✔ [3306/3308] Built Playground.Monkey.Repr.Repr
  ✔ [3307/3308] Built Playground.Monkey.Lexer.LexerTest
  Some required builds logged failures:
  - Playground.Monkey.Ast.Ast
  - Playground.Monkey.Parser.Parser
  error: build failed
  - Playground.Monkey.Parser.ParserTest
  Error:  lake build failed
  Error: Process completed with exit code 1.

[Asei Inoue]

version is: leanprover/lean4:v4.22.0-rc3

[Robin Arnez]

Unix is case-sensitive; you import import Playground.Monkey.Ast.Ast but you have Playground.Monkey.AST.Ast as the file name.

[Robin Arnez]

Windows isn't so it works there

[Julian Berman]

I get bitten by this every so often myself. You might want to thumbs up lean4#5409 and/or lean4#2768

[Asei Inoue]

@Robin Arnez Oh Thank you!!!!!!!

[Bhavik Mehta]

Perhaps this could go on the pitfalls page, since it does indeed show up surprisingly often

[Patrick Massot]

Is there a Windows pitfalls page??

[Edward van de Meent]

arguably this is an ubuntu pitfall

[Ruben Van de Velde]

How do other languages deal with this?

[Niels Voss]

I think python enforces case sensitivity even when the platform is not case sensitive (though somehow for the engineering team I'm part of we still managed to screw this up and write a Python program that only runs on macOS, which shouldn't be possible).

[Niels Voss]

Maybe it's worth considering enforcing on all OSes both case sensitivity of imports and also making sure that all file names are valid identifiers on Windows, Linux, and macOS (https://stackoverflow.com/a/31976060/30840616 claims that Aux.lean is an invalid file name, for example, though it appears to be valid for me on Windows), and making it so that if there are two files with the same name in different case, then importing either of them should fail (if this does not cause a performance penalty)

[Michael Rothgang]

Cross-linking #mathlib4 > Never name a file Con.lean for discoverability

[Michael Rothgang]

The latter (case collisions) has been a mathlib linter for a while now.

[Michael Rothgang]

The former (forbidden names on (all but new versions of) Windows) got a linter yesterday.

[Michael Rothgang]

In mathlib, you can use lake exe lint-style to run these checks.

[Michael Rothgang]

@Anne Baanen You worked on allowing downstream projects to do the same. Can you remind us of the right way to do so?

[Michael Rothgang]

If you dependent on mathlib, you can run lake exe lint-style locally, that should work. (Perhaps you need to set an option to explicitly enable that linter; I'd need to check.)

[Michael Rothgang]

To run things in CI, there is a special CI action now. Anne was involved and can tell us more.

[Michael Rothgang]

Speaking of which: is there a dedicated webpage "here's how you can set up your CI to re-use mathlib's tools"? (In the mean time, there is https://github.com/pitmonticone/LeanProject --- which probably wouldn't mind somebody making a PR adding some of the very recent goodies. https://github.com/pitmonticone/LeanProject/issues/30 tracks some of them.)

[Anne Baanen]

Michael Rothgang said:

Anne Baanen You worked on allowing downstream projects to do the same. Can you remind us of the right way to do so?

To run lint-style in CI it should be as easy as adding the leanprover-community/lint-style-action step to your build workflow. For example:

on:
  push:
  pull_request:

jobs:
  lint-style:
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - uses: leanprover-community/lint-style-action
        with:
          mode: check
          lint-bib-file: true