[SwayamInSync]

Plan items T12 (cvc5 and Lean on macOS CI) and T13 (pinned installers). macOS CI installed only ninja, so every test that needs cvc5 or Lean was unsupported there: 36 tests that are not Linux-only, the backend fidelity gate, the cvc5 counterexample tests, and the Lean export, certification, automation, and identity tests among them. They ran only on Linux.

Change

The macOS job installs, as the Linux jobs do:

• cvc5 1.4.2, the newest release the verifier supports (cvc5-macOS-arm64-static.zip from its GitHub release; Linux also runs the oldest, 1.1.2);
• elan, with the pinned Lean (leanprover/lean4:v4.35.0) unpacked from its GitHub release (lean-4.35.0-darwin_aarch64.zip) into elan's toolchain directory, since releases.lean-lang.org, elan's own source, has been down (the Linux jobs do the same, S8: a smoke test that checks more, and Lean from its GitHub release in CI #108).

The test step prints both versions before running clang/test/Verify, so a log shows what ran.

What the tests found on macOS

The first macOS run failed 5 of the 36 tests:

• A real bug in --lean-auto-timeout. The documented limit is per goal ("milliseconds cppverify_auto may spend on one new goal"), but the clock started when Lean was launched, so the first goal of each Lean process was also charged for loading the project's modules. After a goal timed out, the goal after it starts in a new process and paid that load again: on the slower macOS runner lean_automation.test got a_slow (cppverify_auto proved 1 of 3 goals) instead of 2 of 3. The clock now starts when Lean reports it has loaded the modules (tryLeanGoals, Verifier.cpp). New check in lean_automation.test: a user module whose initialize sleeps 4 s, longer than the test's 3 s limit; main's cpp-verify prints a_slow (cppverify_auto proved 1 of 3 goals) there, and this branch prints the expected 2 of 3 (it fails on Linux too, not just macOS).
• GNU-only sed -i in lean_automation.test, lean_contract_certify.test, lean_readable.cpp, and lean_refutation.test (sed: -I or -i may not be used with stdin on macOS). They now use sed -i.orig, which both seds accept and which the other Lean tests already use.
• backend_fidelity_gate.test stopped the Lean certification of its matrix after 180 s (16 s on Linux). The script's 180 s is a hang guard below cpp-verify's own 300 s limit per lake step, so it could cut off a certification that cpp-verify would have finished or reported. Commands that run Lean now get 900 s, and a command that times out prints its output, so a recurrence shows where it was.

Testing

This PR's macOS job is the test: lit marks a test needing cvc5 or lean supported once the tool is on PATH (clang/test/lit.cfg.py), so the 36 tests run in it for the first time. Locally (Linux) the five tests above pass on this branch, and docs_coverage.test passes.

Docs

Release notes, "Testing". ARCHITECTURE.md and the --lean-auto-timeout entry of the tooling reference say when a goal's time starts.

Pinned installers (plan item T13)

The CI workflow took elan-init.sh from elan's master, ilammy/msvc-dev-cmd@v1, and whatever Ninja Chocolatey had, so a change upstream could change or break a run with no change here. They are pinned now, as LLVM's own workflows pin them: elan-init.sh of elan v4.2.4 by its commit (227caca133724d5516bee25c2aeb3e609478f2d8, both jobs), msvc-dev-cmd at v1.13.0's commit (0b201ec74fa43914dc39ae48a89fd1d8cb592756, as libcxx-build-and-test.yaml and libc-shared-tests.yml), and Ninja 1.13.2, the version the Windows image ships (Chocolatey refuses an older pin without --allow-downgrade, which is given so that a newer image still gets this one).