Zulip Chat Archive

Stream: new members

Topic: leanproject issues


view this post on Zulip 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.

view this post on Zulip Alex J. Best (Apr 24 2020 at 00:00):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cache-olean.20and.20authentication/near/188797478

view this post on Zulip Aniruddh Agarwal (Apr 24 2020 at 00:02):

Thank you!

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Jun 23 2020 at 13:53):

@Ashvni Narayanan That's probably because Kevin refactored PID's

view this post on Zulip Johan Commelin (Jun 23 2020 at 13:53):

I hope that things will actually be easier now

view this post on Zulip 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?

view this post on Zulip 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] :=

view this post on Zulip 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.

view this post on Zulip Ashvni Narayanan (Jun 23 2020 at 14:09):

Yes, I understand. Hopefully I will get used to it soon!


Last updated: May 13 2021 at 06:15 UTC