Skip to content

Conversation

@nomeata
Copy link

@nomeata nomeata commented Nov 12, 2025

This pass lifts type aliases out of recursive groups. There is only one such alias (resulttype), but who knows what comes up later.

It fails ungracefully (relying on the il validator) if the aliases are themselves recursive.

This simplifies generation of Rocq or Lean.

@nomeata nomeata requested a review from DCupello1 November 12, 2025 08:55
@nomeata
Copy link
Author

nomeata commented Nov 12, 2025

Hmm, CI on github fails with

Fatal error: exception Stack overflow

but it works fine locally here.

Copy link

@DCupello1 DCupello1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

About the stack overflow, I have the same issue when trying to merge the uncase removal pass to main #191 .

@rossberg: these two passes do completely different things, so its very likely to be a CI issue. What can we do about this?

@rossberg
Copy link
Collaborator

Did you try a make clean before running the tests locally? If yes, then I don't know what the cause is or what we can do about it. Perhaps the CI environment is configured to use smaller stack space by default?

@nomeata
Copy link
Author

nomeata commented Nov 12, 2025

It might be that mdx_gen.bc.exe itself is stack overflowing, given the huge TEST.md file. That’s consistent with Diegos PR also failing as he adds yet another pass.

So maybe #194 (which I’d advocate for nevertheless) will just avoid this problem, but not using mdx and using pure dune for running tests.

@nomeata nomeata marked this pull request as draft November 12, 2025 14:52
@nomeata
Copy link
Author

nomeata commented Nov 12, 2025

Indeed #194 helps

@DCupello1
Copy link

Great! I'll do the same with #191

@nomeata nomeata marked this pull request as ready for review November 13, 2025 09:11
@nomeata nomeata merged commit 25cee09 into main Nov 13, 2025
18 checks passed
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.

4 participants