nix-shell fails to build on aarch64-darwin/macOS

[crvdgc]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

nix-shell fails to build on aarch64-darwin/macOS.

Context

Following the build setup instruction, when trying to use nix-shell to setup the build environment, the command fails.

I reported the issue in this Zulip thread. The thread is about the need to compile Lean 4 in the Lean 4 repository because elan now (correctly) no longer falls back to a default Lean version when it cannot find the artifact.

Steps to Reproduce

On aarch64-darwin/macOS, run nix-shell in the root directory.

(Alternatively, build the problematic input withnix build .#packages.aarch64-darwin.lean-all.)

Expected behavior: build succeeds

Actual behavior: build fails with the following log:

[...]
 7/42 Test #11: test.fileclone ...................***Failed    1.14 sec
/tmp/nix-build-ccache-4.8.1.drv-2/source/test/suites/base.bash: line 556: syntax error near unexpected token `&&'
/tmp/nix-build-ccache-4.8.1.drv-2/source/test/suites/base.bash: line 556: `       && $COMPILER -E test1.c -gz >preprocessed.i 2>/dev/null \'
Compiler:         clang (/nix/store/l5dr4rvjmiybf3la6mk6gzhszrb9py3v-Toolchains/XcodeDefault.xctoolchain/bin/clang)
Compiler version: clang version 11.1.0
CUDA compiler:    not available

Running test suite fileclone.
FAILED

Test suite:     fileclone (line 32)
Test case:      Base case
Failure reason: Failed to clone
[...]
The following tests FAILED:
         11 - test.fileclone (Failed)
Errors while running CTest

Versions

Lean version: dd42a09
OS version:

$ uname -a
Darwin rubeno.local 23.1.0 Darwin Kernel Version 23.1.0: Mon Oct  9 21:27:24 PDT 2023; root:xnu-10002.41.9~6/RELEASE_ARM64_T6000 arm64

Additional Information

The issue is a bug in the CCache v4.8.1 test script. It has been fixed and the patch is available in CCache v4.8.2. I've tested with a local nix flake update. The updated flake lock now fetches CCache v4.8.3 which fixes this issue and can successfully build Lean 4. I'm planning to submit a PR for that.

Please review if it breaks other usages that depend on the locked flake versions in that PR.

[Kha]

The Nix build has been officially deprecated #4895