Zulip Chat Archive

Stream: general

Topic: leanproject access denied

Kenny Lau (Apr 30 2020 at 13:46):

C:\some-repo> leanproject up
[WinError 5] Access is denied: 'C:\\some-repo\\_target\\deps\\mathlib\\.git\\objects\\82\\8911039fff7d6ef90ccd33eac0dbe03764acc8'

Johan Commelin (Apr 30 2020 at 13:47):

Maybe try leanproject down? /s

Johan Commelin (Apr 30 2020 at 13:47):

Do you have read/write access to that file?

Johan Commelin (Apr 30 2020 at 13:48):

As in, can you verify this using other means?

Kenny Lau (Apr 30 2020 at 13:49):

well I can open it in NotePad++

Kenny Lau (Apr 30 2020 at 13:50):

and I can cat it in the same terminal

Johan Commelin (Apr 30 2020 at 13:52):

Weird...

Kevin Buzzard (Apr 30 2020 at 13:52):

Can you edit it or is it read only?

Steffan (Apr 30 2020 at 13:53):

open command prompt as administrator

Steffan (Apr 30 2020 at 13:53):

then try again?

Steffan (Apr 30 2020 at 13:54):

delete .git folder and try again, maybe?

Kevin Buzzard (Apr 30 2020 at 13:57):

The risk with that is that you lose all your local branches

Kevin Buzzard (Apr 30 2020 at 13:57):

When I've seen errors like that before it's been stuff like disk corruption

Steffan (Apr 30 2020 at 13:57):

Yes, but if you don't care about git so much, like me

Kenny Lau (Apr 30 2020 at 13:58):

very interestingly, renaming it to .git_old doesn't help, but moving it to another place made it work

Kenny Lau (Apr 30 2020 at 13:58):

it was very strange: after I rename it to .git_old it gives me the same error message with .git replaced with .git_old

Steffan (Apr 30 2020 at 13:58):

what if you take the . off?

Kevin Buzzard (Apr 30 2020 at 13:59):

When I've seen copying stuff to other places fixing things, it has been disk corruption

Kenny Lau (May 01 2020 at 10:06):

I have reproduced this error

Kenny Lau (May 01 2020 at 10:06):

  1. delete the .git folder
  2. leanproject up
  3. this works fine, and it clones mathlib
  4. leanproject up
  5. error

Kenny Lau (May 01 2020 at 10:06):

so basically it cannot be executed twice

Kevin Buzzard (May 01 2020 at 10:08):

Open an issue in the GitHub repo and Patrick will look at it when he has time. Nice sleuthing.

Kenny Lau (May 01 2020 at 10:09):

the environment is in the VSCode Terminal on Windows 10

Kenny Lau (May 01 2020 at 10:09):

which uses powershell

Kenny Lau (May 01 2020 at 10:11):

debug:

