ITADN

Setup instructions in README lead to "package 'scilean' was required as 'leanblas'"

#62Opennielsvoss 创建于 2025-06-09
N
nielsvosscommented
I tried following the instructions in the README to make a project that depends on SciLean and I get the error `package 'scilean' was required as 'leanblas'`. I suspect the issue comes from this line in the README: ```lean require leanblas from git "https://github.com/lecopivo/SciLean" @ "v4.18.0" ``` Changing `leanblas` to `scilean` seems to fix this (I also removed the "v4.18.0" from my lakefile because I am using lean v4.20.1).
2 条评论