feat: Add hypothesis filtering mechanism to only show Prop hypotheses

[KacperFKorban]

This PR implements a new feature: filtering the displayed hypotheses so that only the Prop-kinded ones are displayed.

Kooha-2026-03-31-11-04-05.webm

[gares]

Thanks! I think the feature is useful, but I wonder if a completely different approach would be feasible. We already plan to put more info in the goal, like unique names to sub terms so to be able to track back where the user clicked.

Adding a boolean (the universe) to each hypothesis seems simpler, and the filtering could then be done client side. What do you think?

I do like the possibility to replay an event with different options, I do have use cases for the exec event (think at verbose/debug), so the current approach is also acceptable, I'm just exploring alternatives. Maybe I would be more convinced if we could ask to disable a notation (and hence be obliged to re print server side) but we currently lack the notation id in the printed term.

Cc @rtetley since we discussed that before

[KacperFKorban]

Thanks for the answer!
I'm not really set on any particular approach. As with anything, it's a trade-off. Adding the universe information to every hypothesis gives more flexibility, but might be slightly slower, since we have to compute the universe even if the user isn't using that information. I'm happy to change the implementation.

[shilangyu]

I really like this feature and would like to use it day to day. Though I also feel it would be better to just augment the data being sent to the client instead of pushing that config option to the server code.

we have to compute the universe even if the user isn't using that information

Do we know if this is an expensive operation?

[KacperFKorban]

I implemented the approach that you suggested. The filtering is done on the client side now.
Here are the updated screenshots:

I added a bit more structure to the hypotheses type: instead of one pp_string, there is now a record with a name, content, type, universe(string).
As a bonus I changed the color of the name to be different for hypotheses in different universes. I also added a small backwards-compatibility layer to make the new client work with older language server versions.

The CI failure seems unrelated.

[gares]

Why this one?

[gares]

can you add some comment here?
I see the hyps are compacted to display x, y : nat but then I don't get why this extra fiddling.

[KacperFKorban]

Will do, this is basically an attempt to add the universes and ids info to the pre-rendered hypotheses that we get from the Proof_diffs.

[gares]

The current:bool seems a bit fragile to me, is it really necessary? The selected editor tab does not necessarily match the goal window, does it? Can't you just refresh them all?

I kind of understand moving from manual to continuous mode may be a bit violent if you do that in all tabs.

anyway, this change seems orthogonal to the hyp filtering, unless I'm missing something.

[gares]

I'm not really competent about the client code, the only weird thing to me is that the filter is hardwired.

Why can't it be a regex on the sort or the type? (with Prop|SProp the default). I mean a sort of checkbox next to the search widget you get with ^f:

• filter hyps
  I can see use cases where the context is huge and you want to only see hyps about a predicate.
  In this optic, the color change is a bit weird, you already get it with ^f.

I also think a little message like some hyps are hidden would be kind, since one may forget he has a filter on (unless the search widget never disappears), and it is not always the case that stuff in type occurs in stuff in prop, hence you may not see a hidden variable elsewhere.

[gares]

To be clear, I'm in favor of this change, it just seems to be a bit too ad hoc

[KacperFKorban]

The current:bool seems a bit fragile to me, is it really necessary? The selected editor tab does not necessarily match the goal window, does it? Can't you just refresh them all?

I kind of understand moving from manual to continuous mode may be a bit violent if you do that in all tabs.

anyway, this change seems orthogonal to the hyp filtering, unless I'm missing something.

Yes, sorry. That was part of the server-side filtering that I implemented before. I forgot to remove that part of the code by accident. It's not needed for this feature.