Daily report (2026-09-15)

1. Summary

Today work has focused on two things; Progressing on the implementation of the ctest extension stuff, and enabling some smarter Idris diagnostics in my editor.

Thus far, the plan as outlined yesterday continues to be mostly the same, in terms of the ctest module resolution work. The only notable change is that I believe I will not need ancilliary algorithms.

As explained yesterday, I had settled on first determining whether I was handling a glob reexport or a regular reexport. This I think is unnecessary after today’s work on the second core algorithm.

The algorithm I’ve sticked with directly parses the reexport, and returns a list of FfiItems with it. The list corresponds to potentially multiple items that are being introduced from the same use statement.

The item resolution work has been thought about as commented on yesterday’s report. The one thing I have yet to finish working on is the list unification algorithm between items in a grouped import statement.

Each element of the group branches out into an individual run of the second core algorithm. Once its recursion bottoms out, it yields back the list of items introduced by that element. That needs joining with other elements in the group.

In terms of side-project work, today I have been working on implementing better editor integration for Idris diagnostics. Type-checking standalone files provides great insights, but is not supported by upstream.

So I have instead started working on some better typechecking support in my editor by hooking into the diagnostics API of the editor’s buffers. This has thus far not been challenging, though diagnostic parsing is quite wonky.

The Idris compiler does not seem to support structured diagnostics, so I have to manually match string patterns. But beyond that, I have been successful in setting up temporary files and buffers in the editor to display diagnostics.

All through this, I also worked in some other editor integration stuff I had pending from a while ago. This is mostly concerned with setting up a custom pipeline for formatting editor buffers without blocking too much.

2. Blockers

None. Today I had to deal with some stuff in the evening, so there was less time than usual to work on stuff.

3. Plan for the week

I expect the ctest work to continue tomorrow. I think I will likely finish up the second core algorithm by tomorrow. Then I can go back to the first one, and see about “merging” FfiItems instances.

In terms of side-project work, I do not consider my current endeavors to represent side-tracked activities. This means I will likely only take one more day to finish things up, and otherwise go back to the Idris crash course.