chore: bump to v4.8.0-rc1 and fix proofs #118
ramonfmirAnnotations
6 errors and 1 warning
|
build:
CvxLean/Lib/Math/SchurComplement.lean#L58
CvxLean/Lib/Math/SchurComplement.lean:58 ERR_DOT: Line is an isolated focusing dot or uses . instead of ·
|
|
build:
CvxLean/Lib/Math/SchurComplement.lean#L60
CvxLean/Lib/Math/SchurComplement.lean:60 ERR_DOT: Line is an isolated focusing dot or uses . instead of ·
|
|
build:
CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean#L29
CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean:29 ERR_NSP: Non-terminal simp. Replace with `simp?` and use the suggested output
|
|
build:
CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean#L23
CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean:23 ERR_NSP: Non-terminal simp. Replace with `simp?` and use the suggested output
|
|
build:
CvxLean/Examples/FittingSphere.lean#L130
CvxLean/Examples/FittingSphere.lean:130 ERR_DOT: Line is an isolated focusing dot or uses . instead of ·
|
|
build
Process completed with exit code 1.
|
|
build
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|