Add LLVM optional dependency

[joehendrix]

No description provided.

[Kha]

@joehendrix Lean should work with clang 8 now, if you want to test building it with clang on Windows

[joehendrix]

@joehendrix Lean should work with clang 8 now, if you want to test building it with clang on Windows

Thanks. I've pushed commits to have it build with clang on all platforms. MacOS is failing, but that looks unrelated to any of my changes. #24 is failing at the same place.

[leodemoura]

@joehendrix Lean should work with clang 8 now, if you want to test building it with clang on Windows

Thanks. I've pushed commits to have it build with clang on all platforms. MacOS is failing, but that looks unrelated to any of my changes. #24 is failing at the same place.

I am investigating the MacOS failure.

[leodemoura]

Wow, I found the problem on MacOS. It is crazy.
The MacOS file system is not case sensitive. Thus, the Lean path normalization function converts all characters in the pathname to lowercase.
We use the auxiliary Python script relative.py in our makefile.
https://github.com/leanprover/lean4/blob/master/library/relative.py#L12
The Python function os.path.relpath normalizes pathnames, but it only converts all characters to lowercase on Windows :(
Thus, Lean outputs the dependency files such as

/users/leonardodemoura/projects/lean4/library/init/lean/smap.olean

In Python, the current directory is

/Users/leonardodemoura/projects/lean4/library

Thus, os.path.relpath produces

../../../../../users/leonardodemoura/projects/lean4/library/init/lean/smap.olean

instead of

init/lean/smap.olean

[Kha]

Wow, what were they thinking? "We don't know whether this path is case-sensitive or not without touching the file system on macOS, so we'll just default to the non-default option"?

[Kha]

Apparently the macOS Python people explicitly decided against matching imports case-insensitively: https://www.python.org/dev/peps/pep-0235/
I wonder if we should do the same. It doesn't make sense to match individual module names case-insensitively because the project will not work on Linux that way. And the path prefix from LEAN_PATH is rarely entered manually by a user, so it shouldn't need case-insensitivity either.

[leodemoura]

I wonder if we should do the same. It doesn't make sense to match individual module names case-insensitively because the project will not work on Linux that way. And the path prefix from LEAN_PATH is rarely entered manually by a user, so it shouldn't need case-insensitivity either.

I don't know the ideal solution yet. We should add an issue for this.
We should also decide what we should do at:
https://github.com/leanprover/lean4/blob/master/library/init/system/filepath.lean#L34
Some normalization is necessary at least of Windows. Examples: foo/bla.lean ==> foo\bla.lean, and D:\ ==> d:\.

[joehendrix]

I think the behavior of os.path.relpath is definitely the wrong thing to do. Haskell's makeRelative indicates that it will never introduce .. into paths due to symlinks and cites this blog post for why.

To the extent possible, I'd be tempted to not normalize paths to lowercase within Lean on OSX and Windows and just keep everything space sensitive. If there are specific checks one needs to make like checking if two syntactically distinct paths refer to the same file, then those could satisfy OS-specific case-sensitivity rules. You may also want something like a makeCanonicalPath for files that exist. That's not too difficult to get mostly right, but difficult (maybe impossible) to get completely right.

[leodemoura]

merged