refactor(Analysis/ODE): restate existence and uniqueness using integral curve API #271459
Triggered via pull request
February 20, 2026 20:37
winstonyin
winstonyin
synchronize
#35043
Status
Failure
Total duration
2m 33s
Artifacts
1
build_fork.yml
on: pull_request_target
ci (fork)
/
Build
1m 45s
ci (fork)
/
Lint style
2m 3s
ci (fork)
/
Post-CI job
0s
Annotations
8 errors and 1 warning
|
ci (fork) / Build
Process completed with exit code 1.
|
|
ci (fork) / Build
No goals to be solved
|
|
ci (fork) / Build
Invalid `⟨...⟩` notation: The expected type of this term could not be determined
|
|
ci (fork) / Build
Function expected at
|
|
ci (fork) / Build
Process completed with exit code 1.
|
|
ci (fork) / Build
No goals to be solved
|
|
ci (fork) / Build
Invalid `⟨...⟩` notation: The expected type of this term could not be determined
|
|
ci (fork) / Build
Function expected at
|
|
ci (fork) / Build
Cache directory does not exist: /home/lean/.cache/mathlib
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
cache-staging
|
90.7 KB |
sha256:38ee51fc71f1013220aeab3db5b586a82577caaa77ccf58028509df3e2cf0cb7
|
|