Zulip Chat Archive

Stream: general

Topic: unable to use leanproject


Vasily Ilin (Jun 23 2022 at 06:44):

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 (Jun 23 2022 at 07:06):

What OS?

Arthur Paulino (Jun 23 2022 at 10:42):

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

Julian Berman (Jun 23 2022 at 12:25):

(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 (Jun 23 2022 at 16:11):

@Kevin Buzzard , Windows 11

Vasily Ilin (Jun 23 2022 at 16:11):

I use anaconda, @Arthur Paulino

Arthur Paulino (Jun 23 2022 at 16:13):

Try installing pynacl as Julian said

Michael Stoll (Jun 23 2022 at 16:29):

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 (Jun 23 2022 at 16:39):

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

Eric Wieser (Jun 23 2022 at 16:39):

setuptools will automatically put the appropriate shebang in the script

Vasily Ilin (Jun 30 2022 at 04:56):

Arthur Paulino said:

Try installing pynacl as Julian said

It worked, thank you!


Last updated: Dec 20 2023 at 11:08 UTC