Traceback (most recent call last):
  File "c:\python-3.6.4\lib\runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "c:\python-3.6.4\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Python-3.6.4\Scripts\leanproject.exe\__main__.py", line 7, in <module>
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 256, in safe_cli
    handle_exception(err, str(err))
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 51, in handle_exception
    raise exc
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 254, in safe_cli
    cli()
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 829, in __call__
    return self.main(*args, **kwargs)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 782, in main
    rv = self.invoke(ctx)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 1259, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 1066, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 610, in invoke
    return callback(*args, **kwargs)
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 92, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\lib.py", line 468, in upgrade_mathlib
    shutil.rmtree(str(self.mathlib_folder))
  File "c:\python-3.6.4\lib\shutil.py", line 494, in rmtree
    return _rmtree_unsafe(path, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 389, in _rmtree_unsafe
    onerror(os.unlink, fullname, sys.exc_info())
  File "c:\python-3.6.4\lib\shutil.py", line 387, in _rmtree_unsafe
    os.unlink(fullname)
PermissionError: [WinError 5] Access is denied: 'C:\\some-repo\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-36f591561703d876c8ad32e4cc46887e2a0bf6d2.idx'

Kenny Lau (May 01 2020 at 10:14):

https://github.com/leanprover-community/mathlib-tools/issues/46

Sebastien Gouezel (May 01 2020 at 10:23):

I tried to reproduce, but you need to give more details. Here is what I did, in a folder containing a cloned copy of mathlib: I deleted the .git folder, and then I ran leanproject up several times. The output is

PS C:\Users\Sebastien\Desktop\mathlib_klau> leanproject up
'dependencies'
PS C:\Users\Sebastien\Desktop\mathlib_klau> leanproject up
'dependencies'
PS C:\Users\Sebastien\Desktop\mathlib_klau> leanproject up
'dependencies'

It doesn't create a .git folder. I am not surprised it doesn't work, because leanproject up is supposed to use .git.

Kenny Lau (May 01 2020 at 10:24):

I should specify that this is in a repo using mathlib

Sebastien Gouezel (May 01 2020 at 10:29):

This is still not enough for me. Details that you did not specify: is mathlib in a different directory with its own git structure, or is it in a subdirectory of your project, what does the .toml look like, and so on. Ideally, I would just have a github branch to clone, and then I could start experimenting.

Kenny Lau (May 01 2020 at 10:38):

@Sebastien Gouezel https://github.com/kckennylau/test

Johan Commelin (May 01 2020 at 10:58):

Kenny Lau said:

Sebastien Gouezel https://github.com/kckennylau/test

I cloned your repo. leanproject up feels a bit slow when i run it (compared to when I run in mathlib). But it succeeds. Same when I run the command a 2nd time.

Rob Lewis (May 01 2020 at 11:17):

FWIW I can reproduce this on Windows, both Powershell and Git Bash. Running Powershell as admin doesn't fix it, I don't immediately see an issue with the file permissions, I don't see a process blocking write access to that file. Out of time to troubleshoot further right now though.

Kenny Lau (May 01 2020 at 11:21):

@Rob Lewis thanks for your reproduction.

Sebastien Gouezel (May 01 2020 at 12:30):

I am doing something wrong:

PS C:\Users\Sebastien\Desktop\essai> leanproject --version
leanproject, version 0.0.5
PS C:\Users\Sebastien\Desktop\essai> git clone https://github.com/kckennylau/test.git
Cloning into 'test'...
remote: Enumerating objects: 6, done.
remote: Counting objects: 100% (6/6), done.
remote: Compressing objects: 100% (3/3), done.
remote: Total 6 (delta 0), reused 6 (delta 0), pack-reused 0
Unpacking objects: 100% (6/6), done.
PS C:\Users\Sebastien\Desktop\essai> cd test
PS C:\Users\Sebastien\Desktop\essai\test> leanproject up
[WinError 2] Le fichier spécifié est introuvable

Patrick Massot (May 01 2020 at 12:36):

This is really windows specific. I couldn't reproduce here.

Patrick Massot (May 01 2020 at 12:36):

Did you try leanproject --debug up?

Sebastien Gouezel (May 01 2020 at 12:38):

Are you asking Kenny or me?

For me, I get

PS C:\Users\Sebastien\Desktop\essai\test> leanproject --debug up
Traceback (most recent call last):
  File "C:\Program Files\Python37\Scripts\leanproject-script.py", line 11, in <module>
    load_entry_point('mathlibtools==0.0.5', 'console_scripts', 'leanproject')()
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 295, in safe_cli
    handle_exception(err, str(err))
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 51, in handle_exception
    raise exc
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 293, in safe_cli
    cli()
  File "c:\program files\python37\lib\site-packages\click\core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "c:\program files\python37\lib\site-packages\click\core.py", line 717, in main
    rv = self.invoke(ctx)
  File "c:\program files\python37\lib\site-packages\click\core.py", line 1137, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\program files\python37\lib\site-packages\click\core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\program files\python37\lib\site-packages\click\core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 93, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "c:\program files\python37\lib\site-packages\mathlibtools\lib.py", line 592, in upgrade_mathlib
    self.run(['leanpkg', 'upgrade'])
  File "c:\program files\python37\lib\site-packages\mathlibtools\lib.py", line 528, in run
    check=True).stdout.decode()
  File "c:\program files\python37\lib\subprocess.py", line 472, in run
    with Popen(*popenargs, **kwargs) as process:
  File "c:\program files\python37\lib\subprocess.py", line 775, in __init__
    restore_signals, start_new_session)
  File "c:\program files\python37\lib\subprocess.py", line 1178, in _execute_child
    startupinfo)
FileNotFoundError: [WinError 2] Le fichier spécifié est introuvable

But I want to stress that, for my usual case (leanproject up in a mathlib directory), everything works perfectly.

