Stream: math-comp analysis

Topic: Documentation


view this post on Zulip Bas Spitters (Oct 26 2020 at 14:47):

I notice that the documentation in the files is a bit scarce (at least compared to the excellent math-comp style).
https://github.com/math-comp/analysis
I'm also missing an overview of the library. I can click around, but it would be more convenient to have a small readme file describing what is where. Are there any plans for that?

view this post on Zulip Marie Kerjean (Nov 10 2020 at 09:59):

Hi Bas, indeed there is not more documentation than (sometimes short) headers. The names of the files are self-descriptive otherwise. Do you have any specific questions which would help us understand what you need ?

view this post on Zulip Bas Spitters (Nov 10 2020 at 11:58):

Far from perfect, but I think a readme like the one for math-classes could be useful
https://github.com/coq-community/math-classes

view this post on Zulip Reynald Affeldt (Nov 11 2020 at 15:37):

it would be more convenient to have a small readme file describing what is where

We haven't done this so far because contents is still moving a bit from one file to another, and we also already foresee some changes in the near future. I guess we chose to improve the headers locally rather than maintaining a centralized documentation with our limited manpower. Yet following your remark we have added links to publications/slides/etc. in the readme. Some contain pictures that depict the library succinctly.

view this post on Zulip Reynald Affeldt (Nov 14 2023 at 07:58):

We also have a short list of results in the wiki: https://github.com/math-comp/analysis/wiki/What's-where%3F. It is not intended to be exhaustive.

view this post on Zulip Michael Soegtrop (Nov 14 2023 at 08:22):

I find this kind of documentation extremely helpful for people who are looking for a library to use for a certain development and want to get a quick overview of what is there.

view this post on Zulip Bas Spitters (Nov 14 2023 at 15:39):

Nice! I wonder how you want to keep that up to date. Could this be automatically generated from the documentation?

@Michael Soegtrop I believe we've discussed this before, but would it be feasible/pleasant to generate the dependency graphs for all the projects in e.g. platform. I'm thinking of the picture we have here https://math-classes.github.io/, or the graphics we use for the HoTT library.
I believe these scripts should be fairly easy to port...

view this post on Zulip Reynald Affeldt (Nov 14 2023 at 15:48):

Bas Spitters said:

Nice! I wonder how you want to keep that up to date. Could this be automatically generated from the documentation?

This will have to be automated once we reach about 100 entries.

view this post on Zulip Michael Soegtrop (Nov 14 2023 at 16:05):

@Bas Spitters : this could be done together with the project lists. I can make a demo. I would do this only on releases, but if one has the script one could run it on any opam switch.


Last updated: Jun 22 2024 at 15:01 UTC