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?
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).
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?
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.
okay, it was a mistake from me then (concerning the author). Thanks @Kartik Singhal
No problem, Yves!
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.
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.
I am slightly surprised as it seems the head version does compile with coq-8.8
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.
Wow, thank you. I will see if specifying >=8.8 in the Opam file keeps the CI happy.
@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.
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?
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