Kenny Lau (May 01 2020 at 13:29):

@Patrick Massot I have produced the output of leanproject --debug up in the issue

Patrick Massot (May 01 2020 at 14:19):

It fails to remove files in the mathlib folder. What happens if you try to remove it by hand?

Kenny Lau (May 01 2020 at 14:32):

if I remove the .git folder then leanproject up does work, but only once

Rob Lewis (May 06 2020 at 09:02):

I just ran into this in practice. The .idx file does indeed seem to be read-only, which prevents shutil.rmtree from deleting it.

Rob Lewis (May 06 2020 at 09:02):

One workaround: https://stackoverflow.com/questions/21261132/shutil-rmtree-to-remove-readonly-files although blindly deleting read-only stuff is maybe not the smartest thing to do.

Patrick Massot (May 06 2020 at 09:05):

What is this .idx file?

Patrick Massot (May 06 2020 at 09:05):

Oh, in git?

Patrick Massot (May 06 2020 at 09:05):

Windows is so weird

Rob Lewis (May 06 2020 at 09:06):

robyl@DESKTOP-SMPP1GQ MINGW64 /d/lean/doc-gen (master)
$ leanproject up
[WinError 5] Access is denied: 'D:\\lean\\doc-gen\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-1be031bb56944e0cd6652e34e4ab97cadbe780f9.idx'

Patrick Massot (May 06 2020 at 09:06):

If this is only .idx files in .git we can have a rule for them instead of blindly deleting read-only files

Patrick Massot (May 06 2020 at 09:07):

Feel free to submit a patch to leanproject.

Kenny Lau (May 25 2020 at 09:33):

workaround seems to be to execute leanproject up inside _target/deps/mathlib

Kenny Lau (May 25 2020 at 09:33):

push: https://github.com/leanprover-community/mathlib-tools/issues/46

Kevin Buzzard (May 25 2020 at 09:57):

If you do that then you should probably manually edit the leanpkg.toml in your repo so it correctly reports which mathlib commit it's using

Patrick Massot (May 25 2020 at 12:44):

Kenny Lau said:

workaround seems to be to execute leanproject up inside _target/deps/mathlib

No, this is not at all a workaround.

Patrick Massot (May 25 2020 at 12:59):

I blindly tried to push a workaround to the winbug branch, but I need Windows users to test it.

Reid Barton (May 25 2020 at 13:04):

