leanprover-community / mathlib-tools Goto Github PK

Development tools for https://github.com/leanprover-community/mathlib

License: Apache License 2.0

Python 92.63% Shell 5.27% Lean 1.80% Nix 0.30%

mathlib-tools's Introduction

mathlib-tools

This package contains leanproject, a supporting tool for Lean 3 mathlib.

This tool is fully obsolete and no longer has any relevance outside of historical studies. All Lean users are now expected to switch to Lean 4 which is not supported at all by this tool.

Installation

In principle, you should install those tools as part of the global Lean installation procedure recommended by the Lean community. Read what what remains of this section only if you want more details about this specific part of the procedure (the tools described here won't give you anything if Lean itself is not available).

Released version

`pipx`

The tools in this repository use python3, at least python 3.6, which is the oldest version of python supported by the python foundation. They can be installed using pip. The basic install command for the latest released version is thus:

python3 -m pip install mathlibtools

The above command may complain about permissions. This can be solved by running it as root, but this is not recommended in general. You can run python3 -m pip install --user mathlibtools to install it in your home directory (make sure that $HOME/.local/bin/ is on your shell path afterwards), but an even better way is to use pipx:

python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools

`macOS`

If you are on macOS, the recommended way to install is via homebrew, which will handle the above Python installation for you:

brew install mathlibtools

`NixOS`

If you are using NixOS, you can also install mathlib tools using the bundled default.nix file:

nix-env -if https://github.com/leanprover-community/mathlib-tools/archive/master.tar.gz

Development version

If you want to use the latest development version, you can clone this repository, go to the repository folder, and run pip install ..

Usage

See the dedicated page on the community website. Recall this tool is fully obsolete and no longer has any relevance outside of historical studies. All Lean users are now expected to switch to Lean 4 which is not supported at all by this tool.

mathlib-tools's People

Contributors

Stargazers

Watchers

mathlib-tools's Issues

`leanproject check` fails with error

$ elan default 3.4.2
$ leanproject get mathlib
$ cd mathlib
$ lean --version
Lean (version 3.6.1, commit 97f11c47b944, Release)
$ lean -p
{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "/home/gebner/tmp/mathlib/leanpkg.path",
  "path": [
    "/home/gebner/.elan/toolchains/leanprover-community-lean-3.6.1/bin/../library",
    "/home/gebner/.elan/toolchains/leanprover-community-lean-3.6.1/bin/../lib/lean/library",
    "/home/gebner/tmp/mathlib/./src"
  ]
}
$ leanproject check
[Errno 2] No such file or directory: '/home/gebner/.elan/toolchains/3.5c/tmp/bench30.olean'

I'm not sure why it searches in /home/gebner/.elan/toolchains/3.5c at all.

'leanproject new' fails with lean 4 installed

If one has lean 3 and lean 4 both installed with lean 4 as the system default, the behavior of leanproject new test is cryptic.

What happens is that leanproject calls leanpkg new test, but elan interprets that as a call to the lean 4 leanpkg, which does not have a new command.

leanproject hooks scripts are out of date

The edits to the post-checkout hook that @semorrison made in #71 aren't included in 0.0.9.

You can confirm this by downloading and untarring mathlibtools-0.0.9.tar.gz on pypi, and noticing that the post-checkout script there is an old version which doesn't match the one currently in the mathlib-tools repo.

Reported on zulip, but I think the timing of the message was bad.

`elan` is not on $PATH in gnome-terminal

I'm trying out the fast installation instructions, running install-debian.sh on a mostly clean Ubuntu 18.04 installation. After running the installation script, VS Code, elan and lean are all available. However, when I open a new terminal, elan and lean are not on the PATH.

It seems that the cause is that elan is added to the PATH in .profile only, and gnome-terminal opens an interactive, non-login shell, so it will only source .bashrc, not .profile. (And the default .bashrc on Ubuntu doesn't source .profile.) I think the correct solution is to add elan to the PATH both in .profile and in .bashrc, this is also what pipx does with its PATH.

Make a longest-pole script

Integrate the Python script from this PR, which and prints the "Longest Pole".

paramiko causing problems when running leanproject

After installing mathlibtools through pip3, I'm getting this when I run leanproject:

Traceback (most recent call last):
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\runpy.py", line 192, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Users\mateo\AppData\Local\Programs\Python\Python38\Scripts\leanproject.exe\__main__.py", line 4, in <module>
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\mathlibtools\leanproject.py", line 9, in <module>
    import paramiko # type: ignore
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\paramiko\__init__.py", line 22, in <module>
    from paramiko.transport import SecurityOptions, Transport
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\paramiko\transport.py", line 89, in <module>
    from paramiko.dsskey import DSSKey
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\paramiko\dsskey.py", line 37, in <module>
    from paramiko.pkey import PKey
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\paramiko\pkey.py", line 31, in <module>
    import bcrypt
  File "c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\bcrypt\__init__.py", line 25, in <module>
    from . import _bcrypt
ImportError: cannot import name '_bcrypt' from partially initialized module 'bcrypt' (most likely due to a circular import) (c:\users\mateo\appdata\local\programs\python\python38\lib\site-packages\bcrypt\__init__.py)

I tried emptying my pip3 packages and reinstalling:

pip3 freeze --local | xargs pip3 uninstall -y
pip3 --no-cache-dir install mathlibtools

But had no luck. To get around this issue I simply commented out the paramiko imports in leanproject.py. I'm using pip 20.0.2 with python 3.8.0.

lint

Would it be an idea to add leanproject lint so that you can locally lint your PR?

import-graph dot file

Currently, the dot file generated by leanproject import-graph contains lots of layout information. Of course this is useful for creating good-looking rendering. But it's annoying for post-processing the file using command-line filters like sed and grep. Could we have an option to generate a barebones minimalist .dot file?

name of repo vs pip package

Minor issue: Can we use mathlibtools everywhere? Or mathlib-tools?

Making Lean project a git submodule of another git repo

It would be lovely if instructions could be given for accomplishing this task. We want a lean project that we're developing, which uses mathlib, to be a git subproject of a larger git repo that we're developing. We want to be able to update lean and mathlib using these tools, while pushing changes to our own code to our own repo.

`leanproject new projet` fails if default toolchain is not set up correctly

$ leanproject new projet
error: ill-formed search path entry '/home/gebner/lean4/library', should be of form 'pkg=path'
Traceback (most recent call last):
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/bin/.leanproject-wrapped", line 9, in <module>
    sys.exit(cli())
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 717, in main
    rv = self.invoke(ctx)
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 1137, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 66, in new
    LeanProject.new(Path(path), cache_url, force_download)
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 390, in new
    proj = cls.from_path(path, cache_url, force_download)
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 218, in from_path
    repo = Repo(path, search_parent_directories=True)
  File "/nix/store/h5i5dyh5nsgc3m7fnql201lrw2qjng78-python3.7-GitPython-3.0.5/lib/python3.7/site-packages/git/repo/base.py", line 133, in __init__
    raise NoSuchPathError(epath)
git.exc.NoSuchPathError: /home/gebner/projet

`leanproject get mathlib` doesn't fetch oleans

$ leanproject get mathlib
$ cd mathlib
$ find -name \*.olean
(nothing)

Installing with asdf python

After running pip install mathlibtools in an asdf based installation of python (plugin), leanproject is not available:

$ leanproject
leanproject: command not found

I guess the binary gets added to somewhere outside of PATH, but didn't have time to track it down.

Installed in a virtual-env instead, e.g.

cd my_project
python -m venv venv
source venv/bin/activate

pip install mathlibtools

leanproject new

MacOS brew update of Python breaks leanproject

Whenever I update the Python with Homebrew, leanproject breaks

zsh: /Users/ar/.local/bin/leanproject: bad interpreter: /Users/ar/.local/pipx/venvs/mathlibtools/bin/python: no such file or directory

Any idea? So far, I am removing the pipx and reinstalling mathlibtools!

clean up git after leanproject get-mathlib-cache

Feature request: have leanproject get-mathlib-cache execute at the end:

git reset --hard [commit id specified by leanpkg.toml]
git clean -fd

Interrupting download leaves corrupted archive behind

leanproject up
ctrl+c while it is downloading
leanproject up
Error message: Aborted!

In leanpkg.toml, allow git revision commit hash to be replaced by tag name

It would be great if update-mathlib could parse something like the following in leanpkg.toml:

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", tag = "nightly-2020-02-19"}

This would have a couple of significant benefits: it would save having to look up the revision commit hash on github every time an update is wanted, and it would make the dependency much more human-readable.

The code changes required are relatively straightforward; I could write this if wanted.

leanproject get-mathlib-cache doesn't tidy up after itself

The easiest way to explain the issue is to show the problem "backwards".

leanproject get ImperialCollegeLondon/real-number-game
cd real-number-game
git checkout 351e7a41d24413ef1325be3bfa23805af2c42da4
leanproject get-mathlib-cache
lean --make src

produces a gazillion errors, the first one of which is

/home/buzzard/test/real-number-game/_target/deps/mathlib/src/algebra/big_operators.lean:1:0: error: ambiguous import, it can be '/home/buzzard/test/real-number-game/_target/deps/mathlib/src/data/finset/default.lean' or '/home/buzzard/test/real-number-game/_target/deps/mathlib/src/data/finset.lean'

Commit 351e7a41d24413ef1325be3bfa23805af2c42da4 of the real number game used a previous version of mathlib, namely mathlib commit 26918a05936335a46944c7a1fadeefcdb7224f97, where there was src/data/finset.lean. Current mathlib master has src/data/finset/basic.lean. leanproject get-mathlib-cache doesn't sort this out, and the import becomes ambiguous.

Why does this matter? Of course nobody does what I did above in practice. But here is what people do do; this is harder for me to demonstrate so I'll just describe what happens.

Me and collaborators work on real number game.
I decide to bump mathlib, so I do leanproject up, fix errors, and push.
Time passes, and mathlib moves on
A collaborator pulls RNG, and notices that leanpkg.toml has changed.
My collaborator types leanproject get-mathlib-cache -- they can't type leanproject up because mathlib master has moved.
My collaborator gets ambiguous import errors.

After leanproject get-mathlib-cache they will have finset.lean and finset/basic.lean in their _target/deps/mathlib (or possibly the oleans -- I can't remember -- but it is not the same as my _target/deps/mathlib. One fix is https://xkcd.com/1597/ (delete the project and then leanproject get again). All other fixes involve not using leanproject, and not using the VS Code interface to git/github either.

mathlib get-cache and similar should support fetching at specified hash

As discussed in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/get-mathlib-at-commit

Ideally, specifying a branch name, commit, or PR # in mathlib would update the mathlib dep to that target: do the git operations in the subfolder, fetch the oleans, and update the toml. If specifying a branch name where the top of the branch doesn't have oleans, optionally fall back to the latest commit that does, fetch that, and then git checkout the commit to which the branch points to. Similarly, maybe that is also valid for a target commit when specified by a hash.

SSH problems

the block of code at

mathlib-tools/mathlibtools/leanproject.py

Line 180 in 77c707e

try:

seems to exist to test whether an SSH URL (git@...) should be used to clone a project when the latter is given by name. But this test breaks the tool because my ssh_config is set to use a specific identity file for the github.com host, which paramiko does not seem to find automatically

I think perhaps https URLs should just be used as a default if a protocol is not specified, otherwise here is an alternative that does an ssh_config lookup but the user is potentially prompted twice for their key (once by paramiko, then again by git): mattearnshaw@a6193c7

`leanproject get` could create branches as well

I would really like leanproject get to be able to create new branches like this:

leanproject get mathlib:new_branch_name
cd mathlib_new_branch_name
# start working

Should this be another command? I can implement and PR this myself if you prefer, but I'd like to hear your thoughts first.

`leanproject` fails if the Lean project directory is not a Git repository

There are two related error cases:

When trying to build a Lean project that is not part of a Git repository, leanproject fails with Invalid git repository.
When trying to build a Lean project in a subfolder of a Git repository, leanproject fails with Missing leanpkg.toml. The --debug output indicates that it looks for leanpkg.toml in the Git repository's root directory.

To reproduce the first issue:

$ leanproject new test
$ cd test
$ rm -r .git
$ leanproject build

To reproduce the second issue:

$ mkdir repo
$ cd repo
$ git init
$ leanproject new test
$ cd test
$ rm -r .git
$ leanproject build

Tested with mathlibtools-0.0.5.

Mathlib build but not in the LEAN_PATH afterward [Windows]

Hi!

I was trying to play with logical verification 2019, however I ran into issues during the build process of Mathlib.

Trying to pinpoint the problem and reproduce it, I realized that I cannot even generate the tutorial:

$ leanproject get tutorials
Cloning from [email protected]:leanprover-community/tutorials.git
configuring tuto 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 182, done.
remote: Counting objects: 100% (182/182), done.
remote: Compressing objects: 100% (138/138), done.
remote: Total 48871 (delta 93), reused 87 (delta 44), pack-reused 48689
Receiving objects: 100% (48871/48871), 20.76 MiB | 2.76 MiB/s, done.
Resolving deltas: 100% (37626/37626), done.
> git checkout --detach 3710744b411550474ecf27d3c50d92156b5ffc95    # in directory _target/deps/mathlib
HEAD is now at 3710744b feat(meta/uchange): universe lifting and lowering in meta (#2627)
Looking for local mathlib oleans
Found local mathlib oleans

Then I ran into #46

$ cd tutorials
$ leanproject.exe up
[WinError 5] Access is denied: 'D:\\dev\\tmp\\tmp\\tutorials\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-7f4d731199a466a78ed1f930bd4d4b140a20c980.idx'

If instead of doing leanproject.exe up, I do:

rm -vfr tutorials
leanproject get tutorials
cd tutorials
leanproject.exe build

The command outputs something like:

Building project tuto
configuring tuto 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
mathlib: trying to update _target/deps/mathlib to revision 3710744b411550474ecf27d3c50d92156b5ffc95
> git checkout --detach 3710744b411550474ecf27d3c50d92156b5ffc95    # in directory _target/deps/mathlib
M	src/algebra/archimedean.lean
M	src/algebra/associated.lean
M	src/algebra/big_operators.lean
[...]
M	src/topology/uniform_space/separation.lean
M	src/topology/uniform_space/uniform_convergence.lean
M	src/topology/uniform_space/uniform_embedding.lean
HEAD is now at 3710744b feat(meta/uchange): universe lifting and lowering in meta (#2627)
> lean --make src/solutions
upper_bounds : set ?M_1 → set ?M_1
Try this: exact le_max_left (u N - x) (-(u N - x))
Try this: exact one_div_pos_of_pos this

Mathlib seems to build properly!
But then, in Visual Studio Code, all the "Solution" files have import errors for Mathlib, typically:

import data.real.basic
file 'data\real\basic' not found in the LEAN_PATH

If I try to build mathlib by hands, it seems to work:

$ cd _target/deps/mathlib/
$ leanpkg.exe upgrade
configuring mathlib 0.1

$ leanpkg.exe build
configuring mathlib 0.1
> lean --make src

OS: Windows 10
Terminal: Git Bash
VSCode is configured to use Git Bash as terminal
"terminal.external.windowsExec": "D:\\Program Files\\Git\\git-bash.exe",
VSCode has proper paths to lean

$ lean --version
Lean (version 3.11.0, commit fb3f3e88be8a, Release)

If I write at the first line of a solution file #eval 1+1, the goal says 2, so I assume VS find Lean properly.

If needed, I can test on a Linux machine, however, I will not be able to do all my projects on Linux.

hooks not set executable?

I didn't experience this the first time I installed, but on a new machine:

idaeus:mathlib scott$ leanproject hooks
This script will copy post-commit and post-checkout scripts to  /Users/scott/.git/modules/projects/lean/mathlib/hooks
Do you want to proceed (y/n)? y
Successfully copied scripts
idaeus:mathlib scott$ git checkout T50000
Already on 'T50000'
Your branch is up to date with 'origin/T50000'.
hint: The '/Users/scott/.git/modules/projects/lean/mathlib/hooks/post-checkout' hook was ignored because it's not set as executable.
hint: You can disable this warning with `git config advice.ignoredHook false`.
idaeus:mathlib scott$ chmod u+x /Users/scott/.git/modules/projects/lean/mathlib/hooks/post-checkout
idaeus:mathlib scott$ git checkout T50000
Already on 'T50000'
Your branch is up to date with 'origin/T50000'.
Trying to fetch cached olean
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/b95270e520cf26132156a4c04088613c14e26d7c.tar.gz to /Users/scott/.mathlib/b95270e520cf26132156a4c04088613c14e26d7c.tar.gz
...

`leanproject get tutorials` fails when run twice

$ leanproject get tutorials
...
$ leanproject get tutorials
Git command failed

It took me a bit to figure out that this is because the directory tutorials already exists.

macOS installer should suggest install steps for M1 users

Running brew install elan on an M1 mac (which install_macos.sh does) produces:

⊙  brew install elan-init                                                                                                                                                           julian@Airm
elan-init: The x86_64 architecture is required for this software.
Error: An unsatisfied requirement failed this build.

because we've marked elan as not supporting ARM (until/unless lean gets ARM binaries for macOS).

We likely should here emit some more specific instructions suggesting some alternate steps.

refactoring directory structure of mathlib can cause problems

Right now I can break my project-with-mathlib-as-a-dependency using leanproject:
In version 0.0.10:

$ leanproject get ImperialCollegeLondon/group-theory-game
...
Looking for local mathlib oleans
Found local mathlib oleans
$ cd group-theory-game
$ lean --make src/group/definitions.lean ## works fine. Note that master mathlib dependency is after the ring change.
$ git checkout Sylow_theorems ## branch from before the recent ring -> ring/basic mathlib change
$ leanproject get-mathlib-cache
Looking for local mathlib oleans
Found local mathlib oleans
$ lean --make src/group/definitions.lean
/home/buzzard/temp/group-theory-game/_target/deps/mathlib/src/algebra/field.lean:1:0: error: ambiguous import, it can be '/home/buzzard/temp/group-theory-game/_target/deps/mathlib/src/algebra/ring/default.lean' or '/home/buzzard/temp/group-theory-game/_target/deps/mathlib/src/algebra/ring.lean'
...

In the last few weeks, algebra/ring.lean was changed to algebra/ring/basic.lean in mathlib, but after leanproject get-mathlib-cache I have in _target copies of both ring.lean and ring/basic.lean and this leads to ambiguous imports in mathlib later down the line.

failure with old project

I deleted my local oleans for the perfectoid project, to see if leanproject get will install the perfectoid project correctly. It doesn't quite:

$ rm ~/.mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.gz
$ leanproject get lean-perfectoid-spaces
[snip: project clones correctly]
HEAD is now at 4e2c7e36 feat(topology/subset_properties): alternative definitions of irreducible and connected (#1970)
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.xz to /home/buzzard/.mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.xz
Trying to download https://oleanstorage.azureedge.net/mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.gz to /home/buzzard/.mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.gz
Trying to download https://oleanstorage.azureedge.net/mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.bz2 to /home/buzzard/.mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.bz2
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
Trying to download https://github.com/leanprover-community/mathlib-nightly/releases/download/nightly-2020-02-11/mathlib-olean-nightly-2020-02-11.tar.gz to /home/buzzard/.mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.gz
100%|████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 22.7M/22.7M [00:01<00:00, 16.5MiB/s]
Found GitHub mathlib oleans
[Errno 2] No such file or directory: '/home/buzzard/.mathlib/4e2c7e36308b6349c5a794237ebfef91e309ac2f.tar.bz2'

Amusingly, deleting the downloaded project and running leanproject get lean-perfectoid-spaces again works fine :-) The local tgz'ed oleans are unpacked no problem.

`leanproject get` should use SSH authentication if possible

Currently leanproject get foo uses the https connection for the github remote. This makes it hard to contribute.

leanproject get mathlib:some-branch
cd mathlib
git push

The last git push will then fail because git will push to https://github.com/..... The http url does not work if you have two-factor authentication enabled (I have to enable it since it is required by another project). The same issue also exists for non-mathlib projects, I've just chosen mathlib as an example.

It would be nice if leanproject could use the SSH url instead, if possible.

`toml` to `tomli` & `tomli_w` migration

Citing Michał Górny's comment on the Gentoo bugtracker (https://bugs.gentoo.org/878651):
"""
dev-python/toml has had its last release in 2020. It doesn't implement TOML 1.0 and it is buggy. With Python 3.11, we have a built-in tomllib module to handle reading TOML, and in general tomli/tomli-w pair to handle load/dump everywhere.

Useful resources:

https://projects.gentoo.org/python/guide/porting.html#replacing-the-toml-package
https://fedoraproject.org/wiki/Changes/DeprecatePythonToml
"""

I would like to begin work on this issue and submit a PR, but I also would like to have a confirmation this upstream wants to migrate away from the toml Python package.

look for xz archives first on Azure

We're now pushing xz archives to Azure alongside the gz ones: leanprover-community/mathlib#2719

These should be preferred by leanproject when available. To make the transition easier, we'll keep uploading both for a while.

I guess the relevant function is https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/lib.py#L141 but I'm not sure how modularized this is. I can add a few lines there and @PatrickMassot can tell me what I'm missing, or he can do it himself, either way!

`leanproject new` uses wrong branch

$ elan default 3.4.2
$ leanproject new project
$ cd project
$ git add . && git commit -m 'initial commit'
$ git branch
* lean-3.4.2
$ grep lean_version leanpkg.toml
lean_version = "leanprover-community/lean:3.6.1"

That is, the Lean version is 3.6.1 but the current branch is lean-3.4.2.

why are we still talking about branch 'lean-3.4.2'?

I just wrote leanproject new blah and at some point during the installation procedure I noticed that it checked out a branch called lean-3.4.2. That is, at best, confusing. Is there no way we can switch it off? I'd rather it checked out some fancy-sounding 3.23 branch, if I'm a nervous first time user.

access denied in update-mathlib

I was troubleshooting update-mathlib for someone else, because they got an error when extracting the compiled files. It turned out that the tar.gz file had a (plain text) message containing "Access Denied", and also something to do with timeout.

Presumably when downloading the files, the website timed out (maybe due to losing internet for a while), and this error message was written to the tar.gz file.

This error message should not be written to the tar.gz file, because when running update-mathlib again, the code will just use this corrupted file instead of trying to download again.

error: "argument of type 'PosixPath' is not iterable"

Hey! I'm getting the error in the title whenever I try to run a leanproject command. For instance:

$ leanproject new test
> mkdir -p test
> cd test
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring test 0.1
argument of type 'PosixPath' is not iterable

$ leanproject get mathlib
Cloning from [email protected]:leanprover-community/mathlib.git
argument of type 'PosixPath' is not iterable

This is with mathlibtools-0.0.3 installed via pip (python3.6). I don't know what might be causing this, but I'll be happy to provide any additional info you might need for debugging.

Missing / inconsistent version tags

Versions 0.04, 0.07, 0.0.8, 0.0.9 are tagged (the latter two as v0.0.8 and v0.0.9). But there is no tag for v1.0.0. Presumably this commit should be tagged as v1.0.0 (although, confusingly, the Changelog says 1.0.1).

Consistent tagging is useful for tools which monitor upstream repos (e.g. Debian watch ) when source tarballs are not published on GitHub.

[email protected] has a dependency on numpy, but pip doesn't install it automatically

arguta:mathlib scott$ 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.7/site-packages/mathlibtools/leanproject.py", line 20, in <module>
    from mathlibtools.lib import (LeanProject, log, LeanDirtyRepo,
  File "/usr/local/lib/python3.7/site-packages/mathlibtools/lib.py", line 16, in <module>
    import networkx as nx # type: ignore
  File "/usr/local/lib/python3.7/site-packages/networkx/__init__.py", line 115, in <module>
    import networkx.readwrite
  File "/usr/local/lib/python3.7/site-packages/networkx/readwrite/__init__.py", line 15, in <module>
    from networkx.readwrite.graphml import *
  File "/usr/local/lib/python3.7/site-packages/networkx/readwrite/graphml.py", line 314, in <module>
    class GraphML(object):
  File "/usr/local/lib/python3.7/site-packages/networkx/readwrite/graphml.py", line 344, in GraphML
    types = [(np.float64, "float"), (np.float32, "float"),
AttributeError: module 'numpy' has no attribute 'float64'
arguta:mathlib scott$ pip3 install numpy
Collecting numpy
  Downloading numpy-1.18.4-cp37-cp37m-macosx_10_9_x86_64.whl (15.1 MB)
     |████████████████████████████████| 15.1 MB 3.1 MB/s 
Installing collected packages: numpy
Successfully installed numpy-1.18.4
arguta:mathlib scott$ leanproject up

(success!)

`leanproject up` should call `leanpkg configure`

It's easy to forget to call leanpkg configure if you're cloning mathlib and then run leanproject up.

Support looking for leanpkg.toml in cwd

An example of the use case is https://github.com/leanprover-community/format_lean . The lean project is not at the root of the Git repo, so the current logic which looks for leanpkg.toml at the root of the git repo would not apply. The error log can be found here.

I attempted to solve this at utensil-contrib@b2e1641 .

The olean cache was found but something went wrong afterward, it seems to still somehow depend on git related stuff, the error log can be found here when I was trying to add Github Actions CI for https://github.com/leanprover-community/format_lean .

permissions problems with `leanproject up` on Windows

On Windows, running leanproject up on a Lean package that was created with leanpkg (not leanproject) may result in a permission error like the following:

[WinError 5] Access is denied: 'C:\\path\\to\\some_lean_project\\_target\\deps\\mathlib\\.git\\objects\\XX\\some_long_hash'

The solution is to delete the _target folder and then retry leanproject up.

See this Zulip thread.

Execute permission on cache-olean

Doing a fresh curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash gives me a working update-mathlib but cache-olean and setup-lean-git-hooks both lack the x permission. Of course I can add this to the install script but I'd prefer to understand where the difference comes from.

leanproject up access is denied

Error:

PermissionError: [WinError 5] Access is denied: 'C:\\some-repo\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-36f591561703d876c8ad32e4cc46887e2a0bf6d2.idx'

Environment: VSCode Terminal on Windows 10, in some repo that uses mathlib.

Reproduction:

leanproject up
leanproject up

Debug:

Traceback (most recent call last):
  File "c:\python-3.6.4\lib\runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "c:\python-3.6.4\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Python-3.6.4\Scripts\leanproject.exe\__main__.py", line 7, in <module>
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 256, in safe_cli
    handle_exception(err, str(err))
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 51, in handle_exception
    raise exc
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 254, in safe_cli
    cli()
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 829, in __call__
    return self.main(*args, **kwargs)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 782, in main
    rv = self.invoke(ctx)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 1259, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 1066, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 610, in invoke
    return callback(*args, **kwargs)
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 92, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\lib.py", line 468, in upgrade_mathlib
    shutil.rmtree(str(self.mathlib_folder))
  File "c:\python-3.6.4\lib\shutil.py", line 494, in rmtree
    return _rmtree_unsafe(path, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 389, in _rmtree_unsafe
    onerror(os.unlink, fullname, sys.exc_info())
  File "c:\python-3.6.4\lib\shutil.py", line 387, in _rmtree_unsafe
    os.unlink(fullname)
PermissionError: [WinError 5] Access is denied: 'C:\\some-repo\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-36f591561703d876c8ad32e4cc46887e2a0bf6d2.idx'

For example: https://github.com/kckennylau/test

Should `leanproject get` support branches?

I typically have one directory per mathlib branch, so it would be nice to get mathlib and immediately check out a given branch.

$ leanproject get mathlib:mon_loc

leanprover-community / mathlib-tools Goto Github PK

mathlib-tools's Introduction

mathlib-tools

Installation

Released version

pipx

macOS

NixOS