Skip to content
Docker CI

[WIP] replace the infrastructure of mpoly with monalg #412

Sign in to view logs

[WIP] replace the infrastructure of mpoly with monalg

[WIP] replace the infrastructure of mpoly with monalg #412

Triggered via push September 30, 2025 12:57
@pi8027pi8027
pushed 20cbc6c
monalg-based-mpoly
Status Failure
Total duration 4m 58s
Artifacts –

ci.yml

on: push
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

2 errors and 20 warnings
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/mpoly.v#L1735
Unknown interpretation for notation "U_( _ )".
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/mpoly.v#L156
Ill formed “deprecated” attribute.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L13
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L13
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L13
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L13
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/monalg.v#L13
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/monalg.v#L13
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/monalg.v#L13
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/monalg.v#L13
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0