Generate scaladoc of unstable

[konnov]

As we discussed today, we are lacking internal developer's documentation. Although the methods in the new code are usually well-documented, there is no good overview of each package. Additionally, the documentation is written for someone who would maintain the code, not use the code as an API. That is, there is an implicit assumption that the developers of a package have to read its codebase, even if they do not want to change it.

We should improve this situation. The most economic way is probably to write the developer's documentation in javadoc itself. We can draw some inspiration from Java's javadoc, e.g., collections.

The next question is how we should publish the api doc. We can add a target to sbt. In my experience, however, developers would not call this target just to read the docs. IMO, a more effective way is to publish the javadoc of unstable somewhere, e.g., at github pages. What do you think @shonfeder?

[shonfeder]

i expect there is an sbt plugin or boilerplate configuration to publish the docs. Shouldn't be too hard to integrate that with our existing docs publication hopefully.

[konnov]

I am also sure that there is an sbt plugin that does everything locally. Publishing the docs at GH is probably a bit harder.

[shonfeder]

Yep. The given our current status, I'd say the easiest and most impactful step is to just add an sbt target to build and browse the API docs. That will free us up to use that view in our local development and should drive improvement of the quality of our docs.

Publishing a hosted view into the docs shouldn't be too hard, but also, imo, that value of that at this point is a bit more speculative?

[konnov]

Publishing a hosted view into the docs shouldn't be too hard, but also, imo, that value of that at this point is a bit more speculative?

It's a bit like tests in the CI. If you run tests locally, it is somehow less impactful. We could also introduce some linter for javadoc to see how many holes we have.

[shonfeder]

I'm not sure if that analogy pans out: tests in CI make a huge difference because they give automatic feedback that guarantees no changeset with failing tests gets into the trunk. But, iiuc, there's nothing about us publishing the scala doc that gives automatic feedback that guarantees anything. Linting or coverage might help in this way tho.

[konnov]

I have just tried to generated scaladoc. Indeed, it is supposed to be easy. Just type sbt doc. There are several problems though:

• Currently, we have 14 warnings. It would be good to have sbt doc as part of the CI, so we could find issues with the documentation fast.
• The documentation layout is far from perfect. I have to go to each individual module, e.g., tlair/target/scala-2.13/api/. I think Scalatest does it reasonably well. They have tutorials, manuals, and Scaladoc. I don't think we need Scaladoc per package version, as they do, but having it easily accessible would definitely ease onboarding.

[konnov]

Also, it looks like sbt doc does not generate documentation for the classes inside src/test, which makes it hard to read documentation such as in: https://github.com/informalsystems/apalache/pull/1986

[thpani]

@konnov sbt test:doc works

[shonfeder]

Looks like we can use https://github.com/sbt/sbt-unidoc or similar to generate scaladoc for the the multi-project in a unified way. Will investigate how it interacts with tests.

[konnov]

sbt-unidoc looks right the right solution!

[shonfeder]

Cool. I'll integrate this week. We can see how it works running locally at first (hopefully with a one-line command that will also open the docs in our browser) and run the doc generation in CI to catch errors.

If we end up wanting to also publish the docs on the website, we can do that as a followup?

[shonfeder]

This was not fully closed by #1997. Still to do:

• [ ] Make it easy for devs to render and brows the docs
• [ ] Build and include the test docs

I'll argue that a new ticket should be opened to publish the docs on the website should we still want that after these two features are available.