build fail

Stream: condensed mathematics

[Johan Commelin]

I have errors in for_mathlib/sheafification_mono.lean. Is someone wotking on that file?

[Kevin Buzzard]

Not me. I also have errors

[Kevin Buzzard]

I'll bisect. The build seems to have been broken for quite a few commits

[Kevin Buzzard]

fb0f7fe681ccbe340e6133de1503ab88af9b9d3e is the first bad commit
commit fb0f7fe681ccbe340e6133de1503ab88af9b9d3e
Author: Adam Topaz <github@adamtopaz.com>
Date:   Tue May 31 14:04:11 2022 -0400

    wip

 src/condensed/acyclic.lean                         | 50 +++++++++++++++++-----
 src/condensed/adjunctions.lean                     |  4 ++
 .../abelian_sheaves/functor_category.lean          |  2 +-
 src/for_mathlib/chain_complex_exact.lean           |  5 +++
 4 files changed, 49 insertions(+), 12 deletions(-)

[Kevin Buzzard]

I've fixed one error -- let's see how things go.

 noncomputable instance : abelian (Cᵒᵖ ⥤ Ab.{u+1}) :=
-functor.abelian.{(u+2) u (u+1)}
+category_theory.functor_category_is_abelian.{(u+2) u (u+1)}

[Kevin Buzzard]

Might be related to this diff in Adam's commit:

+-- ANNOYING!
+instance presheaf_abelian : abelian (Profinite.{u}ᵒᵖ ⥤ Ab.{u+1}) :=
+category_theory.functor_category_is_abelian.{(u+2) u (u+1)}

[Johan Commelin]

Hmm, seems like you made some progress. But I'm on a train, and my laptop isn't able to do speedy builds. I still get

lean-liquid/src/condensed/projective_resolution_module.lean: parsing at line 133external command exited with status 137

[Kevin Buzzard]

That's just some out of memory error, right? That file is compiling for me on master. I think I've fixed the build. Edit: yeah, master now compiles for me.

[Johan Commelin]

Ok, so my laptop is officially ultra-crappy

[Adam Topaz]

Sorry :( I renamed an iinstance and forgot to fix it elsewhhere...

[Adam Topaz]

Thanks for fiixing the build Kevin

[Kevin Buzzard]

If I build and get a 137, I just build again, it often starts at the place it got stuck and just continues. I see this a lot on one of my computers.

[Adam Topaz]

these fancy universe hacks are really messing with typeclass resolution. Is there something that can be done about that?