FStarLang/FStar

Flag to report unused functions/lemmas/lets.

Open

#1,512 opened on Aug 17, 2018

View on GitHub
 (1 comment) (0 reactions) (0 assignees)F* (258 forks)auto 404
area/usabilitycomponent/dependency-analysisgood first issuekind/enhancementpriority/low

Repository metrics

Stars
 (3,068 stars)
PR merge metrics
 (PR metrics pending)

Description

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

Contributor guide

Research direction
Investigate how to detect unused symbols in F* while respecting SMTPats, interfaces, and friends. Look at existing termination checks or unused dependency detection mechanisms.
Tech stack
None
Domain
compilers
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Mostly clear
Prerequisites
F*compiler internals
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30