Michael Soegtrop (Aug 11 2020 at 09:57): 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.
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?
Michael Soegtrop (Aug 11 2020 at 13:40):Karl Palmskog said:
hmm, wouldn't the Gappa package most simply be named just
gappa, and thencoq-gappais 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.
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.
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.
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, ...
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.
Théo Zimmermann (Aug 11 2020 at 15:02):IIUC this will still be distributed only through the opam-coq-repository
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
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).
Karl Palmskog (Aug 11 2020 at 15:05):@Michael Soegtrop couldn't that package work with Clang also?
Michael Soegtrop (Aug 11 2020 at 15:05):I like the conditions for individual arguments to configure.
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.
Michael Soegtrop (Aug 11 2020 at 15:07):But as I said, it is preliminary and needs some more work.
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)
Enrico Tassi (Aug 11 2020 at 15:11):I think gappa is fine
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: Jun 03 2023 at 04:30 UTC