Setup instructions in README lead to "package 'scilean' was required as 'leanblas'"
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 条评论