Lean failure on PreludeMemMetadata

[jordancarlin]

@ineol @tobiasgrosser The Lean "no binary found" issue finally seems to have resolved itself, but now the Lean build is failing with the following error:

✖ [22/98] Building LeanRV64D.PreludeMemMetadata
trace: .> LEAN_PATH=/home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577/bin/lean --tstack=400000 -Dweak.linter.style.nameCheck=false /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/LeanRV64D/PreludeMemMetadata.lean -R /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D -o /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/lib/lean/LeanRV64D/PreludeMemMetadata.olean -i /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/lib/lean/LeanRV64D/PreludeMemMetadata.ilean -c /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/ir/LeanRV64D/PreludeMemMetadata.c --json
error: LeanRV64D/PreludeMemMetadata.lean:181:56: unexpected token 'meta'; expected '_' or identifier
error: LeanRV64D/PreludeMemMetadata.lean:181:60: unexpected token ':'; expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'example', 'inductive', 'initialize', 'instance', 'opaque', 'structure' or 'theorem'
error: Lean exited with code 1

[tobiasgrosser]

Thank you, @jordancarlin for reporting. This is the corresponding sail PR that should fix the issue: rems-project/sail#1358

[tobiasgrosser]

This PR has now been merged. The CI should be clean on the next rebuild.

[jordancarlin]

Lean building successfully again. Thanks!