Zulip Chat Archive

Stream: new members

Topic: leanproject up


view this post on Zulip James Arthur (Jan 09 2021 at 01:34):

I seem to be getting a weird error on leanproject up, everything is installed properly and has worked thus far but now gives me,

C:\Users\james\Documents\LEAN\circ-area>leanproject up
[WinError 5] Access is denied: 'C:\\Users\\james\\Documents\\LEAN\\circ-area\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-b1b592db29a3c303ea91b490161bc8ac769f1fec.idx'

Is this a known issue and has some fix?

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2021 at 01:38):

What version of leanproject are you using? There was a similar error message here but I think the issue was fixed.

view this post on Zulip James Arthur (Jan 09 2021 at 01:39):

Bryan Gin-ge Chen said:

What version of leanproject are you using? There was a similar error message here but I think the issue was fixed.

leanproject, version 0.0.6

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2021 at 01:40):

The latest version is 1.0.0, so you could try updating and seeing if there's still a problem.

view this post on Zulip James Arthur (Jan 09 2021 at 01:41):

How do I update leanproject? Is there a command?

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2021 at 01:44):

pip install --upgrade mathlibtools should work, though depending on your Python environment you might have to do some other things.

view this post on Zulip James Arthur (Jan 09 2021 at 01:46):

I can't quite remember how I installed Lean but I remember it being a massive pain in the behind, I shall try and go and work out what command to run :rofl:

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2021 at 01:51):

I gave the wrong command before, sorry about that. Try pip install --upgrade mathlibtools if you haven't already.

view this post on Zulip James Arthur (Jan 09 2021 at 01:59):

Bryan Gin-ge Chen said:

I gave the wrong command before, sorry about that. Try pip install --upgrade mathlibtools if you haven't already.

It worked! Thankyou


Last updated: May 11 2021 at 00:31 UTC