leanproject

Stream: general

[Kenny Lau]

How do I download a specific version of mathlib (and Lean)?

[Kenny Lau]

currently I just created a new project using leanproject newand then changed the leanpkg.tomlmanually (by copying from another repo and changing the commit to what I need) and then using leanproject get-mathlib-cache

[Kenny Lau]

do I need to do this every time?

[Ryan Lahfa]

what would you want to see in terms of workflow?

[Ryan Lahfa]

it could be possible I guess to have leanproject new --leanversion XXX, but for mathlib, I don't know if there's any proper tagging or versioning beyond the commit SHA256

[Kenny Lau]

kc_ke@LAPTOP-DBUNR5U5 MINGW64 /c/mathlib (master)
$ leanproject get-cache
 ** On entry to DGEBAL parameter number  3 had an illegal value
 ** On entry to DGEHRD  parameter number  2 had an illegal value
 ** On entry to DORGHR DORGQR parameter number  2 had an illegal value
 ** On entry to DHSEQR parameter number  4 had an illegal value
 ** On entry to DGEBAL parameter number  3 had an illegal value
 ** On entry to DGEHRD  parameter number  2 had an illegal value
 ** On entry to DORGHR DORGQR parameter number  2 had an illegal value
 ** On entry to DHSEQR parameter number  4 had an illegal value
Traceback (most recent call last):
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\runpy.py", line 197, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\runpy.py", line 87, in _run_code
    exec(code, run_globals)
  File "C:\Users\kc_ke\AppData\Local\Programs\Python\Python39\Scripts\leanproject.exe\__main__.py", line 4, in <module>
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\leanproject.py", line 11, in <module>
    from mathlibtools.lib import (LeanProject, log, LeanDirtyRepo,
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\lib.py", line 17, in <module>
    import networkx as nx # type: ignore
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\networkx\__init__.py", line 64, in <module>
    import networkx.readwrite
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\networkx\readwrite\__init__.py", line 16, in <module>
    from networkx.readwrite.gexf import *
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\networkx\readwrite\gexf.py", line 173, in <module>
    class GEXF:
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\networkx\readwrite\gexf.py", line 211, in GEXF
    import numpy as np
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\numpy\__init__.py", line 305, in <module>
    _win_os_check()
  File "c:\users\kc_ke\appdata\local\programs\python\python39\lib\site-packages\numpy\__init__.py", line 302, in _win_os_check
    raise RuntimeError(msg.format(__file__)) from None
RuntimeError: The current Numpy installation ('c:\\users\\kc_ke\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\numpy\\__init__.py') fails to pass a sanity check due to a bug in the windows runtime. See this issue for more information: https://tinyurl.com/y3dm3h86

[Alex J. Best]

https://github.com/twintproject/twint/issues/1030 ?

[Kevin Buzzard]

Don't forget to add a "Thanks a lot!" message at the bottom.

[Kenny Lau]

Thanks, that worked

[Eric Wieser]

I think this came up elsewhere - leanproject should not even attempt to import numpy /networkx until asked for the import graph

[Eric Wieser]

Doing so just makes leanproject slow and fragile

[Yaël Dillies]

I just set up a repo for the formalization of Con(NF) that will happen this summer and people seem unable to get it using leanproject. Namely, running leanproject get con-nf (the repository is https://github.com/leanprover-community/con-nf) returns

> git checkout --detach de5038953210a6ffb013340c7bf82243be226f1c    # in directory _target/deps/mathlib
fatal: reference is not a tree: de5038953210a6ffb013340c7bf82243be226f1c
external command exited with status 128
Command '['leanpkg', 'configure']' returned non-zero exit status 1.

@Patrick Massot, did I miss something obvious by any chance?

[Bryan Gin-ge Chen]

(This likely isn't related to your issue, but you should add /_target and leanpkg.path to a .gitignore file. See e.g. mathlib's.)

[Yaël Dillies]

I independently came to the conclusion that this was my issue, because deleting _target and leanpkg.path and running leanproject get-m fixed the install.

[Bryan Gin-ge Chen]

Ah, I see. You had mathlib set up as a submodule in _target/deps, which I don't think leanproject supports.

[Yaël Dillies]

Do you mean my error is deeper?

[Bryan Gin-ge Chen]

If you make a new commit with a .gitignore like I suggested and git doesn't complain then you've probably fixed it.

[Bryan Gin-ge Chen]

I'm not sure how you created mathlib as a submodule, so I can't be sure if there's a deeper issue.

[Yaël Dillies]

I ran leanproject get-m

[Eric Rodriguez]

(the reference at the bottom of the readme refers to LTE still btw)

[Bryan Gin-ge Chen]

Someone with more git knowledge should probably jump in, but it looks like creating a commit which contains the mathlib git repo as a subdirectory tells git to treat it like a submodule. Anyways, adding a proper .gitignore file and removing _target from the repo if necessary should hopefully fix things.