vernac/declaremods: make object collection tail-recursive

[gasche]

This patch is trying to upstream a jsCoq patch that was written to
solve Stack Overflow issues:

https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/cps.patch

It turns List.fold_right in vernac/declaremods into List.fold_left
followed by List.rev (the output of the fold is a list which is now
constructed in reverse order).

My naive understanding of the code is that the order in which the
collection is performed should not be observable,
only the order of elements in the output, so that the switch from
List.fold_right to List.fold_left should be correct. In particular,
notice that some slight effects (calling Lib.make_oname) were called
from right to left in the collect_* functions, and then from left to
right in the open_* functions.

Of course, reality differs: this modification appears to change
parameter resolution in an obscure use of a pow_N function in
Ncring_tac.v. The existing code would break, and I now have to pass
the (previously implicit) parameters explicitly.

I am not sure whether it means that the current change should be
thrown in the garbage bin (it breaks code), or that there is a bug
somewhere else (sounds somewhat likely to me).

Kind: performance (stack space usage).

(I cannot tell if this change would require an entry in the changelog.)

[SkySkimmer]

In particular, notice that some slight effects (calling Lib.make_oname)

That's just a record builder, no effects there

[SkySkimmer]

It turns List.fold_right in vernac/declaremods into List.fold_left
followed by List.rev (the output of the fold is a list which is now
constructed in reverse order).

Why not do the rev first? IIUC it would be closer to what we do currently.

[gasche]

That's just a record builder, no effects there

Ah, I assumed that there was some "fresh name" effect in KerName.make but I checked and indeed you are correct. Thanks!

Why not do the rev first? IIUC it would be closer to what we do currently.

First, I find reverse-after more natural (it's the standard approach for tail-recursive processing of lists). Second, it is more efficient if the number of exported objects is noticeably smaller than the number of processed objects, which sounds likely to me (but then I don't actually understand that code and how it is used). Third, reverse-before makes it harder to work with items that themselves generate lists, as in collect_module_objects (I have to reverse those lists as well, etc.).

This being said, "less natural and vaguely less efficient and less readable" is better than "unexplained failure", so I may try that if the other change you suggested (thanks!) does not fix the issue.

[gasche]

I pushed a commit implementing the reverse-first approach, and it seems that the breakage in Ncring_tac.v is gone. I would have a small preference for knowing why it breaks, but I can't investigate myself, and avoiding a stack overflow is better than not.

[gasche]

Note: I pushed the previous approach (reverse at the end, breaks one line of code in the stdlib) to a dedicated branch export-tail-recursive-broken, the commit is gasche@852b8c3 . This is in case anyone is curious to investigate why this looking-ok change breaks things. But I realize that you may all have more urgent bugs to hunt that a maybe-not-a-bug in a version of the code that was easily replaced by a fully-correct alternative in this PR.

[SkySkimmer]

@gasche please rebase for fresh CI (elpi failure looks spurious)

@ejgallego I'm taking the assignment considering nothing happened since you assigned.

[gasche]

Thanks, I just rebased the PR.

[ejgallego]

@ejgallego I'm taking the assignment considering nothing happened since you assigned.

Thanks for the help, I wanted to investigate the problems with the first approach and get to investigate this code, but didn't get to it in time.

[SkySkimmer]

@coqbot: merge now