Statically enforce that all the logging options are documented

[gallais]

At the moment we have quite extensive (and everyday expanding) logging options
to get Idris to print more debug output. However these are not documented anywhere
and the best way to discover them is by grepping the source code. This is less
than ideal.

In Idris.Env we use a nifty trick to ensure that all of the environment variables we
attempt to observe in the codebase are thoroughly documented.

It would be nice to have the same enforcement for logging options.

NB: there are 450+ uses of log in the codebase so it'll take a bit of time to
collect all of the existing topics. The documentation part can be left for a future
PR: having an exhaustive list would already be pretty useful!

[AdamBrouwersHarries]

I think I could tackle this.

With the environment variables we don't need to deal with hierarchies of names, but as I understand it with logs we need to be able to deal with them (e.g. elab, elab.with etc). Do we want users to have to write out every possible "path" of log contexts/names, or do we want a smarter way of doing it (e.g. checking membership of a tree structure of some sort).

[gallais]

There are two aspects to this:

• Declaring all of the topics of interest & enforcing the log functions
  can only be called with one such topic
• Generating the documentation

I think you are right that it would be good to print the whole thing not as a list
but as a hierarchical structure. We could do so by reusing (parts of) our existing
functions in Core.Options.Log to generate a trie of documentation strings & printing it nicely.

It's probably worth writing this printer generically for any Libraries.Data.StringTrie

This trie could also be used to efficiently perform the check needed in the first
part of the problem.

[AdamBrouwersHarries]

Declaring topics of interest is what I was specifically referring to, but generating documentation is something I'd not considered, and definitely something that should go into the design.

To clarify, what I was asking was whether "declaring" a topic of interest should be done in a "list like" way, i.e.

topics : List String 
topics = [
    "core", 
    "core.elab",
    "syntax"
]
-- etc

or if it should be done in a "tree like" way, i.e.

-- or equivalent structure
record LogTree where 
    constructor MkTree
    name : String 
    children : List LogTree

-- We can't have "" as the top level name, as otherwise we will require `.core.elab`
options : List LogTree
options = [
    MkTree "syntax" [], 
    MkTree "core" [
        MkTree "elab" [], 
        MkTree "data" []
    ]
]
    

I think there are good arguments for both - the former is a bit more readable I think, but the latter does make the tree a bit more explicit.

[gallais]

I think it should be done like this:

topics : StringTrie String
topics = foldr insert Trie.empty [
    ("core", "Anything related to core")
    -- ^     ^- the associated doc
    -- |
    -- a topic
    ...

where insert : (String, String) -> StringTrie String -> StringTrie String
can be put together by using the topic-parsing logic we have in
Core.Options.log together with the lib functions on tries.

[AdamBrouwersHarries]

How does this work for adding "subtopics"? Do we add them as discrete topics (e.g. core.elab), and then later (i.e. at query or doc generation time) break them into a topic "tree"?

[gallais]

insert into the StringTrie will break down "core.elab" into ["core", "elab"]
(cf. the logic in parseLogLevel) and use that as the path to insert the documentation
into the trie

Query should perform the same split & use StringTrie's lookup that focuses on the
subtree pointed at by the path (apparently it's not part of the library yet: we need
lookup : List String -> StringTrie a -> Maybe (StringTrie a)).

i.e. a topic is valid if the topic (or any subtopic) is documented.
so elab is valid even if elab is not documented but elab.def and elab.data are,
it just acts as a synonym for all of its subtopics.

[AdamBrouwersHarries]

Thanks! That helps clarify a lot. I'll look into StringTrie properly, as it definitely seems that I'm missing some knowledge there.

[AdamBrouwersHarries]

So I've had a hack and think I have a working-ish prototype. The only trouble is that I think Idris2' auto search is not deep enough to be able to effectively search within a trie structure. See the following gist for an example: https://gist.github.com/AdamHarries/2dc75d1efd574cdc405401bd8d3ddc15

Essentially, the type checker complains that it can't find an implementation for a successful search, but also (when flipped around) will also complain that it can't find an implementation for an unsuccessful search. I think it must be giving up part-way, but I'm not well versed enough to know what I can do top ask Idris2 to keep searching.

[ShinKage]

You can use the %auto_implicit_depth <n> pragma to change the maximum depth for auto implicit search, the default value is 50. Obviously this will increase compile times, and it may hang if the search requires to much memory, but at least you can experiment with it. In my experience, if the datatype you are trying to construct automatically isn't branching deeply you can increase it far enough.

[gallais]

This is just doing normalisation though. The proof is extremely shallow
(a single Just constructor).

[gallais]

Is the problem that triefind is not seen as total and thus won't reduce
in the type? Try adding a %default total at the top of the file?