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

CLI: improve hax into -i '...' #497

Open
W95Psp opened this issue Feb 6, 2024 · 6 comments
Open

CLI: improve hax into -i '...' #497

W95Psp opened this issue Feb 6, 2024 · 6 comments
Labels
needs-design We need to write a proper design for this issue.

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Feb 6, 2024

Currently, that -i flag is redundant with F*'s --interfaces flag.

We should have a unified flag that can express a list of queries with modifiers.

A query selects some items, e.g. *some::module::*.

A modifiers say what to do with the selected items:

  • exclude them from the extraction;
  • include them and include all their dependencies as well;
  • include them without their dependencies;
  • include them but only their signature, not their bodies and without their dependencies;
  • include them but only their signature, not their bodies and with their dependencies (as signature only).

https://docs.google.com/document/d/1D_Cqa3JU_1ktm4LMZaLY6gowq2-2xdthhoQ3lPJT9_Q/edit?tab=t.s02xpni8jr0y

@W95Psp
Copy link
Collaborator Author

W95Psp commented May 14, 2024

Chatting with @karthikbhargavan about that, maybe more verbosity would be nicer:
instead of having one -i <something> flag with containing multiple items, we should have --include, --exclude, --include-only, --include-signature

@W95Psp
Copy link
Collaborator Author

W95Psp commented Aug 28, 2024

I'm inlining issue #688 there, as a possible enhancement: the selection query language could include selecting item based on visibility.

@W95Psp
Copy link
Collaborator Author

W95Psp commented Sep 16, 2024

Inlining another issue (#617): allow to reference anonymous paths

@W95Psp
Copy link
Collaborator Author

W95Psp commented Sep 16, 2024

The frontend should also warn if the user writes a selector that selects nothing. This was issue #466.

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 Nov 20, 2024
Copy link

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

@github-actions github-actions bot closed this as not planned Won't fix, can't repro, duplicate, stale Nov 27, 2024
@W95Psp W95Psp added needs-design We need to write a proper design for this issue. and removed stale labels Dec 16, 2024
@W95Psp W95Psp reopened this Dec 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
needs-design We need to write a proper design for this issue.
Projects
None yet
Development

No branches or pull requests

1 participant