master broken

Stream: condensed mathematics

[Kevin Buzzard]

I've been pushing to master today and I've just noticed that for_mathlib/homotopy_category_pretriangulated is broken for me. Hopefully this wasn't my fault!

[Johan Commelin]

I'm doing a build. Let's find out what's wrong (-;

[Johan Commelin]

I think I've fixed it. One more check, then I'll push

[Kevin Buzzard]

I still have

/home/buzzard/lean-projects/lean-liquid/src/for_mathlib/homotopy_category_pretriangulated.lean:91:13: error: unknown identifier 'splitting_of_is_iso_zero'

[Johan Commelin]

Yeah, I'm not done fixing everything. More errors popping up

[Johan Commelin]

Ok, now it's done. Pushed

[Kevin Buzzard]

Normally I would just think "well someone else broke it and probably they'll fix it soon enough" but because I'm active in pushing to master right now I'm always scared that it's my fault! Looks like it's compiling again -- thanks. I'm about to show it off at the University of Southampton!

[Johan Commelin]

I think Scott's refactor caused rw's to miss out on some type class inferences.

[Scott Morrison]

Sorry. :-( I though I let leanpkg build run to completion, but maybe I made further changes afterwards.

[Kevin Buzzard]

for_mathlib/is_quasi_iso_sigma.lean is broken for me on master

[Adam Topaz]

fixed..

[Adam Topaz]

oops wait.

[Adam Topaz]

I'm fixing it now...

[Adam Topaz]

Okay, it should be fixed now.

[Adam Topaz]

sorry about that

[Kevin Buzzard]

I'm just always worried it's my fault!

[Kevin Buzzard]

Hmm, I was just editing stuff in src/laurent_measures and now src/laurent_measures/ext.lean isn't compiling for me. I'm hoping this is @Adam Topaz 's fault and unrelated to my changes...

[Kevin Buzzard]

aargh no it is my fault :-/ I'll fix it