lake check-lint failed

Stream: general

[Artie Khovanov]

I tried to update my blueprint configuration manually to fix the error as at this topic: #lean4 > lake update blueprint project

Now the blueprint action gives me the error "lake check-lint failed". I tried updating everything and even moving manutally to lakefile.toml (I was still on lakefile.lean) but I have no idea what I'm doing and possibly made matters worse.

Anyone know how to fix this?

[Ruben Van de Velde]

Maybe if you give more information, like a link to a log

[Artie Khovanov]

https://github.com/artie2000/real_closed_field/actions/runs/20576523477/job/59094623945

[Bryan Gin-ge Chen]

So the error is just saying that lake lint is failing since there's no linter set up, I think. Maybe copying some of the linting options from another project e.g. https://github.com/RemyDegenne/brownian-motion/blob/master/lakefile.toml will help?

[Artie Khovanov]

Oh I see
I'll just delete the linting step in the action, I don't need to lint in order to see my blueprint

[Artie Khovanov]

Thank you!