FStarLang/FStar

Flag to report unused functions/lemmas/lets.

Open

#1512 aperta il 17 ago 2018

Vedi su GitHub
 (1 commento) (0 reazioni) (0 assegnatari)F* (258 fork)auto 404
area/usabilitycomponent/dependency-analysisgood first issuekind/enhancementpriority/low

Metriche repository

Star
 (3068 star)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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

Guida contributor

Direzione di ricerca
Indaga come rilevare i simboli inutilizzati in F* rispettando SMTPat, interfacce e amici. Esamina i controlli di terminazione esistenti o i meccanismi di rilevamento delle dipendenze non utilizzate.
Tech stack
Nessuno
Dominio
compilers
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Abbastanza chiara
Prerequisiti
F*compiler internals
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30