Stream: coq-community devs & users

Topic: coqffi


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

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

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

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

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:01):

actually it does only supports ocaml.4.10.0

view this post on Zulip Karl Palmskog (Oct 08 2020 at 19:01):

worked fine for me on 4.10.1.

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:02):

yeah sorry, 4.10.*

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:02):

I need to work on that

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:02):

and I don’t mind having the package called coq-coqffi

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:02):

it’s just the README I was referring too here

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:04):

thanks for testing it out though!

view this post on Zulip Karl Palmskog (Oct 08 2020 at 19:04):

I can change the name to just "coqffi", sure this is easy

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:05):

this is exactly why I really wanted to having it published to coq-community (:

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:05):

I would really like that indeed, thanks

view this post on Zulip Karl Palmskog (Oct 08 2020 at 19:05):

but do you still want to keep the namespace to CoqFFI?

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

view this post on Zulip Karl Palmskog (Oct 08 2020 at 19:10):

ah, let's keep CoqFFI for now at least until CI is sorted

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

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

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

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:41):

or is it what you prefer to avoid ?

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:44):

If you agree, I can do that myself, based on your commit (:

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

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:46):

I will have a look tomorrow

view this post on Zulip Thomas Letan (Oct 08 2020 at 19:46):

thanks again!

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

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

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

view this post on Zulip Karl Palmskog (Oct 12 2020 at 15:05):

looks like great plan to me, will meet all my current CI requirements

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

view this post on Zulip 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: Feb 05 2023 at 13:02 UTC