IdrisDoc doesn't create docs for Data.Fin

[melted]

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]

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]

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.

[superfunc]

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.

[eraserhd]

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.

[melted]

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.

[eraserhd]

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]

In loadIBC in IBC.hs there is logic for that, a module that has been previously loaded but not reexported from the module that loaded it is fixed up if it is loaded explicitly. Problem is that loadModule looks at the imported list and quits before it calls that. My patch worked fine except for there not being any check for duplicates in the imported list. Also I'm not happy with the existence of both imported and idris_import in IState. The docgen also seems to have trouble with internal namespaces.

…

3 sep. 2017 kl. 18:43 skrev Jason Felice ***@***.***>: 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. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[eraserhd]

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