search

hrmacbeth / math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
184 stars 82 forks source link

Bump mathlib and Lean #3

Closed PatrickMassot closed 10 months ago

PatrickMassot commented 1 year ago

WIP bump

hrmacbeth commented 1 year ago

Thank you, I will incorporate this at the next major update (probably in a month).

maverick-harmonic commented 11 months ago

Thanks! I actually ran into this same issue when incorporating it into a project with a newer mathlib.

hrmacbeth commented 11 months ago

@maverick-harmonic Can you say more about your use case? I am glad, but a little surprised, that there is something in the book (as opposed to in mathlib itself) which you want to rely on externally.

maverick-harmonic commented 11 months ago

This isn’t a typical use case. I didn’t have internet to download mathlib into your repo so I cloned it into a scratch repo I had that already had mathlib built. So all good 😊

On Sat, Oct 7, 2023 at 12:41 PM Heather Macbeth @.***> wrote:

@maverick-harmonic https://github.com/maverick-harmonic Can you say more about your use case? I am glad, but a little surprised, that there is something in the book (as opposed to in mathlib itself) which you want to rely on externally.

— Reply to this email directly, view it on GitHub https://github.com/hrmacbeth/math2001/pull/3#issuecomment-1751802861, or unsubscribe https://github.com/notifications/unsubscribe-auth/BBRKDHJRPQETLXTKBXF7GXLX6GV4ZAVCNFSM6AAAAAA5MPIEX6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJRHAYDEOBWGE . You are receiving this because you were mentioned.Message ID: @.***>

hrmacbeth commented 10 months ago

Bumped to latest mathlib in fe7386009629bc00a1bcc89065db2db305b0ab63