lean
lean copied to clipboard
leanprover-community
fix(bin/leanpkg): replace `readlink -f`
realpath behaves more uniformly than readlink -f across platforms, which eliminates the mundane test for checking availability of greadlink on OS X. Noting that realpath is not exchangeable everywhere with readlink -f but in this simple case it is suffice. Since realpath has been available from GNU coreutils since v8.15, most users shouldn't be affected by this change.
According to @alexpeattie, realpath isn't installed by default either. Can you shed some light on this, I don't have a mac?
realpath isn't installed on macOS by default either sadly sob . There are some alternatives here if we want to preserve the symlink reading behaviour
Neither greadlink nor realpath is present by default on mac, but if mac users have already installed greadlink from package manager of their choice, i.e. Homebrew, it means they also have realpath installed, which means those Mac users who already installed coreutils don't have to worry about this change.
This change is mean to relief those Mac users who prefer a compatible realpath other than the one from coreutils, such as https://github.com/harto/realpath-osx (it is a barely minimal implementation compared to coreutils), also FreeBSD users, they have realpath present in their systems by default, but not a readlink accepts -f.
I don't know if there's an advantage to switching from greadlink to realpath, but I think we should keep the if statement with a message about installing coreutils for users who don't have it 🙂
So I made another commit change it to prompt user to install coreutils, and still fallback to readlink -f for some distributions with older versions of coreutils such as CentOS.
~Revisiting this again @LdBeth - I'm not sure that changing the if to checking command -v realpath is right, because realpath is present by default on macOS, just not the GNU realpath which supports the -v flag. I think you'd either want to check uname as before, or do something like if realpath -f / >/dev/null 2>&1?~ Oops ignore this, I was getting realpath and readlink mixed up!
Also, just to double check, what's the main advantage to switching to realpath over greadlink? Thanks 🙂 !
@alexpeattie although macOS has neither realpath nor GNU readlink, acquiring the realpath command is fairly simple and flexible, user can choose either an executable calls C realpath, a python script calls os.path.realpath, even pure bash script implementation, or just use realpath from coreutils, which also introduces a bunch of tools may not needed by the user, which I personally find undesirable.
We might choose write shell function to replace call to external tools, but I feel it is unnecessary. realpath is a tool been reinvented too many times.