configure: add option -sharedir to specify where to put compcert.ini

[xavierleroy]

This is similar to #450 by @brad0, but in addition we make sure that the directory specified with -sharedir is one of the three locations where the ccomp executable looks for compcert.ini.

Directories are compared by string equality, which is fragile (e.g. /foo/ and /foo compare different, and so do /bar/../foo and /foo). We could do better by using the realpath command-line utility to normalize directory names before comparison, but realpath is not generally available on macOS and BSD systems.

Closes: #450

[brad0]

Directories are compared by string equality, which is fragile (e.g. /foo/ and /foo compare different, and so do /bar/../foo and /foo). We could do better by using the realpath command-line utility to normalize directory names before comparison, but realpath is not generally available on macOS and BSD systems.

It is generally available on FreeBSD / OpenBSD and DragonFlyBSD. NetBSD will have the command as part of their upcoming 10.0 release. But you're right macOS does not have said command. This is also part of the forthcoming edition of the POSIX standard.

[m-schmidt]

But you're right macOS does not have said command.

Funny, I can read the manpage of realpath on macOS 12.6 (obvisously inherited from FreeBSD) but the command is missing.

[brad0]

Funny, I can read the manpage of realpath on macOS 12.6 (obvisously inherited from FreeBSD) but the command is missing.

Most likely a man page for realpath(3) and not realpath(1).

[m-schmidt]

No, it's realpath (1), mentioning realpath (3)...

[brad0]

No, it's realpath (1), mentioning realpath (3)...

That's really weird then.

[s-wegener]

On Darwin 21.6.0 arm64 (macOS 12.6.1), there is only a manpage for realpath(3).

[m-schmidt]

You are right. man -w realpath shows me that the manpage is contained in the Xcode bundle:

$ man -w realpath /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/share/man/man1/realpath.1

[s-wegener]

JFTR

$ man -w realpath
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/share/man/man3/realpath.3
$ man 1 realpath
No entry for realpath in section 1 of the manual

No idea why your system contains realpath (1).

[xavierleroy]

OpenBSD's realpath(1) doesn't have the -m option, thus it fails on nonexistent directories. Installation directories generally don't exist at the time configure is run.

I'm going to merge this PR with no realpath, just syntactic comparisons of directory names. We'll see later if it's too restrictive.

[brad0]

OpenBSD's realpath(1) doesn't have the -m option, thus it fails on nonexistent directories. Installation directories generally don't exist at the time configure is run.

That's a GNU extension. So even as realpath(1) spreads as being part of POSIX it cannot be used.