odoc: Internal error, uncaught exception in src/odoc/env.ml

[ejgallego]

Using the tree at coq/coq#6857 I get from jbuilder build @doc:

(cd _build/default/_doc/_html && /home/egallego/.opam/4.06.1/bin/odoc html -I ../_odoc/lib/coq.checker -I ../_odoc/lib/coq.clib -I ../_odoc/lib/coq.config -I ../_odoc/lib/coq.engine -I ../_odoc/lib/coq.grammar -I ../_odoc/lib/coq.interp -I ../_odoc/lib/coq.kernel -I ../_odoc/lib/coq.lib -I ../_odoc/lib/coq.library -I ../_odoc/lib/coq.parsing -I ../_odoc/lib/coq.pretyping -I ../_odoc/lib/coq.printing -I ../_odoc/lib/coq.proofs -I ../_odoc/lib/coq.stm -I ../_odoc/lib/coq.tactics -I ../_odoc/lib/coq.toplevel -I ../_odoc/lib/coq.vernac -I ../_odoc/lib/coq.vm -o . ../_odoc/lib/coq.engine/termops.odoc)
WARNING: digest of ../_odoc/lib/coq.checker/names.odoc doesn't match the one excepted for file Names
odoc: internal error, uncaught exception:
      File "src/odoc/env.ml", line 82, characters 6-12: Assertion failed
      Raised at file "src/odoc/env.ml", line 82, characters 6-38
      Called from file "src/odoc/env.ml", line 128, characters 8-45
      Called from file "src/xref/component_table.ml", line 276, characters 16-35
      Called from file "src/xref/component_table.ml", line 349, characters 19-47
      Called from file "src/xref/component_table.ml", line 349, characters 19-47
      Called from file "src/xref/component_table.ml" (inlined), line 596, characters 4-32
      Called from file "src/xref/resolve.ml", line 155, characters 32-63
      Called from file "src/xref/resolve.ml", line 368, characters 12-50
      Called from file "src/model/maps.ml", line 1895, characters 19-33
      Called from file "src/model/maps.ml", line 1887, characters 21-35
      Called from file "src/model/maps.ml", line 1887, characters 21-35
      Called from file "src/model/maps.ml", line 1502, characters 16-30
      Called from file "src/model/maps.ml", line 1192, characters 19-29
      Called from file "list.ml", line 82, characters 20-23
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "list.ml", line 82, characters 32-39
      Called from file "src/model/maps.ml", line 10, characters 30-42
      Called from file "src/model/maps.ml", line 1991, characters 23-37
      Called from file "src/model/maps.ml", line 2011, characters 19-36
      Called from file "src/xref/resolve.ml" (inlined), line 2055, characters 18-32
      Called from file "src/odoc/html_page.ml", line 51, characters 21-65
      Called from file "src/cmdliner_term.ml", line 27, characters 19-24
      Called from file "src/cmdliner.ml", line 106, characters 32-39

This is odoc master. In general, I am having a bit of trouble building the ML documentation for Coq with odoc, see also #111

[ejgallego]

This is likely due to Coq shipping to Names modules in the same namespace but for different binaries.

We will wrap modules ASAP, but for now we cannot do a lot, maybe we could move the checker to a different package but we have a couple of issues due to dependencies.

[pmetzger]

Regardless of how unusual Coq's documentation might be, it should not cause the tool to die with an internal error.

[aantron]

@lpw25, I created a minimal repo that reproduces this failure:

git clone git@github.com:aantron/odoc-148-repro.git
cd odoc-148-repro
git clone git@github.com:ocaml/odoc.git
dune build @doc --verbose

That sequence should trigger it (it needs an opam switch with the deps of odoc installed). There is a small project in the repo's reprodirectory. In it, there are two sublibraries, both with wrapped false, and each with a module Names. wrapped false prevents the names from being decorated, which would prevent triggering of the bug.

The sublibraries don't depend on each other, however I suspect Dune is being too liberal with its -I flags.

The files read for the two Names modules have different digests, because, at the least, the files contain location information with different source paths.

Could you please take a look, and see if you can diagnose this quickly? I am still quite unfamiliar with these parts of odoc.

[trefis]

That's a bug in dune's odoc rules indeed.
As an aside: dune knows there is a problem with that setup, it does print:

Multiple rules generated for _build/default/_doc/_html/repro/Names/index.html:
- <internal location>
- <internal location>

Anyway, Env does make the assumption that unit names are unique in odoc's loadpath. Which is consistent with the compiler, which makes that same assumption.
I guess one thing that could be done in this case is to fail properly earlier on (when we warning that the digest doesn't match what we except), instead of tripping on that assert.

An even better solution (which requires more work though) would be to scan eagerly the loadpath on startup.
So we could report any problem (incl. duplicated unit names) properly earlier in the process.

[trefis]

An even better solution (which requires more work though) would be to scan eagerly the loadpath on startup.

For the record, the compiler will itself start doing that eager scan with 4.08. So I don't think we'd have any performance issue that wouldn't also be experienced by the compiler if we start doing that.

[jonludlam]

I'll take a look at this one if nobody else is right now.

[aantron]

I don't think anyone actively is.

To get started, I suggest running dune build @doc --verbose on the repro repo linked above, and comparing the -I flags added by Dune to the odoc calls with the -I flags added to ocamlc/ocamlopt/ocamldep calls. It is likely that Dune is adding more flags to odoc.

Separately, we should replace the assertion failure with some better error message.

[jonludlam]

Yep, got the repro working (failing!). I'll try the eager scan method first to report the problem as early as possible, and can probably look at the Dune problem next week.

[jonludlam]

In the repro, the problem happened when building the html for repro.two:

odoc html -I ../_odoc/lib/repro.one -I ../_odoc/lib/repro.two -o . ../_odoc/lib/repro.two/two.odoc
WARNING: digest of ../_odoc/lib/repro.one/names.odoc doesn't match the one expected for file Names
odoc: internal error, uncaught exception:
      File "src/odoc/env.ml", line 84, characters 6-12: Assertion failed
...

and since repro.two doesn't depend upon repro.one, this seems to be a bug in dune where it's including too much in the include paths. However, the verbose log also shows a few more interesting details. Firstly:

Multiple rules generated for _build/default/_doc/_html/repro/Names/index.html:
- <internal location>
- <internal location>

as @trefis points out, dune's aware of a problem here. However, this isn't the same problem - it's genuinely true that there are two modules called 'Names' in different libraries that, because we're generating documentation for the entire package and not just the libraries, end up with the same filename. This isn't 'wrong' at all - the two libraries might not be intended to be linked together into the same binary (as is the case with the coq issue that we started with).

Furthermore, looking at more log from the verbose doc build, we see:

odoc html -I ../_odoc/lib/repro.one -I ../_odoc/lib/repro.two -o . ../_odoc/pkg/repro/page-index.odoc

here it's building the package-level index of modules. This necessarily has to have both libraries on the include path, so this isn't a dune problem. This implies that odoc should try to handle (or at least, not die horribly) the case where there are multiple modules with the same name in different places. I've made PR #270 to do this. If we really want to try to support this properly then we should also be putting the output in library-specific paths.

Personally though, I feel we should be pushing people to wrap their libraries which would avoid this issue altogether rather than reworking the output layout for this corner case.

[jonludlam]

I believe we can close this issue now that #270 has been merged.