Skip to content

coqPackages_8_20: fix sort instability - #418946

Closed
trofi wants to merge 1 commit into
NixOS:masterfrom
trofi:coqPackages_8_20-fix-sort-stability
Closed

coqPackages_8_20: fix sort instability#418946
trofi wants to merge 1 commit into
NixOS:masterfrom
trofi:coqPackages_8_20-fix-sort-stability

Conversation

@trofi

@trofi trofi commented Jun 22, 2025

Copy link
Copy Markdown
Contributor

Without the change builtins.sort is not guaranteed to produce stable results across nix implementations or even std::sort implementations.

With a small patch from NixOS/nix#12106 (comment) nix shows predicate instability as:

$ nix eval --impure --expr 'with import ./. {};  coqPackages_8_20' --show-trace
error:
   … while evaluating the attribute 'coqPackages_8_20'
...
   … while calling the 'sort' builtin
     at pkgs/development/coq-modules/metacoq/default.nix:13:48:
       12|   owner = "MetaCoq";
       13|   defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
         |                                                ^
       14|     lib.mapAttrsToList (out: case: { inherit case out; }) {

   error: !(a < a) assert failed

The fix is to use strict < comparison rather than non-strict <= one.

Things done

  • Built on platform(s)
    • x86_64-linux
    • aarch64-linux
    • x86_64-darwin
    • aarch64-darwin
  • For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
    • sandbox = relaxed
    • sandbox = true
  • Tested, as applicable:
  • Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
  • Tested basic functionality of all binary files (usually in ./result/bin/)
  • Nixpkgs 25.11 Release Notes (or backporting 24.11 and 25.05 Nixpkgs Release notes)
    • (Package updates) Added a release notes entry if the change is major or breaking
  • NixOS 25.11 Release Notes (or backporting 24.11 and 25.05 NixOS Release notes)
    • (Module updates) Added a release notes entry if the change is significant
    • (Module addition) Added a release notes entry if adding a new NixOS module
  • Fits CONTRIBUTING.md, pkgs/README.md, maintainers/README.md and other contributing documentation in corresponding paths.

Add a 👍 reaction to pull requests you find important.

Without the change `builtins.sort` is not guaranteed to produce stable
results across `nix` implementations or even `std::sort` implementations.

With a small patch from NixOS/nix#12106 (comment)
`nix` shows predicate instability as:

    $ nix eval --impure --expr 'with import ./. {};  coqPackages_8_20' --show-trace
    error:
       … while evaluating the attribute 'coqPackages_8_20'
    ...
       … while calling the 'sort' builtin
         at pkgs/development/coq-modules/metacoq/default.nix:13:48:
           12|   owner = "MetaCoq";
           13|   defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
             |                                                ^
           14|     lib.mapAttrsToList (out: case: { inherit case out; }) {

       error: !(a < a) assert failed

The fix is to use strict `<` comparison rather than non-strict `<=` one.
@trofi trofi mentioned this pull request Jun 22, 2025
13 tasks
@github-actions github-actions Bot added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin. 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux. 6.topic: coq A formal proof management system labels Jun 22, 2025
@proux01

proux01 commented Jun 22, 2025

Copy link
Copy Markdown
Contributor

The issue is rather theoretical since comparison keys come from an attrset, hence are all distinct, but why not.

@nixpkgs-ci nixpkgs-ci Bot added the 2.status: merge conflict This PR has merge conflicts with the target branch label Jul 1, 2025
@trofi trofi closed this Jul 2, 2025
@trofi
trofi deleted the coqPackages_8_20-fix-sort-stability branch July 2, 2025 06:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

2.status: merge conflict This PR has merge conflicts with the target branch 6.topic: coq A formal proof management system 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin. 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants