Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(engine): item ordering #1140

Merged
merged 3 commits into from
Nov 27, 2024
Merged

fix(engine): item ordering #1140

merged 3 commits into from
Nov 27, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Nov 26, 2024

This PR fixes #771: now the items are sorted topologically but kept in definition order if equal topologically speaking.

Technically this PR:

  • kills the original_items parameter in dependencies.ml functions
  • introduce a functor WithItems instead, that takes a list of items
  • add a module Ordered_concrete_ident that defines a comparison operator sensible to the list of items taken by WithItems
  • apply the functor automatically to provide the same interface as we had before

@W95Psp W95Psp marked this pull request as draft November 26, 2024 13:44
@W95Psp W95Psp requested a review from maximebuyse November 26, 2024 13:55
@W95Psp W95Psp marked this pull request as ready for review November 26, 2024 13:55
@W95Psp W95Psp force-pushed the fix-item-order-771 branch from 45c4a7e to 40ba45e Compare November 27, 2024 07:52
Copy link
Contributor

@maximebuyse maximebuyse left a comment

Choose a reason for hiding this comment

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

Great 🎉

@maximebuyse maximebuyse added this pull request to the merge queue Nov 27, 2024
Merged via the queue into main with commit 7bb4c28 Nov 27, 2024
15 checks passed
@maximebuyse maximebuyse deleted the fix-item-order-771 branch November 27, 2024 08:42
@karthikbhargavan karthikbhargavan restored the fix-item-order-771 branch November 27, 2024 16:57
@maximebuyse
Copy link
Contributor

Following the discussion in #1151 (comment). I think the approach in here is better for now. I'll test if this breaks anything.

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.

Engine: dependencies: the sorting seems unstable
2 participants