failed to delete .olean

Stream: lean4

[Jovan Gerbscheid]

I'm on a new laptop, and run into the following issue: I'm working in B.lean which imports A.lean. I then make a change in A.lean and reload B.lean. Then I get this error:

error: stderr:
failed to delete '.\build\lib\A.olean': 5

I can manually delete the oleans, but that is quite inconvenient. (When I do so, it tells me I can't move them to the bin, but have to permanently delete them instead). Is there a fix?

[Kevin Buzzard]

What is your OS?

[Mario Carneiro]

windows

[Mario Carneiro]

the error message is ERROR_ACCESS_DENIED, so this means your folder is write-protected or the process was not run with enough permission to modify the folder

[Jovan Gerbscheid]

Thanks, the folder was indeed set to read-only