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.

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

ML API documentation meta issue #7155

Open
2 of 7 tasks
ejgallego opened this issue Apr 2, 2018 · 14 comments
Open
2 of 7 tasks

ML API documentation meta issue #7155

ejgallego opened this issue Apr 2, 2018 · 14 comments
Labels
kind: documentation Additions or improvement to documentation. kind: infrastructure CI, build tools, development tools. kind: internal API, ML documentation...

Comments

@ejgallego
Copy link
Member

ejgallego commented Apr 2, 2018

C̶o̶q̶ ̶c̶u̶r̶r̶e̶n̶t̶l̶y̶ ̶p̶r̶o̶v̶i̶d̶e̶s̶ ̶a̶ ̶w̶a̶y̶ ̶t̶o̶ ̶g̶e̶n̶e̶r̶a̶t̶e̶ ̶a̶ ̶d̶o̶c̶u̶m̶e̶n̶t̶a̶t̶i̶o̶n̶ ̶o̶f̶ ̶t̶h̶e̶ ̶m̶l̶-̶l̶e̶v̶e̶l̶ ̶i̶m̶p̶l̶e̶m̶e̶n̶t̶a̶t̶i̶o̶n̶ ̶u̶s̶i̶n̶g̶ ̶t̶h̶e̶ ̶̶s̶o̶u̶r̶c̶e̶-̶d̶o̶c̶̶,̶ ̶̶.̶m̶l̶i̶-̶d̶o̶c̶̶,̶ ̶̶m̶l̶-̶d̶o̶c̶̶ ̶m̶a̶k̶e̶ ̶t̶a̶r̶g̶e̶t̶s̶.̶

H̶o̶w̶e̶v̶e̶r̶,̶ ̶t̶h̶e̶s̶e̶ ̶t̶a̶r̶g̶e̶t̶s̶ ̶a̶r̶e̶ ̶n̶o̶t̶ ̶v̶e̶r̶y̶ ̶w̶e̶l̶l̶ ̶m̶a̶i̶n̶t̶a̶i̶n̶e̶d̶,̶ ̶w̶e̶ ̶d̶o̶n̶'̶t̶ ̶t̶e̶s̶t̶ ̶t̶h̶e̶m̶ ̶o̶n̶ ̶T̶r̶a̶v̶i̶s̶,̶ ̶w̶e̶ ̶d̶o̶n̶'̶t̶ ̶d̶i̶s̶t̶r̶i̶b̶u̶t̶e̶ ̶t̶h̶e̶m̶,̶ ̶a̶n̶d̶ ̶w̶e̶ ̶h̶a̶v̶e̶ ̶n̶o̶ ̶s̶t̶a̶n̶d̶a̶r̶d̶s̶ ̶f̶o̶r̶ ̶P̶R̶ ̶c̶o̶d̶e̶-̶r̶e̶l̶a̶t̶e̶d̶ ̶d̶o̶c̶u̶m̶e̶n̶t̶a̶t̶i̶o̶n̶.̶ ̶I̶n̶ ̶f̶a̶c̶t̶,̶ ̶t̶h̶e̶ ̶c̶u̶r̶r̶e̶n̶t̶ ̶o̶u̶t̶p̶u̶t̶ ̶i̶s̶ ̶u̶n̶f̶o̶r̶t̶u̶n̶a̶t̶e̶l̶y̶ ̶n̶o̶t̶ ̶v̶e̶r̶y̶ ̶h̶e̶l̶p̶f̶u̶l̶.̶ ̶W̶h̶a̶t̶ ̶c̶a̶n̶ ̶w̶e̶ ̶d̶o̶ ̶t̶o̶ ̶i̶m̶p̶r̶o̶v̶e̶ ̶t̶h̶i̶s̶ ̶s̶i̶t̶u̶a̶t̶i̶o̶n̶?̶

