Stream: Coq Platform devs & users

Topic: Naming of Opam packages


view this post on Zulip Michael Soegtrop (Aug 11 2020 at 09:57):

I created a few opam packages to install non OCaml stuff from sources - mostly for Windows up to now. See the "dep-" packages in (https://github.com/MSoegtropIMC/coq-platform/tree/master/opam/packages). But I now think to add an opam package for gappa (which is written in C++). I see now issues doing this (in a platform independent way) but it doesn't seem to be common practice. I wonder how I should name such packages. The windows specific packages I linked above maybe "win-xyz" and link the from the corresponding conf packages (which I already do in the coq platform repo). How would I name the gappa package? cpp-gappa?

I think for the Coq user experience it makes sense to compile Coq centric exotic stuff like gappa from sources in an opam package - it is quite quick and likely much more reliably than trying to get it via system packages.

view this post on Zulip Karl Palmskog (Aug 11 2020 at 11:52):

hmm, wouldn't the Gappa package most simply be named just gappa, and then coq-gappa is the tactic which depends on this?

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 13:40):

Karl Palmskog said:

hmm, wouldn't the Gappa package most simply be named just gappa, and then coq-gappa is the tactic which depends on this?

I think it is not very common to name a package which is not written in OCaml just "package" - at least I don't know of any. Like all packages written in Coq are named coq-xyz. This makes me unsure what is the best practice here.

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 14:59):

The reason why they are all named coq-xyz is so that you find them easily, especially when you have both repositories for OCaml and Coq.

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 15:00):

I think naming the package gappa is fine but maybe @Enrico Tassi may want to give his opinion too.

view this post on Zulip Karl Palmskog (Aug 11 2020 at 15:00):

in the Coq opam repo, we indeed have coq-xyz (which allows us to never clash with regular ocaml packages), but in the regular repo, most packages are called just <name>, like coq, ott, cmdliner, ...

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 15:01):

OK, if there are no strong feelings in the OCaml community to invade opam with packages written in C++, I will name it just gappa.

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 15:02):

IIUC this will still be distributed only through the opam-coq-repository

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 15:02):

If you wanted to add these to the main opam repository, then you would need to check with its maintainers

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 15:05):

I will ask who wants it, but I guess it would make sense in the coq opam repo.
Btw.: opam is quite convenient for this. Here is my preliminary opam file: https://github.com/MSoegtropIMC/coq-platform/blob/v8.11/opam/packages/cpp-gappa/cpp-gappa.1.3.5/opam (still named cpp-gappa).

view this post on Zulip Karl Palmskog (Aug 11 2020 at 15:05):

@Michael Soegtrop couldn't that package work with Clang also?

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 15:05):

I like the conditions for individual arguments to configure.

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 15:06):

Karl Palmskog said:

Michael Soegtrop couldn't that package work with Clang also?

I am not sure - I think gappa configure checks explicitly for gcc.

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 15:07):

But as I said, it is preliminary and needs some more work.

view this post on Zulip Karl Palmskog (Aug 11 2020 at 15:07):

OK I see. Here is an idiom for supporting both GCC and Clang: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-flocq/coq-flocq.3.3.1/opam (if the software does)

view this post on Zulip Enrico Tassi (Aug 11 2020 at 15:11):

I think gappa is fine

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 15:59):

Karl Palmskog said:

OK I see. Here is an idiom for supporting both GCC and Clang: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-flocq/coq-flocq.3.3.1/opam (if the software does)

Thanks, I will give it a try. Maybe I will refactor the remake based packages such that remake is installed via opam upfront - it doesn't make that much sense to compile it for every tool.


Last updated: Jan 30 2023 at 11:03 UTC