void-packages
void-packages copied to clipboard
[WIP] New package: mathlibtools-1.1.1
Testing the changes
- I tested the changes in this PR: briefly
New package
- This new package conforms to the quality requirements: YES
Local build testing
- I built this PR locally for my native architecture, x86-64
I don't know how to make this work:
- Install
elan
following the instructions from https://leanprover-community.github.io/install/linux.html - run
source $HOME/.elan/env
- Install
mathlibtools
from this template
This is the output of leanproject get tutorials
Cloning from [email protected]:leanprover-community/tutorials.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/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
S'està clonant a «_target/deps/mathlib»...
remote: Enumerating objects: 291798, done.
remote: Counting objects: 100% (2157/2157), done.
remote: Compressing objects: 100% (856/856), done.
remote: Total 291798 (delta 1612), reused 1701 (delta 1301), pack-reused 289641
S'estan rebent objectes: 100% (291798/291798), 155.86 MiB | 4.56 MiB/s, fet.
S'estan resolent les diferències: 100% (233183/233183), fet.
> git checkout --detach 178456ffefddf80dec3b26262cebc88c596e4969 # in directory _target/deps/mathlib
HEAD ara és a 178456ffef feat(set_theory/surreal/basic): definition of `≤` and `<` on numeric games (#14169)
Looking for mathlib oleans for 178456ffef
locally...
Found local mathlib oleans
Located matching cache
Applying cache
files extracted: 1 [00:00, 228.29/s]
Aborted!
I don't know what is happening. It should download the cached oleans.
Update: This also happens with mathlibtools installed from pipx...
This error also appears when running leanproject get leanprover-community/tutorials
. Maybe the repo https://github.com/leanprover-community/tutorials has some problem...
Using leanproject get mmasdeu/topologygame
everything works as expected. After following the steps mentioned above, opening the cloned repo in vscode and installing the lean extension, it loads the cached oleans instantly.
So I think that this package works ok.
Should I rename this package to pyhon3-mathlibtools
?
The version here is 1.3.0: https://pypi.org/project/mathlibtools/ but the version in the github repo is 1.2.0: https://github.com/leanprover-community/mathlib-tools/tags
What should I do?
The tests fail with FileNotFoundError: [Errno 2] No such file or directory: 'leanproject'
However when I install the package locally I get leanproject installed. What's happening?
Pull Requests become stale 90 days after last activity and are closed 14 days after that. If this pull request is still relevant bump it or assign it.
Pull Requests become stale 90 days after last activity and are closed 14 days after that. If this pull request is still relevant bump it or assign it.