I̶n̶ ̶m̶y̶ ̶o̶p̶i̶n̶i̶o̶n̶,̶ ̶a̶ ̶f̶i̶r̶s̶t̶ ̶s̶t̶e̶p̶ ̶w̶o̶u̶l̶d̶ ̶b̶e̶ ̶t̶o̶ ̶m̶i̶g̶r̶a̶t̶e̶ ̶t̶o̶ ̶a̶ ̶s̶l̶i̶g̶h̶t̶l̶y̶ ̶m̶o̶r̶e̶ ̶m̶o̶d̶e̶r̶n̶ ̶t̶o̶o̶l̶ ̶c̶h̶a̶i̶n̶,̶ ̶̶o̶d̶o̶c̶̶.̶ ̶̶o̶d̶o̶c̶̶ ̶i̶s̶ ̶u̶s̶e̶d̶ ̶a̶m̶o̶n̶g̶ ̶o̶t̶h̶e̶r̶ ̶p̶r̶o̶j̶e̶c̶t̶s̶ ̶b̶y̶ ̶t̶h̶e̶ ̶J̶a̶n̶e̶ ̶S̶t̶r̶e̶e̶t̶ ̶l̶i̶b̶r̶a̶r̶i̶e̶s̶ ̶s̶t̶a̶c̶k̶ ̶s̶o̶ ̶i̶t̶ ̶i̶s̶ ̶a̶ ̶m̶a̶t̶u̶r̶e̶ ̶t̶o̶o̶l̶.̶ ̶S̶e̶c̶o̶n̶d̶,̶ ̶i̶n̶ ̶o̶r̶d̶e̶r̶ ̶t̶o̶ ̶o̶r̶g̶a̶n̶i̶z̶e̶ ̶A̶P̶I̶ ̶d̶o̶c̶u̶m̶e̶n̶t̶a̶t̶i̶o̶n̶,̶ ̶w̶e̶ ̶c̶o̶u̶l̶d̶ ̶t̶a̶k̶e̶ ̶p̶r̶o̶f̶i̶t̶ ̶f̶r̶o̶m̶ ̶t̶h̶e̶ ̶m̶o̶d̶u̶l̶a̶r̶ ̶r̶e̶-̶o̶r̶g̶a̶n̶i̶z̶a̶t̶i̶o̶n̶ ̶p̶e̶r̶f̶o̶r̶m̶e̶d̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶a̶s̶t̶ ̶m̶o̶n̶t̶h̶s̶ ̶[̶c̶.̶f̶.̶ ̶ ̶#̶6̶5̶2̶,̶ ̶#̶6̶0̶0̶8̶,̶ ̶a̶n̶d̶ ̶m̶a̶n̶y̶ ̶m̶a̶n̶y̶ ̶o̶t̶h̶e̶r̶ ̶c̶o̶m̶m̶i̶t̶s̶]̶.̶
̶
I̶n̶d̶e̶e̶d̶,̶ ̶C̶o̶q̶ ̶i̶s̶ ̶j̶u̶s̶t̶ ̶a̶ ̶f̶e̶w̶ ̶l̶i̶n̶e̶s̶ ̶s̶h̶y̶ ̶o̶f̶ ̶b̶e̶c̶o̶m̶i̶n̶g̶ ̶a̶ ̶t̶r̶u̶l̶y̶ ̶m̶o̶d̶u̶l̶a̶r̶ ̶s̶y̶s̶t̶e̶m̶ ̶[̶o̶t̶h̶e̶r̶ ̶t̶h̶a̶n̶ ̶f̶o̶r̶ ̶s̶t̶a̶t̶i̶c̶ ̶i̶n̶i̶t̶i̶a̶l̶i̶z̶a̶t̶i̶o̶n̶ ̶w̶o̶e̶s̶]̶,̶ ̶a̶n̶d̶ ̶i̶t̶ ̶s̶e̶e̶m̶s̶ ̶I̶'̶d̶ ̶m̶a̶k̶e̶ ̶s̶e̶n̶s̶e̶ ̶t̶o̶ ̶t̶h̶e̶n̶ ̶e̶x̶p̶o̶s̶e̶ ̶t̶h̶e̶ ̶A̶P̶I̶ ̶d̶o̶c̶u̶m̶e̶n̶t̶a̶t̶i̶o̶n̶ ̶i̶n̶ ̶a̶ ̶m̶o̶d̶u̶l̶a̶r̶ ̶f̶o̶r̶m̶.̶ ̶T̶h̶e̶ ̶u̶p̶c̶o̶m̶i̶n̶g̶ ̶D̶u̶n̶e̶ ̶P̶R̶ ̶#̶6̶8̶5̶7̶ ̶m̶a̶k̶e̶s̶ ̶g̶e̶n̶e̶r̶a̶t̶i̶n̶g̶ ̶̶o̶d̶o̶c̶̶ ̶m̶o̶d̶u̶l̶a̶r̶ ̶d̶o̶c̶u̶m̶e̶n̶t̶a̶t̶i̶o̶n̶ ̶t̶r̶i̶v̶i̶a̶l̶,̶ ̶s̶o̶ ̶I̶M̶H̶O̶ ̶w̶e̶ ̶c̶o̶u̶l̶d̶ ̶t̶a̶k̶e̶ ̶p̶r̶o̶f̶i̶t̶ ̶f̶r̶o̶m̶ ̶i̶t̶.̶

I think it makes sense to split the TODO list in two categories, "infrastructure" and "documentation"

Infrastructure:

  • Finish modularization, add preliminary Dune support.
  • Test API document build on Travis. Add a prominent link in the README to master version.
  • Distribute API documents in releases, add link in web.

Documentation

I guess than once we are used to having the link to current docs, and these are part of the standard build we'll get used to writing better doc for OCaml code.

@ejgallego ejgallego added kind: documentation Additions or improvement to documentation. kind: infrastructure CI, build tools, development tools. kind: meta About the process of developing Coq. labels Apr 2, 2018
@Zimmi48
Copy link
Member

Zimmi48 commented Apr 2, 2018

I didn't know odoc but it seems that ocamldoc it's pretty much unmaintained if not deprecated, as @MatejKosik learned the hard way when he tried to have a warning free ocamldoc compilation. So if this new tool can help get a good inline doc of the APIs I'm all for it 😉

@ejgallego
Copy link
Member Author

ejgallego commented Apr 2, 2018

This is an example of how odoc looks like: https://ocaml.janestreet.com/ocaml-core/latest/doc/base/Base/index.html

So instead of base here we would have coq.kernel, etc...

@ejgallego ejgallego added this to Structural changes in API Apr 3, 2018
@ejgallego ejgallego added this to To do [in order-ish] in Dune Apr 24, 2018
ejgallego added a commit to ejgallego/coq that referenced this issue May 4, 2018
This is an experiment in trying to get a more uniform API by merging
together definitions with their operating interfaces. The main
motivation to help the API documentation work (coq#7155), but this also
has a net effect on the number of `open` needed in the codebase and no
downside I can see.

Also see discussions in coq#6512, coq/ceps#19 and
likely elsewhere.

IMO reducing the number of modules is a key point in order to make the
API accessible, if this PR finds some success the pattern:

```ocaml
open Foo
open Fooops
```

should hopefully go away.
ejgallego added a commit to ejgallego/coq that referenced this issue May 4, 2018
This is an experiment in trying to get a more uniform API by merging
together definitions with their operating interfaces. The main
motivation to help the API documentation work (coq#7155), but this also
has a net effect on the number of `open` needed in the codebase and no
downside I can see.

Also see discussions in coq#6512, coq/ceps#19 and
likely elsewhere.

IMO reducing the number of modules is a key point in order to make the
API accessible, if this PR finds some success the pattern:

```ocaml
open Foo
open Fooops
```

should hopefully go away.

cc: coq#7422
ejgallego added a commit to ejgallego/coq that referenced this issue May 4, 2018
This is an experiment in trying to get a more uniform API by merging
together definitions with their operating interfaces. The main
motivation to help the API documentation work (coq#7155), but this also
has a net effect on the number of `open` needed in the codebase and no
downside I can see.

Also see discussions in coq#6512, coq/ceps#19 and
likely elsewhere.

IMO reducing the number of modules is a key point in order to make the
API accessible, if this PR finds some success the pattern:

```ocaml
open Foo
open Fooops
```

should hopefully go away.

cc: coq#7422
ejgallego added a commit to ejgallego/coq that referenced this issue May 5, 2018
This is an experiment in trying to get a more uniform API by merging
together definitions with their operating interfaces. The main
motivation to help the API documentation work (coq#7155), but this also
has a net effect on the number of `open` needed in the codebase and no
downside I can see.

Also see discussions in coq#6512, coq/ceps#19 and
likely elsewhere.

IMO reducing the number of modules is a key point in order to make the
API accessible, if this PR finds some success the pattern:

```ocaml
open Foo
open Fooops
```

should hopefully go away.

cc: coq#7422
ejgallego added a commit to ejgallego/coq that referenced this issue May 7, 2018
This is an experiment in trying to get a more uniform API by merging
together definitions with their operating interfaces. The main
motivation to help the API documentation work (coq#7155), but this also
has a net effect on the number of `open` needed in the codebase and no
downside I can see.

Also see discussions in coq#6512, coq/ceps#19 and
likely elsewhere.

IMO reducing the number of modules is a key point in order to make the
API accessible, if this PR finds some success the pattern:

```ocaml
open Foo
open Fooops
```

should hopefully go away.

cc: coq#7422
@ejgallego ejgallego moved this from To do [in order-ish] to Optional / After merge in Dune May 10, 2018
ejgallego added a commit to ejgallego/coq that referenced this issue May 21, 2018
This is an experiment in trying to get a more uniform API by merging
together definitions with their operating interfaces. The main
motivation to help the API documentation work (coq#7155), but this also
has a net effect on the number of `open` needed in the codebase and no
downside I can see.

Also see discussions in coq#6512, coq/ceps#19 and
likely elsewhere.

IMO reducing the number of modules is a key point in order to make the
API accessible, if this PR finds some success the pattern:

```ocaml
open Foo
open Fooops
```

should hopefully go away.

cc: coq#7422
ejgallego added a commit to ejgallego/coq that referenced this issue Jun 2, 2018
ejgallego added a commit to ejgallego/coq that referenced this issue Jun 2, 2018
cc: coq#7155

We also need to remove a duplicated spurious file as for the doc build not to fail.
ejgallego added a commit to ejgallego/coq that referenced this issue Jun 2, 2018
cc: coq#7155

We also need to remove a duplicated spurious file as for the doc build not to fail.
@ejgallego
Copy link
Member Author

So #6857 provides a make -f Makefile.dune apidoc target that will build the current ML API documentation. Example here:

https://coq.gitlab.io/-/coq/-/jobs/72015056/artifacts/_build/default/_doc/_html/coq/index.html

Still a looong way to go; in particular we need improve the intro page. Wrapping the modules would help, but on the other hand it would create a mess (maybe we could wrap for documentation only?)

The old documentation system also had some interesting goodies, such as the dependency generation. Maybe we should preserve them.

Anyways the odoc and ocamldoc syntax are compatible, so I am enabling the generation of ML docs artifacts (#7684) so we can start to work on the documentation itself. See the artifacts here:

ejgallego added a commit to ejgallego/coq that referenced this issue Jun 3, 2018
cc: coq#7155

Changes:

- we remove a spurious duplicated file
- [docker]
  + `source-doc` requires textlive-science
  + `hevea` is not used anymore
ejgallego added a commit to ejgallego/coq that referenced this issue Jun 3, 2018
cc: coq#7155

Changes:

- we remove a spurious duplicated file
- [docker]
  + `source-doc` requires textlive-science
  + `hevea` is not used anymore
ejgallego added a commit to ejgallego/coq that referenced this issue Jun 3, 2018
cc: coq#7155

Changes:
- [general] we remove a spurious duplicated file;
- [docker]:
  + `source-doc` requires textlive-science
  + `hevea` is not used anymore
ejgallego added a commit to ejgallego/coq that referenced this issue Jul 13, 2018
cc: coq#7155

Changes:
- [general] we remove a spurious duplicated file;
- [makefile] we remove the `SPHINXENV` hack in favor of std variables.
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
cc: coq#7155

Changes:
- [general] we remove a spurious duplicated file;
- [makefile] we remove the `SPHINXENV` hack in favor of std variables.
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
cc: coq#7155

Changes:
- [general] we remove a spurious duplicated file;
- [makefile] we remove the `SPHINXENV` hack in favor of std variables.
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is still not optimal as we have to rebuild the `.cmi` files due
to local/global build flags. We should introduce a make variable
stating where the output of the build is.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is still not optimal as we have to rebuild the `.cmi` files due
to local/global build flags. We should introduce a make variable
stating where the output of the build is.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is still not optimal as we have to rebuild the `.cmi` files due
to local/global build flags. We should introduce a make variable
stating where the output of the build is.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 3, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: coq#7155
@ejgallego
Copy link
Member Author

OK so medium term, I would definitely support wrapping/packing.

Note that Dune supports now a "(wrapped transition "msg")" mode that could help in transitioning to a wrapped system; the current make system could be more of a headache but I think that Pierre did most of the work for us to be able to use .mlpack files so we may not be in such a bad shape.

@ejgallego
Copy link
Member Author

But plugins would have to use a Dune-built Coq in order to smooth the transition.

silene pushed a commit that referenced this issue Oct 2, 2018
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: #7155
(cherry picked from commit 5cc3e11)
@ejgallego
Copy link
Member Author

Update, since a few days the API doc artifacts are available at https://coq.inria.fr/api/master/

@ejgallego ejgallego removed the kind: meta About the process of developing Coq. label Oct 14, 2018
@Zimmi48
Copy link
Member

Zimmi48 commented Oct 15, 2018

Yep, that's a work by @maximedenes. However, as I suggested on Gitter, it should be https://coq.inria.fr/master/api instead so that the manual can be at https://coq.inria.fr/master/refman, etc.

@ejgallego
Copy link
Member Author

New odoc is almost ready by the way, and the docs change dramatically [for better IMO]

It would be interesting to make a task force to do passes on the ML files. They do need a lot of work, see:

https://ejgallego.gitlab.io/-/coq/-/jobs/108321332/artifacts/_build/default/_doc/_html/index.html

@ejgallego
Copy link
Member Author

Note that more documentation tooling is going to be added to Dune soon , see ocaml/dune#3094

I wonder if it is time to close this meta-issue in favor or smaller ones and a project; well, github now has the related-issue feature so that could help organize?

@Alizter Alizter moved this from Structural changes to To Do in API May 8, 2022
@Alizter
Copy link
Contributor

Alizter commented May 8, 2022

What is the status of this? I see that there used to be an explicit "API" but now we are going towards the route of properly documented libraries. Is the API project pretty much abandoned now?

@ejgallego
Copy link
Member Author

Yes, the API project is not active in its original form, tho we can still improve a lot of stuff.

I think the main missing thing here is the landing page, and high-level overview. Now we just have a dump of the libs; moreover, some core libs are just undocumented.

@Alizter Alizter added this to Meta issues in User documentation May 17, 2022
@Alizter Alizter moved this from Meta issues to Developer in User documentation May 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: documentation Additions or improvement to documentation. kind: infrastructure CI, build tools, development tools. kind: internal API, ML documentation...
Projects
API
  
To Do
Dune
  
Forward to Dune
Status: No status
User documentation
  
Developer
Development

No branches or pull requests

3 participants