Zulip Chat Archive
Stream: new members
Topic: leanproject issues
Aniruddh Agarwal (Apr 23 2020 at 23:57):
Hello,
I'm trying to use "leanproject get <github repo>" to pull a project from github, but I'm getting this error:
... Looking for GitHub mathlib oleans Info: No github section found in 'git config', we will use GitHub with no authentication 403 {"message": "API rate limit exceeded for 73.144.197.24. (But here's the good news: Authenticated requests get a higher rate limit. Check out the documentation for more details.)", "documentation_url": "https://developer.github.com/v3/#rate-limiting"}
Can someone help me fix this? BTW I use SSH to normally communicate with Github.
Alex J. Best (Apr 24 2020 at 00:00):
Aniruddh Agarwal (Apr 24 2020 at 00:02):
Thank you!
Ashvni Narayanan (Jun 23 2020 at 13:44):
I just run
leanproject up
and now I suddenly have 23 errors in my code.
Any help is appreciated. Thank you!
Reid Barton (Jun 23 2020 at 13:50):
I suggest trying to fix the first error, then rebuilding and repeating until there are no more errors!
Johan Commelin (Jun 23 2020 at 13:53):
@Ashvni Narayanan That's probably because Kevin refactored PID's
Johan Commelin (Jun 23 2020 at 13:53):
I hope that things will actually be easier now
Ashvni Narayanan (Jun 23 2020 at 13:57):
Ah I see. The code is unchanged :
import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization
universe u
class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=
The first two errors are
Test.lean:9:51: error
unknown identifier 'principal_ideal_domain'
Test.lean:9:51: error
invalid 'structure', expression must be a 'parent' structure
How do I call things that are not parent structures?
Kevin Buzzard (Jun 23 2020 at 14:00):
The super-cool way to do this sort of thing would be to update mathlib on a branch. This sort of breakage is inevitable because I am messing with code which you're using.
That line now should look something like
class discrete_valuation_ring (R : Type u) [integral_domain R] [is_principal_ideal_domain R] :=
Patrick Massot (Jun 23 2020 at 14:04):
Ashvni, this is expected. mathlib is moving very fast and lot of refactoring happens. leanproject up is not only about getting new toys, you need to be prepared for breakage from times to times.
Ashvni Narayanan (Jun 23 2020 at 14:09):
Yes, I understand. Hopefully I will get used to it soon!
Last updated: Dec 20 2023 at 11:08 UTC