leanproject up

Stream: new members

[James Arthur]

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?

[Bryan Gin-ge Chen]

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

[James Arthur]

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

[Bryan Gin-ge Chen]

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

[James Arthur]

How do I update leanproject? Is there a command?

[Bryan Gin-ge Chen]

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

[James Arthur]

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:

[Bryan Gin-ge Chen]

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

[James Arthur]

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