search

b-mehta / topos

Topos theory in lean
55 stars 2 forks source link

Lean 3.7.2 and new mathlib #33

Closed Vtec234 closed 4 years ago

Vtec234 commented 4 years ago

Staying on the bleeding edge, plus another attempt to use leanproject more. over.lean still fails, could you fix please @b-mehta ?

b-mehta commented 4 years ago

Have you seen the CI changes made by Ed in the beck branch? It might be better to adapt those instead of the ones from master (to be honest, those should be in master anyway though)

Vtec234 commented 4 years ago

I think the changes on master are more recent, but for now I reverted back to leanpkg because leanproject doesn't yet report errors via the exit code properly.

b-mehta commented 4 years ago

Sure, the changes in beck do have that fix

b-mehta commented 4 years ago

Sorted!

b-mehta commented 4 years ago

@Vtec234 I'm happy to merge this if you are!

Vtec234 commented 4 years ago

Thanks! CI is happy, let's merge.