analysis icon indicating copy to clipboard operation
analysis copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

better advertise the `coq-mathcomp-classical`

Open affeldt-aist opened this issue 1 year ago • 4 comments

It was observed during the MathComp-Analysis dev meeting of 2023-12-21 that the existence of the coq-mathcomp-classical is not well-known @Tragicus

We should maybe improve the MathComp website https://math-comp.github.io/installation.html so that it is more apparent (and indeed it is not mentioned there!) @t6s

affeldt-aist avatar Dec 21 '23 14:12 affeldt-aist

In an attempt to address this issue I have edited the web page with installation instructions to streamline it and make the coq-mathcomp-classic package apparent: https://math-comp.github.io/installation.html

@Tragicus What do you think?

affeldt-aist avatar Jun 21 '24 02:06 affeldt-aist

It looks great (although is not the opam package coq-mathcomp-classical?). I believe the README here is more visible, so it should be documented here too.

Tragicus avatar Jun 21 '24 07:06 Tragicus

although is not the opam package coq-mathcomp-classical?

Yes, typo, it is fixed now.

affeldt-aist avatar Jun 21 '24 07:06 affeldt-aist

believe the README here is more visible, so it should be documented here too.

You mean in the README of MathComp-Analysis? Indeed. I'll try to come up with something.

affeldt-aist avatar Jun 21 '24 07:06 affeldt-aist