Skip to content

Conversation

@Alizter
Copy link
Collaborator

@Alizter Alizter commented Apr 8, 2024

We have some better support for sharing flags in Dune 3.13 allowing us to reduce the size of the coq.theory stanzas.

@Alizter
Copy link
Collaborator Author

Alizter commented Apr 13, 2024

I'm going to hold off on this as there is a bug in 3.14 that makes compiling Coq slow. This is fixed in 3.15 but that was only recently released. I'll wait a little longer for this as it isn't critical so that 3.15 is more widespread.

Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: d0c60b0f-4aee-46ac-8e2d-3e5f52288b3c -->
@Alizter Alizter force-pushed the ps/rr/bump_to_dune_3_13 branch from 462a6f5 to 83f4cd5 Compare April 30, 2024 17:16
@Alizter
Copy link
Collaborator Author

Alizter commented Apr 30, 2024

The bug in Dune has been fixed and the fix is available in 3.15.2. See #1924 for a more detailed explanation of the issue.

@Alizter Alizter marked this pull request as ready for review April 30, 2024 17:27
@jdchristensen
Copy link
Collaborator

LGTM

@Alizter Alizter merged commit c143d87 into HoTT:master Apr 30, 2024
@Alizter Alizter deleted the ps/rr/bump_to_dune_3_13 branch April 30, 2024 17:30
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.

3 participants