What is elpi_trace_elaborator? Shouldn't it move to libexec?

[SnarkBoojum]

While updating the elpi package in Debian, one of the tools complains that there is no associated manpage. Indeed, if it ends up in a user's path, an executable should have an associated manpage.

If it isn't supposed to be called directly by the user, then it shouldn't be installed in a user's path - it should end up in a libexec/ directory rather than a bin/ directory.

[gares]

It is called by the vscode extension. I don't know the convention for these binaries.

[SnarkBoojum]

If an executable is supposed to be ised directly by users, it belongs to some bin/ directory; if it's purely internal to something else then it should go to a libexec/ directory. In that case it looks like it's internal.

[gares]

I recall that, but it is not elpi that calls it, rather the vscode extension. So please, before moving it outside of the PATH, we should make the vscode extension also try to look into libexec, or patch elpi REPL to execute the other tool on demand.