search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
194 stars 43 forks source link

better advertise the `coq-mathcomp-classical` #1126

Closed affeldt-aist closed 1 month ago

affeldt-aist commented 8 months ago

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 commented 2 months ago

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?

Tragicus commented 2 months ago

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.

affeldt-aist commented 2 months ago

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

Yes, typo, it is fixed now.

affeldt-aist commented 2 months ago

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.