unable to use leanproject

Stream: general

[Vasily Ilin]

When I do leanproject --help I get an error: ModuleNotFoundError: No module named 'nacl'. A month ago I used leanproject and it worked, not sure what changed since then. Also, pip install nacl does not work.

[Kevin Buzzard]

What OS?

[Arthur Paulino]

I suspect it's a Python environment issue. @Vasily Ilin do you use anaconda, miniconda, virtualenv or any other Python ENV manager?

[Julian Berman]

(FWIW nacl is a package that comes from PyNacl, so if your install somehow has had its salt go missing you get it back by installing pynacl not just nacl, which is a dependency of mathlibtools)

[Vasily Ilin]

@Kevin Buzzard , Windows 11

[Vasily Ilin]

I use anaconda, @Arthur Paulino

[Arthur Paulino]

Try installing pynacl as Julian said

[Michael Stoll]

I had a smilar problem recently, which was probably caused by my system updating from python3.8 to 3.10. Changing #!/usr/bin/python to #!/usr/bin/python3.8 at the top of the leanproject script solved that for me (this is on Linux, though).

[Eric Wieser]

I think reinstalling leanproject is a better idea than tweaking its scripts by hand

[Eric Wieser]

setuptools will automatically put the appropriate shebang in the script

[Vasily Ilin]

Arthur Paulino said:

Try installing pynacl as Julian said

It worked, thank you!