Skip to content

Reimplement the trace elaborator in TypeScript - #41

Open
VojtechStep wants to merge 10 commits into
LPCIC:masterfrom
VojtechStep:builtin-trace-elaborator
Open

Reimplement the trace elaborator in TypeScript#41
VojtechStep wants to merge 10 commits into
LPCIC:masterfrom
VojtechStep:builtin-trace-elaborator

Conversation

@VojtechStep

@VojtechStep VojtechStep commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

This does most of the work necessary for closing #12.

The basic change is reimplementing the trace elaborator in TypeScript. The current situation is weird, since the elaborator is not shipped with the extension, so we technically have two interfaces to version, the raw trace and the elaborated trace. With this change, the elaborated trace is an implementation detail of the extension, and elpi doesn't need to know about it at all (so the public interface of tracing gets reduced to these four types). I also think it wasn't great that the whole thing got materialized as a big JSON with the stack traces duplicated everywhere; not materializing them means way more object sharing. So I reimplemented the elaborator, and it works correctly on all the traces in the test suite. I also changed some of the assert falses to proper exceptions, but I don't think these code paths are ever tested.

With the elaboration being done on the client side, it would then be possible to deploy the trace explorer as a static site. I have a prototype that still needs polish that I want to upstream in a future PR.

I initially wanted to use the ocaml implementation and translate it with js_of_ocaml or wasm_of_ocaml, but looking at the commit history of those projects quickly turned me away, so I did the port by hand.

I'm keeping this a draft until I add support for V1 traces (done) and port regression tests from the ocaml repo (done).

@VojtechStep
VojtechStep force-pushed the builtin-trace-elaborator branch from a51f511 to 6f50eab Compare July 24, 2026 23:03
This makes it easier to reuse when the trace explorer becomes a
standalone static HTML document
Options set to their less strict variants are options I'd like to
eventually make strict, but it's too much of a bother right now
@VojtechStep
VojtechStep force-pushed the builtin-trace-elaborator branch from 6f50eab to ca5982c Compare July 24, 2026 23:05
@VojtechStep

Copy link
Copy Markdown
Contributor Author

I just added elaboration testing. The JSONs are copied out of the elpi repo, and I'm using partialDeepStrictEqual because the OCaml atd-generated serializer skips optional fields with default values, while the TS generated one includes them (so the actual output has some extra more_failing_attempts: []). I'll fix those and switch to deepStrictEqual once I implement promotion

@VojtechStep
VojtechStep marked this pull request as ready for review July 26, 2026 15:30
@VojtechStep

Copy link
Copy Markdown
Contributor Author

I'm marking this as ready for review. There are still some TODOs left in the code, but most of them are meant as clarification questions where I didn't fully understand the ocaml implementation, but the behavior is the same as upstream

@VojtechStep

Copy link
Copy Markdown
Contributor Author

I also put in the effort to make the PR reviewable by commits. Most of the +418000 lines added are the test cases of course. There is one commit which copies them from the elpi repo, and another which normalizes them through the roundtrip of parsing and printing (the ocaml implementation has more heuristics for when to keep things on one line)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant