[ docs ] Build IdrisDoc in a namespace.

[jfdm]

When invoking idris2 --mkdocs foobar.ipkg, the current behaviour is for the compiler to dump the documentation in ${builddir}/docs. The location ${builddir}/docs is used regardless of the package name. Thus for projects that present multiple packages the docs build directory will become polluted and corrupt if the developer is not careful. This one change ensures that for package x the documentation is generated in the directory: ${builddir}/docs/x.

Idris2 Makefile has been updated to reflect the change.

Should this change go in the CHANGELOG?

• [x] If this is a user-facing change or a compiler change, I have updated CHANGELOG.md (and potentially also CONTRIBUTORS.md).

[gallais]

IIUC this will require us to update the CI script that generates the docs automatically:

https://github.com/idris-lang/Idris2/blob/45fc038300979a9e3ff7799e8c22f3fc80b4014d/.github/scripts/katla.sh#L23

Something like:

-     cp -r "$prefix"/"$libname"/build/docs/* html/"$libname"
+     cp -r "$prefix"/"$libname"/build/docs/"$libname"/* html/"$libname"

[jfdm]

Ah good catch! I thought I had updated everything that used the docs.

[jfdm]

I will leave this open until Tuesday, when I will merge it.

[gallais]

I don't know what to think.

On the one hand it allows you to know the output you're looking at will only talk about that one package's content, on the other hand it breaks sharing (or are we always recomputing the html docs no matter what?).

Basically: why is this necessary for mkdocs but not build?