git issue: 2367 changed files

Stream: general

[Damiano Testa]

Dear All,

I installed Lean and mathlib on a new computer, made PR #11567 in which I thought that I changed only one file (algebra/pointwise.lean) and found that the PR mentions 2367 changed files, the first few of which are empty. What have I done wrong? How can I fix this?

Thank you!

[Henrik Böving]

As we can see from the file list: https://github.com/leanprover-community/mathlib/pull/11567/files it appears that you changed the permission of a ton of files from 644 to 755 for some reason (Maybe accidentally?). You'd have to undo these permission changes. (Do you know what UNIX file permission are and how they work?)

[Eric Wieser]

Sometimes this can be due to a weird filesystem configuration (such as the windows filesystem when viewed from inside WSL) - what platform are you doing this on?

[Damiano Testa]

I am on a university-managed machine that runs CentOS

[Damiano Testa]

I have certainly not changed permissions intentionally, but the change might be some "standard security measure" in place at the university.

[Henrik Böving]

Ehhh actually these permission changes made the files rather more open than more secure :p 644 was: owner can read and write, group can read, other can read, 755 is owner can write read and execute, group can read and execute everyone else can read and execute

[Johan Commelin]

644 → 755 sounds like adding the executable flag. Didn't we even have a linter against this?
git ls-files | grep '[.]lean$' | xargs chmod a-x should fix this.

[Henrik Böving]

Sounds to me like someone did a chmod +x on the repo

[Damiano Testa]

I have certainly not typed by mistake chmod +x. I changed no permissions with chmod...

[Damiano Testa]

I have no idea why this happened, but I am now pushing Johan's suggestion.

[Damiano Testa]

Now I am down to 74 changed files!!

[Damiano Testa]

a huge improvement!

[Damiano Testa]

Johan Commelin said:

644 → 755 sounds like adding the executable flag. Didn't we even have a linter against this?

Oh, the linter was not happy...

[Johan Commelin]

I guess you can run the same command but grepping for [.]md$'

[Johan Commelin]

That should take care of a whole lot of other files.

[Johan Commelin]

What you want to avoid is taking away the executable bit from some stuff in scripts/. But apart from that, I think nothing should have +x.

[Damiano Testa]

ok, I am getting the hang of this. I will try to fix this and hope that this is a one-time-fix and it never happens again

[Johan Commelin]

It might even be easier to do grep -v '[.]sh$'

[Damiano Testa]

ok, this is converging, just 3 .py files to go!

[Johan Commelin]

yeah, for those you need to add the +x back. So chmod a+x them.

[Damiano Testa]

Ok, I am almost done, but I need to teach! I will get back to this, but I think that I can take it from here: thank you all very much!

[Damiano Testa]

I thought that I was getting it, but the remaining files challenge me more. I tried to change the permissions of scripts/detect_errors.py and scripts/yaml_check.py but Git gives the error:

> git add -A -- /home/maskal/Lean/mathlib/scripts/yaml_check.py
error: open("scripts/yaml_check.py"): Permission denied
error: unable to index file scripts/yaml_check.py
fatal: updating files failed

Does anyone know what I should do?

[Yaël Dillies]

Btw Damiano have a look at #11486! It's likely gonna conflict with yours.

[Damiano Testa]

Yael (can't find the trema on this keyboard), thank you for the head-up! Once I manage to solve the permissions issue, I will try to merge the other branch into this one and see how it goes!

[Yaël Dillies]

Actually, looking at yours more closely, it seems you're modifying the one bit of the file I didn't touch, so it will likely be fine!

[Damiano Testa]

Anyway, I am stumped by the inability to change the permissions, so this will have to wait until I get my hands on a different computer!