Laurent Théry (Oct 17 2022 at 14:01): Laurent Théry (Oct 17 2022 at 14:01):The CI of Sudoku seems broken #17. I have no idea how to fix it.
Karl Palmskog (Oct 17 2022 at 14:03):it looks like the new code is only compatible with Coq 8.16.0 and not any other version, including master
Théo Zimmermann (Oct 17 2022 at 14:06):Indeed. Something we can observe is that the errors are not the same in 8.12-8.14 (The reference Lt.le_lt_or_eq_stt was not found in the current environment) and in master (Found no subterm matching "length (add l1 ?M1249)" in the current goal.).
Théo Zimmermann (Oct 17 2022 at 14:07):The error in master is very likely due to auto having become more powerful and thus a goal has disappeared.
Théo Zimmermann (Oct 17 2022 at 14:07):It is easy to solve with explicit goal management.
Théo Zimmermann (Oct 17 2022 at 14:08):Regarding the non-compatibility with Coq < 8.16, let us know if you want to drop old versions from the CI.
But the latest sudoku release (8.12.0) is not even in opam and it isn't likely to be compatible all the way to Coq 8.15, so it would be nicer to ensure that Coq 8.11-8.15 compatible releases are available before dropping these old versions.
Gaëtan Gilbert (Oct 17 2022 at 14:09):btw you're not supposed to use this _stt stuff, it's just there so that the deprecated notation can use the original name since we don't yet have a way to deprecate definitions/lemmas
Laurent Théry (Oct 17 2022 at 14:46):oops I was only at the first failure : COQ_IMAGE=coqorg/coq:dev-ocaml-4.11-flambda
Error response from daemon: manifest for coqorg/coq:dev-ocaml-4.11-flambda not found: manifest unknown: manifest unknown
Laurent Théry (Oct 17 2022 at 14:49):Gaëtan Gilbert said:
btw you're not supposed to use this _stt stuff, it's just there so that the deprecated notation can use the original name since we don't yet have a way to deprecate definitions/lemmas
didn't know, will fix this one
Karl Palmskog (Oct 17 2022 at 14:50):oh OK, this [the CI problem] can be fixed quite easily, it should be coq:dev-ocaml-4.13-flambda
Karl Palmskog (Oct 17 2022 at 14:51):I can update the PR if you want
Laurent Théry (Oct 17 2022 at 15:36):grrr I did a ./configure -prefix /tmp/coq and a dune install and everything got installed in my current opam directory. Not my day today. I will try to fix things tomorrow
Karl Palmskog (Oct 17 2022 at 15:41):@Laurent Théry I think I figured out the sudoku problem on master in a backward-compatible way. If you don't mind I'll commit to your PR branch.
Théo Zimmermann (Oct 17 2022 at 15:42):Laurent Théry said:
grrr I did a ./configure -prefix /tmp/coq and a dune install and everything got installed in my current opam directory. Not my day today. I will try to fix things tomorrow
Indeed, nowadays, you have to provide the -prefix again when doing dune install.
Karl Palmskog (Oct 17 2022 at 16:29):the PR builds with Coq master now (and all other versions previously supported): https://github.com/coq-community/sudoku/pull/17
Karl Palmskog (Oct 17 2022 at 16:32):I think the general recommendation should be w.r.t. Coq master and opam: please use coq.dev from the core-dev opam repo over building yourself. Dune seems to develop quite rapidly these days.
Laurent Théry (Oct 18 2022 at 11:48):thanks to @Karl Palmskog now the CI passes. Can I merge it or do you want me to do an opam release first?
Théo Zimmermann (Oct 18 2022 at 12:24):Please do merge, an opam release afterward would be really nice as it would be compatible with Coq 8.12-8.16 (possibly even Coq 8.17).
Théo Zimmermann (Oct 18 2022 at 12:24):We may want to add explicit CI testing with Coq 8.15-8.16 before releasing though.
Karl Palmskog (Oct 18 2022 at 12:25):no requirement here to do any opam release, please go ahead and merge
Notification Bot (Oct 19 2022 at 11:40):Laurent Théry has marked this topic as resolved.
Last updated: Jun 03 2023 at 18:01 UTC