Why3doc is too fragile in presence of multiple files
Consider a command line why3 doc -L . ./foo.mlw ./bar.mlw
and assume that bar.mlw
depends on a theory foo.Foo
(hence the need for -L .
). Why3 first reads ./foo.mlw
in isolation; that is fine. Then it reads ./bar.mlw
, which depends on ./foo.mlw
(and it is exactly ./foo.mlw
due to -L .
). So, Why3 also loads foo
as a library. But it has already registered tons of definitions in ./foo.mlw
, so all the definition of foo.Foo
are dropped. As a consequence, any use of a symbol of foo.Foo
in bar.mlw
will be assumed to be from the current file, since that is what foo.mlw
was at the time it was first parsed. All the corresponding links are thus broken.
There are two potential workarounds:
- Make sure the files are in syntactically different locations, e.g.,
why3 doc -L . foo.mlw bar.mlw
. - Make sure the files are documented after they have been already used once, e.g.,
why3 doc -L . ./bar.mlw ./foo.mlw
.
This breaks hundreds of links in the documentation of Why3's standard library. Workaround 1 will be used there. But this still needs to be fixed properly.