search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

at the end of HB.howto output, it suggests a link to a guide on how to declare mathcomp instances #437

Closed Tvallejos closed 1 month ago

Tvallejos commented 1 month ago

At CUDW 2024, we discussed the idea of ​​writing a guide for declaring mathcomp instances. This PR refers to that guide.

CohenCyril commented 1 month ago

Looks good to me in principle. However HB is meant to be used outside of math-comp. Shouldn't the command refer to a doc in HB wiki rather than math-comp wiki?

Tvallejos commented 1 month ago

It is true, there are conflicting interests. On the one hand, HB is used outside of mathcomp. And on the other hand, mathcomp uses HB to declare its instances. We thought with @gares of adding this link to the HB message so that it would be easy to reach for mathcomp users. Regarding the guide's location, the guide has a section that is only valid for mathcomp, because it uses definitions that are in mathcomp files. I think it would be less convenient to put it on the HB wiki.

gares commented 1 month ago

The message talks about math comp explicitly, so I don't think it is too misguiding.