Partial support for mutual inductives in derive

[Janno]

This is currently just a naive rebase on top of master. AFAICT (and that's not very far) the current status is this:

• all derive passes support un-indexed mutual inductive types
• all passes that could meaningfully support indexed mutual inductive types do so, except for eq, invert, idx2inv.

I think one big problem with the current files is the testing strategy. My idea to record the expected terms in functors is less than ideal. I think for most passes we simply care that the derivation succeeds and that the term printed (without implicits) looks reasonable. This sounds like a perfect use case for the new output tests. So I suggest we wait until #1033 lands so that we get to use those. That should cut down the noise by a huge factor.

The other potential problem is that there might be a lot of opportunity for refactoring, code sharing, etc, that I won't be able to spot on my own. I think the LLM already did refactor a few passes so that the non-mutual case is simply a special case of the more general code path for mutual inductives but I am not sure it did that everywhere.

[Janno]

I have rebased, squashed, and then re-exploded the changes into one commit for shared helpers, one commit for tests the LLM thought were still missing from param1, and then one commit per derive pass.

[gares]

Nice.

[Janno]

I see that there are unexpected conflicts. I think I have not based these changes on the correct branch. I'll rebase on master.

[Janno]

Rebased. The conflicts were resolved by the LLM using param1 as the guideline. AFAICT the conflict resolution mostly removed code that went against your preferred way of structuring the derivations.

[gares]

Many thanks!

How much work can I ask you to put on the LLM? We are converging, but there is still some slop.
Eg:

• mutual_lib can go to coq-lib.elpi, in a namespace mutual (no derive prefix) so to remove the accumulation of that file everywhere
• param1_mutual_lib can go into paramX_lib.elpi
• the tree/forest data type and similar that the LLM uses in his additional tests should go to test_derive_corelib.v
• the huge apps/derive/tests/test_derive_mutual.v fails to compile in CI. I can live with a mega file to track regressions, but it has to compile in the first place

[Janno]

How much work can I ask you to put on the LLM? We are converging, but there is still some slop.

As much as it takes for the changes to be of good (enough) quality.

the huge apps/derive/tests/test_derive_mutual.v fails to compile in CI. I can live with a mega file to track regressions, but it has to compile in the first place

It also fails locally and it seems to be because of an "optimization" that had been introduced by the LLM but not longer exists: maps for types without parameters would return an identity function and that was recorded in the tests. I don't know if this is ever useful. I can fix the test or ask the LLM to reinstate the change.

[gares]

Oh I see I removed that. If it is only an optimization in case one executes the code, I think it can go. If it helps with dependent types because of the extra computation, eg (map_nat x = x), ask the LLM to put it back.

[Janno]

Oh I see I removed that. If it is only an optimization in case one executes the code, I think it can go. If it helps with dependent types because of the extra computation, eg (map_nat x = x), ask the LLM to put it back.

Neither me nor the LLM can say anything useful about the use of the optimization, I think. All I know is that I think it's a little weird to ask for maps on types without parameters and I am not sure what the expected answer is suppose to be. This is probably something to be addressed in another issue/PR once there are actual use cases for the optimization.

The tests now document the expected terms (with fixpoints) and I had the LLM work on the remaining comments. I forgot to do individual commits for each one. Let me know if that's a problem.

[gares]

please work on #1091