Comments (3)
PatrickMassot
commented on July 17, 2024
leanpkg has the standing assumption that your elan setup is sane. I don't see I could fix that issue, except for hiding the python Traceback.
from mathlib-tools.
gebner
commented on July 17, 2024
Most of the leanproject commands don't care about the default lean version set in elan. They all use the version specified in the leanpkg.toml of the current project.
I wonder how many of our users have set 3.4.0 as the default lean version from when they first installed elan. For them leanproject new will fail as well:
$ elan default 3.4.0
$ leanproject new foo
...
mathlibtools.lib.InvalidMathlibProject: This project does not depend on mathlib
from mathlib-tools.
PatrickMassot
commented on July 17, 2024
Fixed in 7f0216d.
from mathlib-tools.
Related Issues (20)
- Missing / inconsistent version tags HOT 1
- macOS installer should suggest install steps for M1 users HOT 3
- Make a longest-pole script HOT 1
- 'leanproject new' fails with lean 4 installed HOT 2
- `toml` to `tomli` & `tomli_w` migration HOT 6
- [email protected] has a dependency on numpy, but pip doesn't install it automatically HOT 6
- import-graph dot file HOT 1
- clean up git after leanproject get-mathlib-cache HOT 5
- permissions problems with `leanproject up` on Windows HOT 3
- Interrupting download leaves corrupted archive behind HOT 1
- Support looking for leanpkg.toml in cwd HOT 1
- failure with old project
- leanproject get-mathlib-cache doesn't tidy up after itself HOT 1
- SSH problems HOT 5
- leanproject hooks scripts are out of date HOT 2
- refactoring directory structure of mathlib can cause problems HOT 1
- mathlib get-cache and similar should support fetching at specified hash HOT 1
- `elan` is not on $PATH in gnome-terminal HOT 2
- why are we still talking about branch 'lean-3.4.2'? HOT 3
- MacOS brew update of Python breaks leanproject HOT 7
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from mathlib-tools.