Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: Creating projects in lean


Clarissa Martelli (Nov 09 2020 at 10:19):

I keep having "leanproject : command not found" even if I keep downloading and following the steps on how to install lean and mathlib tools, how can I create a project using mac OS?

Eric Wieser (Nov 09 2020 at 10:28):

It sounds like your python installation isn't putting scripts on the path. Out of curiousity, does python -m mathlibtools.leanproject --help do anything?


Last updated: Dec 20 2023 at 11:08 UTC