wish: jump to ckauses in the builtin file

[gares]

currently does not work

[VojtechStep]

I briefly looked into this, so I'm making this note for future reference: the problem is that elpi doesn't use files for builtins. The data of the builtins is kept in the executable (e.g. in elpi or in rocq-elpi), and this data is bundled into virtual files with hardcoded file names (e.g. 1, 2), and passed to the runtime when starting the program (e.g. 1, 2). This data is then printed and parsed in the compiler. At no point is this data materialized on disk.

I was thinking that a program processing a trace might just print the builtins to a virtual buffer, but that won't work in general, since each runner can provide a completely different set of builtins, so some cooperation with the runner is required.

What do we think about having a content-addressed store in a predictable location (maybe XDG_CACHE_HOME/elpi/<hash> on Unix platforms), and adding an API for dumping the builtins there? Maybe at first it would be okay to put it there when elpi is invoked with tracing enabled, but that won't cover the case when I want to send a trace to a friend (and it'd be nice if they didn't have to run a dummy traced program to seed the store).

[VojtechStep]

... or we can just dump all of the builtins as metapackets in the trace... Maybe throw in the user's source files as well; then all jump-to-definition buffers can be virtual!