Yves Bertot (Jun 05 2020 at 06:50): Yves Bertot (Jun 05 2020 at 06:50):Hello, a recent PR to opam-coq-archive concerning hoare-tut attracted my attention. First, I wish to thank @Kartik Singhal for his work on this, second I am amazed that Boulmé is mentioned in the README file but not in the opam file. Do we, or should we have a rule about this?
Karl Palmskog (Jun 05 2020 at 06:53):the proper way to handle authorship is to include it in meta.yml, which will make sure it appears both in the README and in the opam file when the templates are properly used. Maybe something went awry here. I might be able to take a look later today.
For a completely different reason also, that opam package definition needs to be revised (no proper Coq version restriction).
Kartik Singhal (Jun 05 2020 at 11:12):Ah, I had used the ../templates/generate.sh script to create the default opam file before editing it for basics, it contains the author name as its last field. Then I used the opam-publish plugin to send the PR. At first glance, I thought the author field was missing too, but I do see it at https://github.com/coq/opam-coq-archive/pull/1273/files#diff-bfbf80eba76a01e7d076f7591c19ae0cR40 Perhaps the author field should be pushed up in the template's generation script?
Kartik Singhal (Jun 05 2020 at 11:22):For Coq versions, is there a way to find the longest interval of versions for which a Coq package will work (such as using the CI)? I do have several versions of Coq on my local machine, but it can be tedious to test. In my unfamiliarity with the CI and release system, I was trying to avoid restricting the Coq version (especially for future) as then the OPAM packages can keep breaking with each release even if the source compiles just fine.
Yves Bertot (Jun 05 2020 at 11:31):okay, it was a mistake from me then (concerning the author). Thanks @Kartik Singhal
Kartik Singhal (Jun 05 2020 at 11:31):No problem, Yves!
Yves Bertot (Jun 05 2020 at 11:37):I would advocate having the author next to the maintainer in the template.
I plan to try the current version of coq-community/hoare-tut on 8.9 and 8.10 and give you feedback.
Kartik Singhal (Jun 05 2020 at 11:39):Thanks, I imagine it will work on 8.10 and might break on 8.9 as my first PR in that package involved fixing the build for 8.10. But yes, I agree, we should move the author field up. Let me take care of that in both the source and the PR.
Yves Bertot (Jun 05 2020 at 11:41):I am slightly surprised as it seems the head version does compile with coq-8.8
Yves Bertot (Jun 05 2020 at 11:47):To me, it seems compilation succeeds with version 8.8, 8.9, 8.10, and 8.11 of coq. I don't have 8.7 installed locally, so I did not test it yet.
Kartik Singhal (Jun 05 2020 at 11:59):Wow, thank you. I will see if specifying >=8.8 in the Opam file keeps the CI happy.
Théo Zimmermann (Jun 05 2020 at 13:04):@Kartik Singhal If you want, we can activate CI in the hoare-tut repository so that you keep a better view of which versions are supported at any given time.
Kartik Singhal (Jun 05 2020 at 13:27):That could be useful (and perhaps I can add the coq-action.yml myself now, but just to clarify: do we allow only supported versions for these community maintained packages or also the older ones such as 8.8 and 8.9 on which this package continues to work as tested by Yves?
Théo Zimmermann (Jun 05 2020 at 13:38):I suggest that you test the largest range of versions possible (math-classes still tests 8.6!) but you don't commit yourself to maintain compatibility with the old versions (i.e., if it breaks at some point, you can just remove the support for these versions from the README and the CI).
Last updated: Jun 03 2023 at 17:29 UTC