X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=4200a4e95e66355376b9558871596ca24cb05dd7;hb=7bbce6bc163892cfd99cfcda65db42001b86789f;hp=aed2cf93cb3d53a8dba525006e092e54c145e03d;hpb=10ad9a25f7c1f59af054398f9c2c6eab43d003b9;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index aed2cf93c..4200a4e95 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -6,6 +6,8 @@ TODO 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 + - bug universi e tipi induttivi + - Set predicativo TATTICHE @@ -22,8 +24,6 @@ TODO in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply oltre che di bug! - Dare errore significativo al posto di NotWellTypedInterpreation -> CSC - - Bug nella generazione dei principi di eliminazione: - 1. generazione nomi (usa ref incrementata localmente) - elim_intros_simpl e rewrite_simpl: ora non viene usata dal ^^^^^^ ^^^^^^ toplevel la variante che semplifica. Capire quali sono i problemi @@ -46,48 +46,85 @@ TODO GUI GRAFICA - - bug di refresh del widget quando si avanza ("swap" tra la finestra dei - sequenti e la finestra dello script) + - integrare il famoso logo mancante (anche nell'About dialog) + - 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 + - finire e rendere piu' compliant (e.g. tags gestiti in maniera anomala) + il Cic Browser + - la barra di stato: c'e' ma non funziona? + + - menu contestuale (tasto dx) nel sequent viewer - feedback su hyperlink nei sequenti e nel browser: rendere visibili gli hyperlink (cursore a "manina"? hyperlink evidenziati?). La maction che collassa la prova e' fastidiosa: la prova si chiude se non si clicca correttamente su un hyperlink (anche tooltip sui bottoni) - - Implementare menu edit: cut/copy/undo/etc. - - invertibilita' dell'inserimento automatico di alias: quando si torna - su bisognerebbe tornare su di un passo e non fare undo degli alias - (Zack: nella history ci sono anche gli offset per sapere a che pezzo di - script uno stato appartiene) - - 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 - - quando si sposta il punto di esecuzione dello script cambiare la parte di - script visibile nella finestra dello script (finche' l'utente non lo - modifica lui, tipo agendo sulla scrollbar) - - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza - salvare. In verita' foo e' stato scritto lo stesso! + + - che farne della palette delle tattiche? - script outline -> Zack - - menu contestuale (tasto dx) nel sequent viewer -> attende notazione - - riattaccare hbugs (brrr...) -> Zack - - highlight degli errori di parsing nello script (usando lo sfondo come per la - parte lockata di testo, da ripulire quando si modifica il testo o si sposta - il punto di esecuzione) - - salvare la parte di testo lockata dagli effetti di undo/redo (come?????) - con ctrl-Z + - riattaccare hbugs (brrr...) -> Zack GUI LOGICA - - matitaclean all (o matitamake cleanall) dovrebbe radere al suolo la - directory .matita - - tornare indietro (verso il cursore) in matita dovrebbe essere O(1) e non un - Undo passo passo (sembra che il collo di bottiglia sia fare iterare su ogni - uri da togliere (accorpare almeno il lavoro sul db magari aiuta). - - freeze durante avanzamento + - in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e + eval_from_stream_greedy + - disambiguazione: attualmente io (CSC) ho committato la versione di + disambiguate.ml che NON ricorda gli alias in caso di disambiguazione + univoca (senza scelte per l'utente). [ cercare commento "Experimental" ] + Il problema di questa soluzione e' che rallenta in maniera significativa + l'esecuzione degli script. DOMANDA: quanto costano le fasi di + 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. + 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 + 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 + gli alias nello script viene un paciugo, credo! in particolare quando + vengono usate n istanze + - matitamake foo/a.ma non funziona; bisogna chiamarlo con + matitamake /x/y/z/foo/a.ma - notazione -> Luca e Zack - - gestione dei path per include: il path deve essere assoluto? da decidere ... - ( -I ?? o chiedere a matitamake la root e farci una find? ) - - copiare nel .moo la baseuri e poi il matitaclean la legge da li e non dal - .ma (si evita il syntax error) + - non chiudere transitivamente i moo ?? DONE +- invertibilita' dell'inserimento automatico di alias: quando si torna + su bisognerebbe tornare su di un passo e non fare undo degli alias + (Zack: nella history ci sono anche gli offset per sapere a che pezzo di + script uno stato appartiene) -> CSC +- bug di refresh del widget quando si avanza ("swap" tra la finestra dei + sequenti e la finestra dello script) -> CSC +- sensitiveness per goto begin/end/etc. (???) -> Gares +- cut&paste stile "X": rimane la parte blu e lockata! -> CSC +- highlight degli errori di parsing nello script -> CSC +- quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo + dalla finestra principale!!! -> CSC +- sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC +- fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza + salvare. In verita' foo e' stato scritto lo stesso! -> CSC +- matitaclean deve rimuovere anche i .moo; in alternativa il makefile + non deve basarsi sui .moo per decidere se qualcosa e' stato compilato o meno + -> CSC, Gares +- matitaclean all (o matitamake cleanall) dovrebbe radere al suolo la + directory .matita -> CSC, Gares +- icone standard per zoom-in/out/= e piu' aderenza alle Gnome Interface + Guidelines (e.g. about dialog) -> CSC +- salvare la parte di testo lockata dagli effetti di undo/redo con + (shift-)ctrl-Z e anche usando il menu che si apre con il tasto destro -> CSC +- fare in modo che il testo caricato inizialmente da matita non sia + undoable (usando i metodi begin/end_not_undoable_action di gtk_source_view) + -> Gares +- Implementare menu edit: cut/copy/undo/etc. -> CSC +- gestione dei path per include: il path deve essere assoluto? da decidere ... + ( -I ?? o chiedere a matitamake la root e farci una find? ) -> Gares +- freeze durante avanzamento -> Gares, CSC +- tornare indietro (verso il cursore) in matita dovrebbe essere O(1) e non un + Undo passo passo (sembra che il collo di bottiglia sia fare iterare su ogni + uri da togliere (accorpare almeno il lavoro sul db magari aiuta) -> Gares, CSC +- quando si sposta il punto di esecuzione dello script cambiare la parte di + script visibile nella finestra dello script -> Gares, CSC - find & replace -> Gares - Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo lockato! -> Gares @@ -96,6 +133,7 @@ DONE perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug stupido da qualche parte -> CSC - Bug vari nella generazione dei principi di eliminazione: + 1. generazione nomi (usa ref incrementata localmente) -> Andrea 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo passo il test inversion.ma) -> CSC, Gares 3. usato trucco outtype non dipendenti per il case -> CSC, Gares