search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
127 stars 166 forks source link

release coq-htt and coq-htt-core 2.0.0 #3169

Closed aleksnanevski closed 1 month ago

aleksnanevski commented 1 month ago

Updated coq-htt to mathcomp2 and fcsl-pcm.2.0.0.

Note that the package names have changed.

coq-htt contains the whole development, including metatheory and examples. coq-htt-core contains just the metatheory. Previously this used to be called coq-htt.

palmskog commented 1 month ago

@aleksnanevski it looks like coq-htt-core does not depend on coq-htt, i.e., they are independent packages. However, this means that they will install files into the same directory in opam and should be marked as conflicting, i.e., it should be impossible to install them both at the same time, since they "own" the same files.

aleksnanevski commented 1 month ago

You're right. Is there a way to mark them as conflicting?

silene commented 1 month ago

I think the conflict is in the wrong direction. If I understand correctly that the files of coq-htt-core are also in coq-htt (including pre-2.0 versions), then it is coq-htt-core that should contain the line

conflicts: [ "coq-htt" ]

Otherwise, the users will be able to install both coq-htt=1.3.0 and coq-htt-core=2.0.0, which will break havoc in their filesystem.

aleksnanevski commented 1 month ago

Hmm, good point. Let me update then.