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

Fixing the behavior of --dep with --extract #2389

Merged
merged 7 commits into from
Nov 11, 2021
Merged

Fixing the behavior of --dep with --extract #2389

merged 7 commits into from
Nov 11, 2021

Conversation

nikswamy
Copy link
Collaborator

@nikswamy nikswamy commented Nov 8, 2021

See issue #2385

From CHANGES.md:

  • Issue #2385.
    The behavior of the --extract option was changed so that it no
    longer treats the OCaml and Kremlin targets
    differently. Previously, when used with --dep full, F* would
    disregard the --extract setting when emitting the
    ALL_KRML_FILES variable.

From the new message associated with fstar --help:

  --extract One or more semicolon separated occurrences of '[TargetName:]ModuleSelector'
                Extract only those modules whose names or namespaces match the provided options.
                        'TargetName' ranges over {OCaml, Kremlin, FSharp, Plugin}.
                        A 'ModuleSelector' is a space or comma-separated list of '[+|-]( * | namespace | module)'.
                        For example --extract 'OCaml:A -A.B' --extract 'Kremlin:A -A.C' --extract '*' means
                                for OCaml, extract everything in the A namespace only except A.B;
                                for Kremlin, extract everything in the A namespace only except A.C;
                                for everything else, extract everything.
                        Note, the '+' is optional: --extract '+A' and --extract 'A' mean the same thing.
                        Note also that '--extract A' applies both to a module named 'A' and to any module in the 'A' namespace
                Multiple uses of this option accumulate, e.g., --extract A --extract B is interpreted as --extract 'A B'.

I also have patches to hacl-star, mitls-fstar and kremlin to accommodate this change.
With those patches, I have an everest green.

@nikswamy
Copy link
Collaborator Author

We discussed this extensively and I have open PRs in the other repos anticipating this change. Merging here followed by merges to the other everest repos.

@nikswamy nikswamy merged commit dff9662 into master Nov 11, 2021
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.

1 participant