Checking permissions of a file

Stream: lean4

[Michael Rothgang]

I'd like to rewrite the check for executable Lean files in mathlib: in short, I'd like to rewrite the following line in Lean.
executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))
(I can shell out to find, but would prefer not to.)

Finding all .lean files is doable (there's code for this already) --- can I check a file's permissions in Lean? I didn't see anything obvious from the documentation.

[Eric Wieser]

I think it's ok to leave some checks in bash, especially the ones that don't need to know anything about lean

[Eric Wieser]

In particular, if you write it in Lean, then you run into trouble on windows where the permissions bits don't really exist in the same way except where emulated by git bash.

[Number Eighteen]

For such I/O missing from Lean, I was told to use Alloy to call C code directly from Lean. In this
situation, you can get the platform from System.Platform and call the appropriate C code to get file
permissions if the platform allows it. I still haven't tested this workflow, though.