CLI: improve `hax into -i '...'`

hacspec / hax

A Rust verification tool

https://hacspec.org/blog

Apache License 2.0

200 stars 21 forks source link

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

Closed W95Psp closed 17 hours ago

W95Psp commented 9 months ago

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).

W95Psp commented 6 months ago

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 commented 3 months ago

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

W95Psp commented 2 months ago

Inlining another issue (https://github.com/hacspec/hax/issues/617): allow to reference anonymous paths

W95Psp commented 2 months ago

The frontend should also warn if the user writes a selector that selects nothing. This was issue https://github.com/hacspec/hax/issues/466.

github-actions[bot] commented 1 week ago

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[bot] commented 17 hours ago

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.