@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.
@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.)
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.
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
actually it does only supports ocaml.4.10.0
worked fine for me on 4.10.1.
yeah sorry, 4.10.*
I need to work on that
and I don’t mind having the package called coq-coqffi
it’s just the README I was referring too here
thanks for testing it out though!
I can change the name to just "coqffi", sure this is easy
this is exactly why I really wanted to having it published to
I would really like that indeed, thanks
but do you still want to keep the namespace to
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
ah, let's keep
CoqFFI for now at least until CI is sorted
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)
@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.
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?
or is it what you prefer to avoid ?
If you agree, I can do that myself, based on your commit (:
the README and CI are unfortunately connected, but if you want to split out changes, go ahead
I will have a look tomorrow
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
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.
Hi @Thomas Letan @Karl Palmskog, just FYI we indeed discussed with @Théo Zimmermann on this topic, and I've summarized the plan here:
looks like great plan to me, will meet all my current CI requirements
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!
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: Feb 05 2023 at 13:02 UTC