## 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):

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

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: May 13 2021 at 06:15 UTC