Support builds On Mac

[seanmcl]

Before opening, please confirm:

• I have searched for duplicate or closed issues.
• I have read the guide for submitting bug reports.
• I have done my best to include a minimal, self-contained set of instructions for consistently reproducing the issue.

Bug Category

Other

Describe the bug

I followed the instructions for osx. Got to here:

$ source cedar-drt/set_env_vars.sh
info: downloading component 'lean'
info: installing component 'lean'
cedar-drt/set_env_vars.sh:25: command not found: ldd
awk: syntax error at source line 1
 context is
	BEGIN {exit !( >>>  < <<<  2.27)}
awk: illegal statement at source line 1

ldd is indeed not a thing on mac.

Expected behavior

installation succeeds

Reproduction steps

$  git clone [email protected]:seanmcl/cedar-spec.git
$ brew install elan-init
$ elan default leanprover/lean4:stable
$ cd cedar-spec
$ source cedar-drt/set_env_vars.sh

Code Snippet

// Put your code below this line.

Log output

// Put your output below this line

Additional configuration

No response

Operating System

osx

Additional information and screenshots

No response

[mwhicks1]

FYI, that error message can be ignored, very likely. The script is calling ldd to check for an old glibc, which is unlikely to be there on a Mac that was able to install Lean. Maybe we can gate the check with whether you are running on Linux or MacOs.

[mwhicks1]

(I was able to build on my Mac just fine.)