Skip to content
continuous integration (mathlib forks)

[Merged by Bors] - feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable #271470

Sign in to view logs

[Merged by Bors] - feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable

[Merged by Bors] - feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable #271470

Triggered via pull request February 20, 2026 22:31
@j-loreauxj-loreaux
synchronize #35589
Status Failure
Total duration 18m 25s
Artifacts 1

build_fork.yml

on: pull_request_target
ci (fork)  /  Build
17m 36s
ci (fork) / Build
ci (fork)  /  Lint style
1m 59s
ci (fork) / Lint style
ci (fork)  /  Upload to cache
44s
ci (fork) / Upload to cache
ci (fork)  /  Post-Build Step
0s
ci (fork) / Post-Build Step
ci (fork)  /  Post-CI job
0s
ci (fork) / Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

20 errors and 21 warnings
ci (fork) / Build
(kernel) declaration has metavariables 'Matrix.linfty_opNorm_eq_opNorm'
ci (fork) / Build
unknown metavariable '?_uniq.72766'
ci (fork) / Build
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
ci (fork) / Build
could not synthesize default value for parameter 'cont' using tactics
ci (fork) / Build
linter _private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.unusedFintypeInType failed: unknown metavariable '?_uniq.72766'
ci (fork) / Build
(kernel) declaration has metavariables 'Matrix.linfty_opNNNorm_eq_opNNNorm'
ci (fork) / Build
Tactic `rewrite` failed: Did not find an occurrence of the pattern
ci (fork) / Build
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
ci (fork) / Build
could not synthesize default value for parameter 'cont' using tactics
ci (fork) / Build
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
ci (fork) / Build
(kernel) declaration has metavariables 'Matrix.linfty_opNorm_eq_opNorm'
ci (fork) / Build
unknown metavariable '?_uniq.72766'
ci (fork) / Build
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
ci (fork) / Build
could not synthesize default value for parameter 'cont' using tactics
ci (fork) / Build
linter _private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.unusedFintypeInType failed: unknown metavariable '?_uniq.72766'
ci (fork) / Build
(kernel) declaration has metavariables 'Matrix.linfty_opNNNorm_eq_opNNNorm'
ci (fork) / Build
Tactic `rewrite` failed: Did not find an occurrence of the pattern
ci (fork) / Build
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
ci (fork) / Build
could not synthesize default value for parameter 'cont' using tactics
ci (fork) / Build
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
`continuous_add_right` has been deprecated: Use `continuous_add_const` instead
ci (fork) / Build
`continuous_add_left` has been deprecated: Use `continuous_const_add` instead
ci (fork) / Build
Cache directory does not exist: /home/lean/.cache/mathlib

Artifacts

Produced during runtime
Name Size Digest
cache-staging
82.1 MB
sha256:446fa9b8fb041b369845fdd439207debd62933f370a6b9589510b11acee1d571