Compileation problem when submit PR in mathlib.

Stream: general

[Brisal]

Hello! After I submitted my PR, this issue occurred during the mathlib compilation. How can I resolve it?

uncaught exception: object file '/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib.olean' of module Mathlib does not exist

[Kevin Buzzard]

Can you tell us the PR number? Ideally you would also put your github username in your Zulip profile, then I could just look for it without having to bother you.

[Eric Wieser]

You're not reading the right error message, there's a better error message higher up

[Brisal]

Kevin Buzzard said:

Can you tell us the PR number? Ideally you would also put your github username in your Zulip profile, then I could just look for it without having to bother you.

Hello professor, this is my pr number #29361

[Riccardo Brasca]

It is related to a very recent change in mathlib. Start the file with

module

import Mathlib.RingTheory.PowerSeries.Basic
import Mathlib.Combinatorics.Enumerative.Catalan

and

## TODO
* Find and prove the closed formula for the Catalan generating function:
  `C(X) = (1 - √(1 - 4X)) / (2X)`

-/

@[expose] public section

open Finset

[Kevin Buzzard]

@FlAmmmmING I didn't mean "change your Zulip username to your github username", I meant "go to your Zulip profile and where it says Github Username put your Github username". Ideally your Zulip username would be your full real name, that is the convention we like here (particular for people who are making PRs to mathlib).

[Brisal]

Kevin Buzzard said:

FlAmmmmING I didn't mean "change your Zulip username to your github username", I meant "go to your Zulip profile and where it says Github Username put your Github username". Ideally your Zulip username would be your full real name, that is the convention we like here (particular for people who are making PRs to mathlib).

OKOK :joy: , thank you professor.

[Eric Wieser]

Eric Wieser said:

You're not reading the right error message, there's a better error message higher up

The real error is here:

start of lake build: attempt 1
✖ [7571/7572] Building Mathlib (4.0s)
  trace: .> LEAN_PATH=/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/Cli/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/batteries/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/Qq/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/aesop/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/importGraph/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/plausible/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean /home/lean/.elan/toolchains/leanprover--lean4---v4.26.0-rc1/bin/lean /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib.lean -o /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib.olean -i /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib.ilean -c /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/ir/Mathlib.c --setup /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/ir/Mathlib.setup.json --json
  Error: error: Mathlib.lean:1:0: cannot import non`-module` Mathlib.RingTheory.PowerSeries.Catalan from `module`
  error: Lean exited with code 1
Some required targets logged failures:
- Mathlib
error: build failed

[Brisal]

Eric Wieser said:

Eric Wieser said:

You're not reading the right error message, there's a better error message higher up

The real error is here:

start of lake build: attempt 1
✖ [7571/7572] Building Mathlib (4.0s)
  trace: .> LEAN_PATH=/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/Cli/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/batteries/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/Qq/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/aesop/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/importGraph/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/plausible/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean /home/lean/.elan/toolchains/leanprover--lean4---v4.26.0-rc1/bin/lean /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib.lean -o /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib.olean -i /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib.ilean -c /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/ir/Mathlib.c --setup /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/ir/Mathlib.setup.json --json
  Error: error: Mathlib.lean:1:0: cannot import non`-module` Mathlib.RingTheory.PowerSeries.Catalan from `module`
  error: Lean exited with code 1
Some required targets logged failures:
- Mathlib
error: build failed
````

Thank you, I've noticed now that the new version of mathlib has quite a few changes. I'm currently fixing my PR.