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.

Sign up for GitHub

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

Jump to bottom

Engine: dependencies: the sorting seems unstable #771

Open
W95Psp opened this issue Jul 15, 2024 · 3 comments · Fixed by #1140 · May be fixed by #1151
Open

Engine: dependencies: the sorting seems unstable #771

W95Psp opened this issue Jul 15, 2024 · 3 comments · Fixed by #1140 · May be fixed by #1151
Labels
bug Something isn't working engine Issue in the engine keep-open

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Jul 15, 2024

See https://github.com/cryspen/libcrux/blob/ml-kem-lax-check/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst

In this module, functions are in big part independent, but still, they get reordered.
@W95Psp W95Psp added bug Something isn't working engine Issue in the engine labels Jul 15, 2024
@W95Psp
Copy link
Collaborator Author

W95Psp commented Jul 24, 2024

After investigations, it seems like we are sorting the items alphabetically at some point...
See this example.

@github-actions GitHub Actions
Copy link

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

@github-actions github-actions bot added the stale label Sep 23, 2024
@W95Psp W95Psp added keep-open and removed stale labels Sep 23, 2024
W95Psp added a commit that referenced this issue Nov 26, 2024
@W95Psp
fix(engine/dependencies): item order (fixes #771)
ecd4947
@W95Psp W95Psp mentioned this issue Nov 26, 2024
Merged
W95Psp added a commit that referenced this issue Nov 27, 2024
@W95Psp
fix(engine/dependencies): item order (fixes #771)
6235c03
@W95Psp
Copy link
Collaborator Author

W95Psp commented Nov 28, 2024

Re-opening, after testing on libcrux, we got reordering issues. We're investigating.

@W95Psp W95Psp reopened this Nov 28, 2024
@franziskuskiefer franziskuskiefer linked a pull request Nov 28, 2024 that will close this issue
fix(engine/deps): preserve definitions order whenever possible #1151
Draft
@karthikbhargavan karthikbhargavan linked a pull request Dec 3, 2024 that will close this issue
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working engine Issue in the engine keep-open
Projects
None yet
Milestone
No milestone
1 participant
@W95Psp