The Wayback Machine - https://web.archive.org/web/20210122045320/https://github.com/FStarLang/FStar/issues/1512
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

Flag to report unused functions/lemmas/lets. #1512

Open
wintersteiger opened this issue Aug 17, 2018 · 1 comment
Open

Flag to report unused functions/lemmas/lets. #1512

wintersteiger opened this issue Aug 17, 2018 · 1 comment

Comments

@wintersteiger
Copy link
Contributor

@wintersteiger wintersteiger commented Aug 17, 2018

It would be super useful if F* could report all unused functions/lemmas upon request. This is not totally trivial in the presence of SMTPats, interfaces, friends, etc, but for a start I think it would be enough to report unused symbols under the assumption that all relevant files are presented to F*.

@fournet @s-zanella @dranov

@wintersteiger wintersteiger changed the title Flag to report unused functions/lemmas. Flag to report unused functions/lemmas/lets. Aug 20, 2018
@fournet
Copy link
Contributor

@fournet fournet commented Aug 20, 2018

This is tricky, because this is a global-program property and we have multiple back-ends (including Z3 via patterns). Let's try to refine it into a clear ask.

@fournet fournet removed the easy label Aug 20, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment