trouble setting up mathlib after upgrade

Stream: maths

[Jakob von Raumer]

I upgraded my (Ubuntu) dist and since have trouble getting mathlib to build. I'm getting errors like the following:

javra2@i44pc23:/data1/jakob/mathlib$ leanproject build
Building project mathlib
configuring mathlib 0.1
> lean --make src
/data1/jakob/mathlib/src/topology/sheaves/sheaf.lean:1:0: error: file 'category_theory/limits/punit' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

I reckoned this was due to some mistake by mathlibtools and tried to reinstall mathlibtools with pipx reinstall mathlibtools but I'm getting a

/home/javra2/.local/pipx/venvs/mathlibtools/bin/python: No module named pip

which is weird. I do have python3-pip installed.

Since I've no idea about python, can somebody help?

[Anne Baanen]

Jakob von Raumer said:

I reckoned this was due to some mistake by mathlibtools and tried to reinstall mathlibtools with pipx reinstall mathlibtools but I'm getting a

/home/javra2/.local/pipx/venvs/mathlibtools/bin/python: No module named pip

I've seen this error before when I updated Python. Assuming Ubuntu puts things in the typical place, maybe you can try /usr/bin/python3 -m pip install pipx to reinstall pipx for the new Python version.

[Eric Wieser]

"not found in the search path" usually means you need to run leanpkg configure

[Jakob von Raumer]

Anne Baanen said:

I've seen this error before when I updated Python. Assuming Ubuntu puts things in the typical place, maybe you can try /usr/bin/python3 -m pip install pipx to reinstall pipx for the new Python version.

Ahh, that seems to have worked, thanks!

[Jakob von Raumer]

Eric Wieser said:

"not found in the search path" usually means you need to run leanpkg configure

Had tried that already, but there's something else wrong I guess

[Jakob von Raumer]

Still getting /home/javra2/.local/pipx/venvs/mathlibtools/bin/python: No module named pip :(

[Jakob von Raumer]

Seems like something is wrong with some "virtual environment" used by pip?

[Jakob von Raumer]

Maybe the two problems are actually unrelated to each other, I don't know... But i can't seem to solve either one

[Jakob von Raumer]

Okay, the one problem seems to be that category_theory.limits.punit seems to be on the end of my branch (preserves-universes) :grimacing: