linter

Stream: condensed mathematics

[Ben Toner]

The linter broke yesterday due to a change in the mathlib interface - I've fixed that.

Separately, the linter was not working because of conflicts between https://github.com/leanprover-community/lean-liquid/blob/master/src/condensed/proetale_site_as_small.lean and https://github.com/leanprover-community/lean-liquid/blob/master/src/condensed/proetale_site.lean . I'm not following the maths, but I'm assuming these are alternatives... is that right?

The current linting workflow creates a file all.lean which imports everything in src, i.e., both of these. It seems totally reasonable to me to have alternate implementations on master but I don't know the right way to fix the linter to deal with this. As a temporary fix, I've excluded proetale_site_as_small.lean from being included in all.lean.

[Johan Commelin]

@Ben Toner Thanks for the catch. @Adam Topaz can you confirm that we can now use the as_small version, and comment out the other file?

[Adam Topaz]

@Johan Commelin I was going to take care of this today, but my power went out about 2 hours ago... Not sure if it's coming back any time soon

[Johan Commelin]

Ok, well good luck!

[Adam Topaz]

It's back :light_bulb: And I modified the stuff in the condensed/* folder to use the proetale topology on as_small Profinite. Just checking everything compiles before pushing to master.

[Adam Topaz]

Okay, it's pushed now.

I think it should be safe to include proetale_site_as_small.lean in the all.lean file again (the stuff in proetale_site.lean is all commented out)

[Ben Toner]

Thanks - I reverted the temporary fix and proetale_site_as_small.lean is included again. The linting step is still red but linting is no longer broken - the linting errors will be cleaned up in the next run of the nolints.txt workflow.

[Johan Commelin]

Thanks, both of you!