Error when importing Mathlib.RingTheory.TensorProduct

Stream: lean4

[Ali Ramsey]

Hi, I'm trying to contribute to Mathlib, but when I try to work on my branch, I get the error message

`c:\Users\arams\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lake.exe print-paths Init Mathlib.RingTheory.TensorProduct` failed:

stderr:
info: [835/1052] Building Mathlib.Algebra.GroupRingAction.Subobjects
info: [835/1052] Building Mathlib.GroupTheory.Subgroup.ZPowers
error: > LEAN_PATH=.\.lake/packages\std\.lake\build\lib;.\.lake/packages\Qq\.lake\build\lib;.\.lake/packages\aesop\.lake\build\lib;.\.lake/packages\proofwidgets\.lake\build\lib;.\.lake/packages\Cli\.lake\build\lib;.\.lake\build\lib PATH c:\Users\arams\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lean.exe -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false .\.\.\Mathlib\GroupTheory\Subgroup\ZPowers.lean -R .\.\. -o .\.lake\build\lib\Mathlib\GroupTheory\Subgroup\ZPowers.olean -i .\.lake\build\lib\Mathlib\GroupTheory\Subgroup\ZPowers.ilean -c .\.lake\build\ir\Mathlib\GroupTheory\Subgroup\ZPowers.c
error: external command `c:\Users\arams\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lean.exe` exited with code 3221225477

after just trying to import Mathlib.RingTheory,TensorProduct. I was previously working on my own Lean project separate from this, and the import worked fine there, so I'm not sure what's going wrong here? When I try to push to my branch without letting everything build, it fails the "check all files imported" test, just outputting Error: Process completed with exit code 1. Does anyone know what I'm doing wrong?

[Alex J. Best]

You mean the build is failing in CI even? Do you have a link?

[Ali Ramsey]

I think so, the branch is github.com/leanprover-community/mathlib4/tree/aramsey-coalgebras

[Oliver Nash]

@Ali Ramsey To get CI to pass you just need to add the line:

import Mathlib.RingTheory.Coalgebra

just below the line importing the class group file here: https://github.com/leanprover-community/mathlib4/blob/afb00b052d03e99a1c4abf4810dc4e6314f969f6/Mathlib.lean#L2946C5-L2946C5

[Oliver Nash]

I look forward to having coalgebras :-)

[Ali Ramsey]

Ohh ok, thank you!