Stream: math-comp users

Topic: Compatibility testing MC+Coq

view this post on Zulip Karl Palmskog (Jan 23 2022 at 21:20):

This is getting a bit ridiculous in CI for projects that happen to be compatible with MC 1.12 and above:

image:
  - 'mathcomp/mathcomp-dev:coq-dev'
  - 'mathcomp/mathcomp-dev:coq-8.15'
  ...
  - 'mathcomp/mathcomp-dev:coq-8.11'
  - 'mathcomp/mathcomp:1.14.0-coq-8.15'
  ...
  - 'mathcomp/mathcomp:1.14.0-coq-8.11'
  - 'mathcomp/mathcomp:1.13.0-coq-8.15'
  ...
  - 'mathcomp/mathcomp:1.13.0-coq-8.11'
  - 'mathcomp/mathcomp:1.12.0-coq-8.14'
  ...
  - 'mathcomp/mathcomp:1.12.0-coq-8.10'

Are there any heuristics to figure out combinations that are in some sense redundant?

view this post on Zulip Pierre Roux (Jan 23 2022 at 21:56):

1.14.0 and 1.13.0 are very close, so maybe testing only 1.12.0 and 1.14.0 is good enough (plus maybe 1.13.0 for some random Coq version)

view this post on Zulip Cyril Cohen (Jan 23 2022 at 23:00):

maybe we can also drop Coq < 8.12 now...

Last updated: Feb 08 2023 at 08:02 UTC