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.

Sign up for GitHub

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

Jump to bottom

F* cli: --interface: add an option to extract only an fsti without a fst #465

Closed
W95Psp opened this issue Jan 29, 2024 · 0 comments · Fixed by #470
Closed

F* cli: --interface: add an option to extract only an fsti without a fst #465

W95Psp opened this issue Jan 29, 2024 · 0 comments · Fixed by #470
Assignees
@W95Psp
Labels
cli Related to command line engine Issue in the engine f* F* backend

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Jan 29, 2024 •
edited
Loading

When something of the shape +!Foo is passed to --interfaces, only a Foo.fsti should be extracted (ignoring the Foo.fst)
@W95Psp W95Psp added engine Issue in the engine cli Related to command line f* F* backend labels Jan 29, 2024
@W95Psp W95Psp self-assigned this Jan 29, 2024
@W95Psp W95Psp mentioned this issue Jan 29, 2024
Closed
W95Psp added a commit that referenced this issue Jan 29, 2024
@W95Psp
feat(engine/fstar): --interfaces: extract only fsti
3f22e37 
Fix #397
Fix #465
@W95Psp W95Psp mentioned this issue Jan 29, 2024
Merged
W95Psp added a commit that referenced this issue Jan 29, 2024
@W95Psp
feat(engine/fstar): --interfaces: add option to extract only fsti
afa9bd5 
Fix #397
Fix #465
W95Psp added a commit that referenced this issue Jan 29, 2024
@W95Psp
feat(engine/fstar): --interfaces: add option to extract only fsti
fd4c50a 
Fix #397
Fix #465
W95Psp added a commit that referenced this issue Jan 30, 2024
@W95Psp
feat(engine/fstar): --interfaces: add option to extract only fsti
5d24f44 
Fix #397
Fix #465
W95Psp added a commit that referenced this issue Jan 30, 2024
@W95Psp
feat(engine/fstar): --interfaces: add option to extract only fsti
60f10d1 
Fix #397
Fix #465
@github-project-automation github-project-automation bot moved this to Done in hax Jan 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@W95Psp W95Psp

Labels
cli Related to command line engine Issue in the engine f* F* backend
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat(engine/fstar): --interfaces: add option to extract only fsti cryspen/hax
1 participant
@W95Psp