Stream: coq-community devs & users

Topic: Sudoku


view this post on Zulip Laurent Théry (Oct 17 2022 at 14:01):

The CI of Sudoku seems broken #17. I have no idea how to fix it.

view this post on Zulip 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

view this post on Zulip 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.).

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 17 2022 at 14:07):

It is easy to solve with explicit goal management.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 17 2022 at 14:51):

I can update the PR if you want

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 18 2022 at 12:25):

no requirement here to do any opam release, please go ahead and merge


Last updated: Feb 05 2023 at 13:02 UTC