idris-lang/Idris-dev

IdrisDoc doesn't create docs for Data.Fin

melted opened this issue · 8 comments

When running idris --mkdoc base.ipkg, docs aren't built for some modules and it outputs the following:

Warning: Ignoring empty or non-existing namespace 'Syntax.PreorderReasoning'
Warning: Ignoring empty or non-existing namespace 'Data.Fin'
Warning: Ignoring empty or non-existing namespace 'Control.Monad.Trans'
Warning: Ignoring empty or non-existing namespace 'Control.Monad.State'
Warning: Ignoring empty or non-existing namespace 'Control.Monad.Writer'
Warning: Ignoring empty or non-existing namespace 'Control.Monad.Reader'
Warning: Ignoring empty or non-existing namespace 'Control.IOExcept'

Reported by DanC on IRC.

uwap commented

I have encountered a similar bug after working on #2494. It seems that nonEmpty in fetchInfo (https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/IdrisDoc.hs#L155) gets wrong data.

While some Modules that were ignored appear in nonOrphan and reachedNss they don't seem to appear in nonEmpty. I'm not too deep into those things.

Would be glad if someone would look into that

jfdm commented

So on Idris version 0.11 this is now reporting that only two packages are not being added to the doc generation output. Syntax.PreorderReasoning and Control.Monad.Trans.

I'm seeing this issue as well on my package(github.com/superfunc/tp) where no docs are being generated.

repro:

$ git clone https://github.com/superfunc/tp
$ cd tp
$ idris --mkdoc tp.ipkg
Type checking src/System/Posix/Paths.idr
Type checking src/Test/System/Posix/Paths.idr
Warning: Ignoring empty or non-existing namespace 'System.Posix.Paths'
Warning: Ignoring empty or non-existing namespace 'Test.System.Posix.Paths'
No namespaces to generate documentation for

When I believe there are public, and validly doc'd functions and types.

What I found today:

Idris.IdrisDoc.getAccess returns Hidden for every member of Data.Nat.Views, which is why there are no docs for Data.Nat.Views members.

This can be found in the logs, from IBC.hs:

Setting (hidden,Data.Nat.Views.Half) to hidden
Not exporting Data.Nat.Views.Half
Setting (hidden,Data.Nat.Views.HalfEven) to hidden
Not exporting Data.Nat.Views.HalfEven
Setting (hidden,Data.Nat.Views.HalfOdd) to hidden
Not exporting Data.Nat.Views.HalfOdd
Setting (hidden,Data.Nat.Views.HalfRec) to hidden
Not exporting Data.Nat.Views.HalfRec
Setting (hidden,Data.Nat.Views.HalfRecEven) to hidden
Not exporting Data.Nat.Views.HalfRecEven
Setting (hidden,Data.Nat.Views.HalfRecOdd) to hidden
Not exporting Data.Nat.Views.HalfRecOdd
Setting (hidden,Data.Nat.Views.HalfRecZ) to hidden
Not exporting Data.Nat.Views.HalfRecZ
Setting (hidden,Data.Nat.Views.half) to hidden
Not exporting Data.Nat.Views.half
Setting (hidden,Data.Nat.Views.halfRec) to hidden
Not exporting Data.Nat.Views.halfRec

This appears to be in the case that a module is included though a second module, but not re-exported, so the names are hidden, which could be happening here. This last part might be a dead end.

I'm going to sleep on it. Any thoughts welcome.

documentPkg uses loadModule to load the modules (apparently it is the only consumer of that function that doesn't have the REPL flag set, which makes everything visible). loadModule does nothing when an already loaded IBC is put in there, so the Hidden flag that is set on Data.Nat.Views is never adjusted because it's not loaded in it's own right.

I'm still looking at this - (slowly, and when I have time). I don't think there's an easy solution. I suspect that access is modeled in a way that only works for having one top-level code module loaded at a time.

@melted I suspect that your previous patch would have made different modules inaccessible based on load order, and I've observed that load order from a package isn't necessarily consistent.

I think the underlying problem is that the accessibility of top-level names is stored with those top-level names, as if this is a property of the object (it's not, it is a relationship between the caller and callee specified by modules). In places, we make names globally inaccessible because the names were not re-exported from an imported module. We then patch this up by making names reaccessible when re-importing a module which has been imported "Private" (note that this will, again, hide definitions which are imported into this module and not reexported). We lose the intended access of the definitions whenever we make something public for the REPL (see #1209) or hidden through, so we need to reload from disk.

I'm currently figuring how the accessibility is used to figure out if there's a simpler, more accurate way to model this that doesn't require a janky state machine to manipulate accessibility. That'll take a while.

@melted I worked it out and now agree that your approach works. I'm going to move on to another ticket.