Currently the tests/dep/ folder has a lakefile that points to Mathlib's master branch. As this can move without this repo moving, it means testing is not reproducible.
Instead, we should pin a commit of Mathlib here.
I have added a note to the "Development" section of README.md to remind that this should be updated along with the lean-toolchain.
Description
Currently the
tests/dep/folder has a lakefile that points to Mathlib'smasterbranch. As this can move without this repo moving, it means testing is not reproducible.Instead, we should pin a commit of Mathlib here.
I have added a note to the "Development" section of README.md to remind that this should be updated along with the
lean-toolchain.