Thomas Letan (Oct 08 2020 at 18:51): Thomas Letan (Oct 08 2020 at 18:51):@Karl Palmskog Thanks for the community-ci branch! Just a quick thought, I would rather keep the original way of writing coqffi, that is coqffi, rather than your proposal (CoqFFI). There is indeed a CoqFFI theory, but the main component of this repo is the OCaml tool.
Karl Palmskog (Oct 08 2020 at 18:56):@Thomas Letan if you want your package to be in the Coq OPAM archive, it will have to be named coq-coqffi, or something else coq-*. This is a baseline requirement (meaning, we are not going to merge packages not conforming to this.)
Karl Palmskog (Oct 08 2020 at 18:58):and if you put the package in the general OPAM repo, you have to separate out the Coq parts, since they will not merge any package with coq-simple-io as a dep.
Karl Palmskog (Oct 08 2020 at 18:59):the main problem I discovered with CoqFFI as it currently stands is that it requires OCaml 4.10.0 or later. This unfortunately makes it unusable for the vast majority of Coq users (and in particular those using the Coq platform), since they are running on OCaml in the range 4.05.0 - 4.09.0
Thomas Letan (Oct 08 2020 at 19:01):actually it does only supports ocaml.4.10.0
Karl Palmskog (Oct 08 2020 at 19:01):worked fine for me on 4.10.1.
Thomas Letan (Oct 08 2020 at 19:02):yeah sorry, 4.10.*
Thomas Letan (Oct 08 2020 at 19:02):I need to work on that
Thomas Letan (Oct 08 2020 at 19:02):and I don’t mind having the package called coq-coqffi
Thomas Letan (Oct 08 2020 at 19:02):it’s just the README I was referring too here
Thomas Letan (Oct 08 2020 at 19:04):thanks for testing it out though!
Karl Palmskog (Oct 08 2020 at 19:04):I can change the name to just "coqffi", sure this is easy
Thomas Letan (Oct 08 2020 at 19:05):this is exactly why I really wanted to having it published to coq-community (:
Thomas Letan (Oct 08 2020 at 19:05):I would really like that indeed, thanks
Karl Palmskog (Oct 08 2020 at 19:05):but do you still want to keep the namespace to CoqFFI?
Thomas Letan (Oct 08 2020 at 19:07):I guess we could rename it Coqffi, I don’t really mind. I distinguish between the tool and the theory, but I guess it makes sense to try to keep everything consistent
Karl Palmskog (Oct 08 2020 at 19:10):ah, let's keep CoqFFI for now at least until CI is sorted
Karl Palmskog (Oct 08 2020 at 19:15):it seems we currently don't have any prebuilt Coq Docker images with 4.10.X (maybe @Erik Martin-Dorel knows if this would be easy to add)
Karl Palmskog (Oct 08 2020 at 19:31):@Thomas Letan I'm done with adding the boilerplate in the branch community-ci, like opam package definition. Rather than having an ad-hoc CI, I would prefer to wait for a Coq Docker image for 4.10.X before the branch is merged (or for compatibility with OCaml 4.09.X, if that is an option). Actual changes to existing files are quite trivial compared to what was added, so rebases should not be hard.
Thomas Letan (Oct 08 2020 at 19:41):Another approach could be to split your commit into two, and I could merge the README modification first, and we could have a draft PR for the CI?
Thomas Letan (Oct 08 2020 at 19:41):or is it what you prefer to avoid ?
Thomas Letan (Oct 08 2020 at 19:44):If you agree, I can do that myself, based on your commit (:
Karl Palmskog (Oct 08 2020 at 19:45):the README and CI are unfortunately connected, but if you want to split out changes, go ahead
Thomas Letan (Oct 08 2020 at 19:46):I will have a look tomorrow
Thomas Letan (Oct 08 2020 at 19:46):thanks again!
Erik Martin-Dorel (Oct 08 2020 at 19:50):Karl Palmskog said:
it seems we currently don't have any prebuilt Coq Docker images with 4.10.X (maybe Erik Martin-Dorel knows if this would be easy to add)
it is feasible, but actually before publishing images with 4.10 for some Coq versions (not all Coq versions support 4.10, unlike e.g. 4.07.1+flambda), we need to agree on a policy…
and for the moment, the discussion in https://github.com/coq-community/docker-coq/issues/12 is still open
Erik Martin-Dorel (Oct 08 2020 at 19:53):anyway I have a video meeting planned with @Théo Zimmermann on next week, I guess we'll be able to focus on this as well, and try to make the discussion progress on this issue.
Erik Martin-Dorel (Oct 12 2020 at 14:48):Hi @Thomas Letan @Karl Palmskog, just FYI we indeed discussed with @Théo Zimmermann on this topic, and I've summarized the plan here:
https://github.com/coq-community/docker-coq/issues/12#issuecomment-707165691
Karl Palmskog (Oct 12 2020 at 15:05):looks like great plan to me, will meet all my current CI requirements
Thomas Letan (Oct 12 2020 at 18:02):I will have to take the time to read this once or twice, I am not that well familiar with this (: that being said, thanks for your work!
Karl Palmskog (Oct 12 2020 at 20:15):the bottom line for nearly any user of CI (e.g., in coq-community) is that they will have to choose a "tag" in Coq's Docker hub, which uniquely determines the OCaml version and the Coq version/branch. If one uses Docker-Coq, this choice of tag solves nearly everything.
Last updated: Jun 06 2023 at 22:01 UTC