Description
The documentation says:
Tail call is not optimized in general. However, mutually recursive functions are optimized: self recursive functions (when the tail calls are the function itself) are compiled using a loop. trampolines are used otherwise.
However, this seems not to be the case in a particular part of Coq, see ejgallego/jscoq#13.
In particular, calls to generic_search with large arguments result in stack overflows. They are 100% correlated to the argument size. I need to investigate more, but in particular the codepath here is:
generic_search
https://github.com/ejgallego/coq/blob/jscoq-patchqueue/toplevel/search.ml#L94- which calls
iter_declarations, which in turn is just a wrapper for
https://github.com/ejgallego/coq/blob/jscoq-patchqueue/toplevel/search.ml#L91 Declaremods.iter_all_segments
https://github.com/ejgallego/coq/blob/jscoq-patchqueue/library/declaremods.ml#L936
which basically does:
MPmap.iter apply_mod_obj (ModObjs.all ());
List.iter apply_node (Lib.contents ())with MPmap.iter being the regular Map.iter.
Where did things go wrong?
Maybe some cMap trickery could be getting on the way?
https://github.com/ejgallego/coq/blob/jscoq-patchqueue/lib/cMap.ml
An example script illustrating the problem is at https://x80.org/collacoq/xupufegeno.coq We basically add enough definitions to the environnement such that iter will SO.