Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

better advertise the coq-mathcomp-classical #1126

Closed
affeldt-aist opened this issue Dec 21, 2023 · 4 comments · Fixed by #1263
Closed

better advertise the coq-mathcomp-classical #1126

affeldt-aist opened this issue Dec 21, 2023 · 4 comments · Fixed by #1263
Assignees
@t6s @affeldt-aist
Labels
documentation 📝 This issue/PR is about documentation of the library / repository
Milestone
1.3.0

Comments

@affeldt-aist
Copy link
Member

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 affeldt-aist added the documentation 📝 This issue/PR is about documentation of the library / repository label Dec 21, 2023
@affeldt-aist affeldt-aist added this to the 0.6.7 milestone Dec 21, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.7, 0.6.8 Jan 8, 2024
@affeldt-aist affeldt-aist modified the milestones: 0.7.0, 1.0.0 Jan 17, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.0.0, 1.0.1 Jan 25, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.0.1, 1.1.0, 1.2.0 Mar 24, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.2.0, 1.3.0 Jun 5, 2024
@affeldt-aist
Copy link
Member Author

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
Copy link
Collaborator

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
Copy link
Member Author

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

Yes, typo, it is fixed now.

@affeldt-aist
Copy link
Member Author

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 affeldt-aist self-assigned this Jul 19, 2024
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Jul 21, 2024
@affeldt-aist
fixes math-comp#1126
d976f0c
@affeldt-aist affeldt-aist mentioned this issue Jul 21, 2024
Merged
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Jul 21, 2024
@affeldt-aist
fixes math-comp#1126
becd817
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@t6s t6s

@affeldt-aist affeldt-aist

Labels
documentation 📝 This issue/PR is about documentation of the library / repository
Projects
None yet
Milestone
1.3.0
Development

Successfully merging a pull request may close this issue.

fixes #1126 affeldt-aist/analysis
3 participants
@t6s @affeldt-aist @Tragicus