Updates available but manual intervention required

[github-actions]

Try lake update and then investigate why this update causes the lean build to fail.

Files changed in update:

• lean-toolchain
• lake-manifest.json

Build Output

✖ [44/94] Building Iris.Algebra.CMRA
trace: .> LEAN_PATH=/home/runner/work/iris-lean/iris-lean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.21.0/bin/lean /home/runner/work/iris-lean/iris-lean/./src//Iris/Algebra/CMRA.lean -R /home/runner/work/iris-lean/iris-lean/./src/ -o /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Algebra/CMRA.olean -i /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Algebra/CMRA.ilean -c /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Algebra/CMRA.c --json
error: ./src//Iris/Algebra/CMRA.lean:227:51: ambiguous, possible interpretations 
  x • y : ?m.22868
  
  x • y : ?m.22857
error: ./src//Iris/Algebra/CMRA.lean:232:6: overloaded, errors 
  232:7 overloaded, errors 
    232:11 Application type mismatch: In the application
      x • y
    the argument
      y
    has type
      x✝ : Type u_1
    but is expected to have type
      α : Type u_2
    
    failed to synthesize
      HSMul α x✝ ?m.23304
    
    Additional diagnostic information may be available using the `set_option diagnostics true` command.
  
  232:7 overloaded, errors 
    232:11 Application type mismatch: In the application
      x • y
    the argument
      y
    has type
      x✝ : Type u_1
    but is expected to have type
      α : Type u_2
    
    failed to synthesize
      HSMul α x✝ ?m.23362
    
    Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: ./src//Iris/Algebra/CMRA.lean:232:24: overloaded, errors 
  232:29 overloaded, errors 
    Application type mismatch: In the application
      op y
    the argument
      y
    has type
      x✝ : Type u_1
    but is expected to have type
      α : Type u_2
    
    failed to synthesize
      HSMul x✝ α ?m.23422
    
    Additional diagnostic information may be available using the `set_option diagnostics true` command.
  
  232:29 overloaded, errors 
    232:33 Application type mismatch: In the application
      y • z
    the argument
      z
    has type
      α : Type u_2
    but is expected to have type
      x✝ : Type u_1
    
    failed to synthesize
      HSMul x✝ α ?m.23601
    
    Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: ./src//Iris/Algebra/CMRA.lean:233:24: overloaded, errors 
  233:29 overloaded, errors 
    233:33 Application type mismatch: In the application
      z • y
    the argument
      y
    has type
      x✝ : Type u_1
    but is expected to have type
      α : Type u_2
    
    failed to synthesize
      HSMul α x✝ ?m.24351
    
    Additional diagnostic information may be available using the `set_option diagnostics true` command.
  
  233:29 overloaded, errors 
    233:33 Application type mismatch: In the application
      z • y
    the argument
      y
    has type
      x✝ : Type u_1
    but is expected to have type
      α : Type u_2
    
    failed to synthesize
      HSMul α x✝ ?m.24579
    
    Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: ./src//Iris/Algebra/CMRA.lean:233:6: invalid 'calc' step, failed to synthesize `Trans` instance
  Trans (Dist n) (Dist n) ?m.25166

Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: ./src//Iris/Algebra/CMRA.lean:237:55: ambiguous, possible interpretations 
  x • y : ?m.23083
  
  x • y : ?m.23072
error: Lean exited with code 1
Some required builds logged failures:
- Iris.Algebra.CMRA
error: build failed