(it's just a patch that installs linux)

Kenny Lau (May 25 2020 at 13:10):

@Patrick Massot how do I test it?

Patrick Massot (May 25 2020 at 13:13):

git clone the repo, git checkout winbug, pip install . and try to use leanproject as usual

Kenny Lau (May 25 2020 at 13:14):

but how do I differentiate between the two different leanprojects?

Kenny Lau (May 25 2020 at 13:14):

if I want to switch back to the original one do I pip install mathlibtools?

Patrick Massot (May 25 2020 at 13:16):

yes

Patrick Massot (May 25 2020 at 13:16):

pip installing the clone repo will overwrite your install, but you can switch back as you wrote

Patrick Massot (May 25 2020 at 13:17):

Also, if you help enough then we can hopefully fix it today and it will become the official version

Kenny Lau (May 25 2020 at 13:28):

Traceback (most recent call last):
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\Scripts\leanproject.exe\__main__.py", line 7, in <module>
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\mathlibtools\leanproject.py", line 308, in safe_cli
    handle_exception(err, str(err))
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\mathlibtools\leanproject.py", line 58, in handle_exception
    raise exc
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\mathlibtools\leanproject.py", line 306, in safe_cli
    cli() # pylint: disable=no-value-for-parameter
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\click\core.py", line 829, in __call__
    return self.main(*args, **kwargs)
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\click\core.py", line 782, in main
    rv = self.invoke(ctx)
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\click\core.py", line 1259, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\click\core.py", line 1066, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\click\core.py", line 610, in invoke
    return callback(*args, **kwargs)
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\mathlibtools\leanproject.py", line 100, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\site-packages\mathlibtools\lib.py", line 598, in upgrade_mathlib
    shutil.rmtree(str(self.mathlib_folder))
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\shutil.py", line 516, in
rmtree
    return _rmtree_unsafe(path, onerror)
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\shutil.py", line 395, in
_rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\shutil.py", line 395, in
_rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\shutil.py", line 395, in
_rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\shutil.py", line 400, in
_rmtree_unsafe
    onerror(os.unlink, fullname, sys.exc_info())
  File "C:\Program Files\WindowsApps\PythonSoftwareFoundation.Python.3.7_3.7.2032.0_x64__qbz5n2kfra8p0\lib\shutil.py", line 398, in
_rmtree_unsafe
    os.unlink(fullname)
PermissionError: [WinError 5] Access is denied: 'C:\\[repo]\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-49c3746f3db30550d71ee61c3234d10c6308216c.pack'

Patrick Massot (May 25 2020 at 13:30):

Try to replace *.idx by * at https://github.com/leanprover-community/mathlib-tools/commit/6e06675add7a35228e2b81d9eb11a2e510ade538#diff-a97f9d481b2b8a9dffffdebc0e0de1d1R595

Kenny Lau (May 25 2020 at 13:35):

also how do I tell pip to not install it in a deep directory?

Kenny Lau (May 25 2020 at 13:35):

as in, not C:\Users\Kenny Lau\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.7_qbz5n2kfra8p0\LocalCache\local-packages\Python37\Scripts\leanproject.exe

Patrick Massot (May 25 2020 at 13:35):

pip install -e .

Patrick Massot (May 25 2020 at 13:35):

but it shouldn't matter

Patrick Massot (May 25 2020 at 13:35):

why do you need to access this install path at all?

Kenny Lau (May 25 2020 at 13:36):

because pip told me that pip installed it there and it is not in PATH

Patrick Massot (May 25 2020 at 13:37):

Then your system is broken

Kenny Lau (May 25 2020 at 13:38):

  File "c:\python-3.6.4\lib\runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "c:\python-3.6.4\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Python-3.6.4\Scripts\leanproject.exe\__main__.py", line 7, in <module>
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 256, in safe_cli
    handle_exception(err, str(err))
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 51, in handle_exception
    raise exc
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 254, in safe_cli
    cli()
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 829, in __call__
    return self.main(*args, **kwargs)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 782, in main
    rv = self.invoke(ctx)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 1259, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 1066, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\python-3.6.4\lib\site-packages\click\core.py", line 610, in invoke
    return callback(*args, **kwargs)
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\leanproject.py", line 92, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "c:\python-3.6.4\lib\site-packages\mathlibtools\lib.py", line 468, in upgrade_mathlib
    shutil.rmtree(str(self.mathlib_folder))
  File "c:\python-3.6.4\lib\shutil.py", line 494, in rmtree
    return _rmtree_unsafe(path, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 384, in _rmtree_unsafe
    _rmtree_unsafe(fullname, onerror)
  File "c:\python-3.6.4\lib\shutil.py", line 389, in _rmtree_unsafe
    onerror(os.unlink, fullname, sys.exc_info())
  File "c:\python-3.6.4\lib\shutil.py", line 387, in _rmtree_unsafe
    os.unlink(fullname)
PermissionError: [WinError 5] Access is denied: 'C:\\[repo]\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-49c3746f3db30550d71ee61c3234d10c6308216c.pack'

Patrick Massot (May 25 2020 at 13:38):

https://www.pcmag.com/how-to/how-to-make-the-switch-from-windows-to-linux

Patrick Massot (May 25 2020 at 13:39):

Are you sure you modified that line?

Patrick Massot (May 25 2020 at 13:40):

And rerun pip install if you didn't use -e in the first place

Kenny Lau (May 25 2020 at 13:41):

pip doesn't tell me this time where it installed mathlibtools in

Kenny Lau (May 25 2020 at 13:41):

so I assumed it's in PATH

Kenny Lau (May 25 2020 at 13:44):

maybe I shouldn't use -e to make sure

Patrick Massot (May 25 2020 at 13:45):

Honestly I don't understand how it can be that slow to iterate on this. But I'm not used to Windows hell

Kenny Lau (May 25 2020 at 13:46):

hey it worked!

Patrick Massot (May 25 2020 at 13:49):

Great

Patrick Massot (May 25 2020 at 13:49):

I'll push this fix

Patrick Massot (May 25 2020 at 13:55):

This is now live on pypi. You can update your official copy using pip install --update mathlibtools

Kenny Lau (May 25 2020 at 14:00):

why does it keep installing in a remote path

Last updated: Dec 20 2023 at 11:08 UTC