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

Disable recursive priorities #1600

Merged
merged 1 commit into from
Sep 13, 2023
Merged

Disable recursive priorities #1600

merged 1 commit into from
Sep 13, 2023

Commits on Sep 13, 2023

  1. Remove recursive priorities

    Recursive priorites were added pre-RFC005, where their semantics was
    straightforward. Because metadata could appear anywhere, recursive
    priorities (or also called push priorities) just amounted to have a
    primop that pushed the priorities down a term, in one lazy step.
    
    Since RFC005, this isn't possible anymore, because only record field can
    hold metadata. It's now much more intricate to implement, because when
    encountering a `rec force` at the field level, we first need to know if
    there's any value able to receive it underneath this field to know if we
    should attach it to the field or no. To know that, we might need to
    evaluate the field first, and then decide.
    
    Before sorting out both the new semantics and implementation, this
    commit disable the syntax (but keep the rest of the machinery) from
    1.2.0 so that we can do some design before shipping new recursive
    priorities or scraping them entirely. Recursive priorities were
    undocumented, and should have been disabled from 1.0.0, so it's not
    considered a breaking change.
    yannham committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    e3c78c6 View commit details
    Browse the repository at this point in the history