leanproject and python 3.9.1

Stream: general

[Scott Morrison]

Someone (err... me, I guess?) has upgraded python underneath me, and now I get:

$ python3 --version
Python 3.9.1
$ leanproject up
Traceback (most recent call last):
  File "/usr/local/bin/leanproject", line 5, in <module>
    from mathlibtools.leanproject import safe_cli
  File "/usr/local/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 11, in <module>
    from mathlibtools.lib import (LeanProject, log, LeanDirtyRepo,
  File "/usr/local/lib/python3.8/site-packages/mathlibtools/lib.py", line 17, in <module>
    import networkx as nx # type: ignore
  File "/usr/local/lib/python3.8/site-packages/networkx/__init__.py", line 115, in <module>
    import networkx.readwrite
  File "/usr/local/lib/python3.8/site-packages/networkx/readwrite/__init__.py", line 15, in <module>
    from networkx.readwrite.graphml import *
  File "/usr/local/lib/python3.8/site-packages/networkx/readwrite/graphml.py", line 314, in <module>
    class GraphML(object):
  File "/usr/local/lib/python3.8/site-packages/networkx/readwrite/graphml.py", line 344, in GraphML
    types = [(np.float64, "float"), (np.float32, "float"),
AttributeError: module 'numpy' has no attribute 'float64'

(This is on macos.) Anyone seen this / know what to do?

[Scott Morrison]

Solution: run the all-in-one macos Lean installation script over the top of everything!

[Scott Morrison]

Works now. :-)

[Eric Wieser]

leanprover-community/mathlib-tools#95 will make this problem go away by not even trying to import numpy unless you ask for an import graph