X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=d71a5f510dce1deedd0684eaec42708509013c20;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=3d3fb2702bf73af58dd27e714f6bda0c3b5ccd53;hpb=750b872516df21ab4232001648a3d8ce7de13360;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 3d3fb2702..d71a5f510 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -1,25 +1,24 @@ TODO NUCLEO - - CRITICO: quando l'environment non e' trusted non compila la library di - matita!!! - PREOCCUPANTE: per inductive i : Prop := K : True (*-> i*) -> i. noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON genera i_rec e i_rect quando c'e' un argomento ricorsivo. (CSC: manca vincolo aggiuntivo non dipendente dalla sorta per il caso in - questione) -> CSC + questione) -> Gares - bug universi e tipi induttivi - Set predicativo TATTICHE - - simplify (e altre tattiche) non debbono zeta-espandere i let-in - - tattica unfold su rel a let-in bound variables - - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con + - verificare il comportamento di tutte le tattiche con il parsing lazy -> CSC + - file elim.ma: vengono creati lambda dummy e referenziati nell'outtype di + un case + - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire + - comportamento di tutte le tattiche nei confronti dei let-in + - elim con pattern + - theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con True. - - parsing contestuale (tattiche replace, change e forse altre) - capire dove fare la select per avere i contesti in cui disambiguare gli - altri argomenti. - assiomi (manca sintassi concreta e AST). - Guardare il commento (*CSC: this code is suspect and/or bugged: we try first without reduction @@ -50,8 +49,6 @@ TODO GUI GRAFICA - - Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra - con la notazione alla Coq V7.0 che non riesce piu' a riparsare! - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare @@ -75,12 +72,14 @@ TODO - riattaccare hbugs (brrr...) -> Zack GUI LOGICA + - nuovo pretty-printer testuale: non stampa usando la notazione + (e.g. guardare output di matitac) + - matitaclean (e famiglia) non cancellano le directory vuote + (e per giunta il cicbrowser le mostra :-) - codice di inizializzazione di matita, matitac, matitatop replicato e non in sync - fattorizzare codice fra MatitaEngine e DisambiguatePp (dove, fra l'altro, ora io (=CSC) ho messo anche un parser!!!) - - integrare nuova contrib ferruccio nel bench notturno; guardare bug - generazione principi di eliminazione - bug "Warn: baseuri cic:/matita/higher_order_defs/ordering is not empty" mentre si compila Z/times.ma. Il bug sembra essere transiente. - in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e @@ -93,10 +92,14 @@ TODO fetch/decode/execute delle linee dello script? Una possibile alternativa e' avere alias "soft": se la disambiguazione fallisce gli alias soft vengono ripuliti e si riprova. + Altra soluzione (Gares): avere alias multipli e provare tutti gli alias + multipli. Da combinare con il "ritenta con istanze multiple in caso di + fallimento". SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias implicito; 2. gli alias vengono ricordati come nella soluzione originale (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono - dimenticati (quali? tutti?) e si ritenta; se fallisce ancora si generano + dimenticati (quali? tutti? tutti tranne quelli chiesti all'utente?) + e si ritenta; se fallisce ancora si generano istanze differenti e si ritenta; 4. ritentare anche senza e poi con coercions? oppure ordinare preferendo la soluzione che non ha introdotto coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono @@ -108,10 +111,35 @@ TODO - non chiudere transitivamente i moo ?? DEMONI E ALTRO - - implementare inclusione file di configurazione (perche' ora tutti - i demoni scopiazzano venti righe per via del getter embedded :-( DONE +- parsing contestuale (tattiche replace, change e forse altre) + capire dove fare la select per avere i contesti in cui disambiguare gli + altri argomenti. -> Zack, Enrico, CSC +- tattica unfold su rel a let-in bound variables: c'e' ancora un bug + aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto + del goal e non in quello del pattern. Pertanto invece di cercare di + fare unfolding di x viene fatto unfolding di altro. + Soluzione: la funzione ProofEngineHelpers.select deve tornare una + funzione per rilocare i termini nel contesto giusto. + Esempio: + theorem t: let uno \def S O in uno + uno = S uno \to uno=uno. + intros. unfold uno in H. + NOTA: questo bug e' legato a quello di parsing in presenza di tattiche + con pattern, visto che in tal caso e' l'intero parsing a dover essere + fatto in un contesto differente. Risolvendo quel bug si risolve + automaticamente anche questo. + -> Zack, Enrico, CSC +- Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra + con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack +- implementare inclusione file di configurazione (perche' ora tutti + i demoni scopiazzano venti righe per via del getter embedded :-( -> Zack +- simplify non debbono zeta-espandere i let-in -> CSC, Gares +- integrare nuova contrib ferruccio nel bench notturno e rilocarla in + contribs o qualcosa del genere -> CSC +- CRITICO: quando l'environment non e' trusted non compila la library di + matita!!! -> Gares, CSC +- bug di unsharing -> CSC - CRITICO (trovato anche da Ferruccio): typechecking di cic:/Coq/ring/Quote/index_eq_prop.con asserzione del nucleo (applicazione senza argomenti). -> CSC