4 inductive i : Prop := K : True (*-> i*) -> i.
5 noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON
6 genera i_rec e i_rect quando c'e' un argomento ricorsivo.
7 (CSC: manca vincolo aggiuntivo non dipendente dalla sorta per il caso in
9 - bug universi e tipi induttivi
14 - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire
15 - comportamento di tutte le tattiche nei confronti dei let-in
16 - tattica unfold su rel a let-in bound variables: c'e' ancora un bug
17 aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto
18 del goal e non in quello del pattern. Pertanto invece di cercare di
19 fare unfolding di x viene fatto unfolding di altro.
20 Soluzione: la funzione ProofEngineHelpers.select deve tornare una
21 funzione per rilocare i termini nel contesto giusto.
23 theorem t: let uno \def S O in uno + uno = S uno \to uno=uno.
24 intros. unfold uno in H.
25 NOTA: questo bug e' legato a quello di parsing in presenza di tattiche
26 con pattern, visto che in tal caso e' l'intero parsing a dover essere
27 fatto in un contesto differente. Risolvendo quel bug si risolve
28 automaticamente anche questo.
30 - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
32 - parsing contestuale (tattiche replace, change e forse altre)
33 capire dove fare la select per avere i contesti in cui disambiguare gli
35 - assiomi (manca sintassi concreta e AST).
36 - Guardare il commento
37 (*CSC: this code is suspect and/or bugged: we try first without reduction
38 and then using whd. However, the saturate_term always tries with full
39 reduction without delta. *)
40 in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply
42 - Dare errore significativo al posto di NotWellTypedInterpreation -> CSC
43 - elim_intros_simpl e rewrite_simpl: ora non viene usata dal
45 toplevel la variante che semplifica. Capire quali sono i problemi
46 e/o cosa fare delle varianti con semplificazione.
47 (con sintassi concreta alla \section*, analogamente cut e similia che fanno
49 - eta_expand non usata da nessuno? (ask Andrea?)
50 - eliminare eta_fix? (aspettare notazione) (correlato con sopra?)
51 - bug di ferruccio: fare un refresh dei nomi dopo l'applicazione
52 di una tattica. Di quali nomi fare refresh? (Andrea) di quelli
53 veramente ambigui, ovvero dell'ultimo binder tale che sotto di
54 esso un nome viene usato in maniera ambigua. Esempio:
55 \lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh
56 \lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh
57 Capita quando un tipo dall'environment (e.g. \lambda x.T)
58 viene inserito in un contesto (e.g. x:nat) dove le variabili
59 sono gia' state legate in precedenza.
60 - supportare l'apertura di piu' script contemporaneamente in tab/finestre
65 - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
66 finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
67 codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
68 - la finestrella per i development ha i pulsanti non sensitive.
69 E' possibile fare "Build" senza selezionare nulla, ottenendo un
71 - l'entry "Save" da menu non e' context sensitive (ti fa salvare anche
72 quando il file non e' stato modificato)
73 - finire e rendere piu' compliant (e.g. tags gestiti in maniera anomala)
75 - la barra di stato: c'e' ma non funziona?
77 - menu contestuale (tasto dx) nel sequent viewer
78 - feedback su hyperlink nei sequenti e nel browser: rendere visibili gli
79 hyperlink (cursore a "manina"? hyperlink evidenziati?). La maction che
80 collassa la prova e' fastidiosa: la prova si chiude se non si clicca
81 correttamente su un hyperlink (anche tooltip sui bottoni)
83 - che farne della palette delle tattiche?
84 - script outline -> Zack
85 - riattaccare hbugs (brrr...) -> Zack
88 - nuovo pretty-printer testuale: non stampa usando la notazione
89 (e.g. guardare output di matitac)
90 - matitaclean (e famiglia) non cancellano le directory vuote
91 (e per giunta il cicbrowser le mostra :-)
92 - codice di inizializzazione di matita, matitac, matitatop replicato e non
94 - fattorizzare codice fra MatitaEngine e DisambiguatePp (dove, fra l'altro,
95 ora io (=CSC) ho messo anche un parser!!!)
96 - bug "Warn: baseuri cic:/matita/higher_order_defs/ordering is not empty"
97 mentre si compila Z/times.ma. Il bug sembra essere transiente.
98 - in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e
99 eval_from_stream_greedy
100 - disambiguazione: attualmente io (CSC) ho committato la versione di
101 disambiguate.ml che NON ricorda gli alias in caso di disambiguazione
102 univoca (senza scelte per l'utente). [ cercare commento "Experimental" ]
103 Il problema di questa soluzione e' che rallenta in maniera significativa
104 l'esecuzione degli script. DOMANDA: quanto costano le fasi di
105 fetch/decode/execute delle linee dello script?
106 Una possibile alternativa e' avere alias "soft": se la disambiguazione
107 fallisce gli alias soft vengono ripuliti e si riprova.
108 Altra soluzione (Gares): avere alias multipli e provare tutti gli alias
109 multipli. Da combinare con il "ritenta con istanze multiple in caso di
111 SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias
112 implicito; 2. gli alias vengono ricordati come nella soluzione originale
113 (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono
114 dimenticati (quali? tutti? tutti tranne quelli chiesti all'utente?)
115 e si ritenta; se fallisce ancora si generano
116 istanze differenti e si ritenta; 4. ritentare anche senza e poi con
117 coercions? oppure ordinare preferendo la soluzione che non ha introdotto
118 coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono
119 gli alias nello script viene un paciugo, credo! in particolare quando
120 vengono usate n istanze
121 - matitamake foo/a.ma non funziona; bisogna chiamarlo con
122 matitamake /x/y/z/foo/a.ma
123 - notazione -> Luca e Zack
124 - non chiudere transitivamente i moo ??
129 - Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra
130 con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack
131 - implementare inclusione file di configurazione (perche' ora tutti
132 i demoni scopiazzano venti righe per via del getter embedded :-( -> Zack
133 - simplify non debbono zeta-espandere i let-in -> CSC, Gares
134 - integrare nuova contrib ferruccio nel bench notturno e rilocarla in
135 contribs o qualcosa del genere -> CSC
136 - CRITICO: quando l'environment non e' trusted non compila la library di
137 matita!!! -> Gares, CSC
138 - bug di unsharing -> CSC
139 - CRITICO (trovato anche da Ferruccio): typechecking di
140 cic:/Coq/ring/Quote/index_eq_prop.con
141 asserzione del nucleo (applicazione senza argomenti). -> CSC
142 - verificare se tutte le query sono ora ottimizzate (usando il comando
143 explain) e usano gli indici in maniera ottimale; inoltre migliorare gli
144 indici sulle tabelle hits and count -> CSC
145 - ???????????? Perche'?
146 mowgli:~# du -s /var/lib/mysql/mowgli/
147 250696 /var/lib/mysql/mowgli/
148 mowgli:~# du -s /var/lib/mysql/matita/
149 455096 /var/lib/mysql/matita/ -> CSC
150 - library/nat/primes.ma: ex_prime ci mette un secolo il db (binding) a fare
151 la Mysql.exec che ritorna una lista vuota di risultati. Investigare.
152 Anche peggio in library/nat/minimization/f_max_true. -> CSC
153 - integrare il famoso logo mancante (anche nell'About dialog) -> CSC
154 - invertibilita' dell'inserimento automatico di alias: quando si torna
155 su bisognerebbe tornare su di un passo e non fare undo degli alias
156 (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
157 script uno stato appartiene) -> CSC
158 - bug di refresh del widget quando si avanza ("swap" tra la finestra dei
159 sequenti e la finestra dello script) -> CSC
160 - sensitiveness per goto begin/end/etc. (???) -> Gares
161 - cut&paste stile "X": rimane la parte blu e lockata! -> CSC
162 - highlight degli errori di parsing nello script -> CSC
163 - quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo
164 dalla finestra principale!!! -> CSC
165 - sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC
166 - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza
167 salvare. In verita' foo e' stato scritto lo stesso! -> CSC
168 - matitaclean deve rimuovere anche i .moo; in alternativa il makefile
169 non deve basarsi sui .moo per decidere se qualcosa e' stato compilato o meno
171 - matitaclean all (o matitamake cleanall) dovrebbe radere al suolo la
172 directory .matita -> CSC, Gares
173 - icone standard per zoom-in/out/= e piu' aderenza alle Gnome Interface
174 Guidelines (e.g. about dialog) -> CSC
175 - salvare la parte di testo lockata dagli effetti di undo/redo con
176 (shift-)ctrl-Z e anche usando il menu che si apre con il tasto destro -> CSC
177 - fare in modo che il testo caricato inizialmente da matita non sia
178 undoable (usando i metodi begin/end_not_undoable_action di gtk_source_view)
180 - Implementare menu edit: cut/copy/undo/etc. -> CSC
181 - gestione dei path per include: il path deve essere assoluto? da decidere ...
182 ( -I ?? o chiedere a matitamake la root e farci una find? ) -> Gares
183 - freeze durante avanzamento -> Gares, CSC
184 - tornare indietro (verso il cursore) in matita dovrebbe essere O(1) e non un
185 Undo passo passo (sembra che il collo di bottiglia sia fare iterare su ogni
186 uri da togliere (accorpare almeno il lavoro sul db magari aiuta) -> Gares, CSC
187 - quando si sposta il punto di esecuzione dello script cambiare la parte di
188 script visibile nella finestra dello script -> Gares, CSC
189 - find & replace -> Gares
190 - Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
192 - Bug: non disambigua
193 inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
194 perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug
195 stupido da qualche parte -> CSC
196 - Bug vari nella generazione dei principi di eliminazione:
197 1. generazione nomi (usa ref incrementata localmente) -> Andrea
198 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
199 passo il test inversion.ma) -> CSC, Gares
200 3. usato trucco outtype non dipendenti per il case -> CSC, Gares
201 - controllo per script modificato o meno prima di uscire -> Gares
202 - LApply deve prendere in input gli identificatori che va a generare;
203 lascio a Ferruccio la scelta della sintassi concreta -> Ferruccio
204 - fare tornare a matitac -1 quando lo stato finale e'
205 diverso da No_proof, non eseguire comandi quando lo
206 stato e' diverso da No_proof -> CSC
207 - uri_of_term and term_of_uri: cambiare il tipo per far
208 tornare delle uri!!! -> CSC
209 - intro = intros 1 -> Gares
210 - timetravel (urimanager) -> Gares
211 - implementare macro in matitaScript.ml -> Gares
212 - history deve aggiornare anche la whelp bar -> Gares
213 - commenti exeguibili (forse devono essere una lista e non
214 un singolo executable e forse devono contenere anche Note
215 e non solo Executable) -> Gares
216 - spostare il codice di creazione delle tabelle da
217 MatitaDb, al momento quelle create da matita possono
218 andare out of sync con quelle create dai file .sql -> Gares
219 - tree update in background -> Gares
220 - update del getter in background -> Zack
221 - agganciare href_callback del sequent_viewer -> Zack
222 - shortcut varie per script handling -> Zack
223 - operazioni rimanenti su script (top, bottom, jump) -> Zack
224 - lighting-ls-getter in matita -> Gares
225 - riagganciare toolbar -> Zack
226 - evitare che n-mila tattiche Goal siano nello script
227 (una per ogni cambio di tab) -> Zack
228 - implementazione comandi rimanenti in matitaEngine.ml -> Gares
229 - sintassi per gli alias -> Gares
230 - implementazione script handling (sopra engine) -> Zack
231 - matitaSync all'indietro -> Gares
232 - riagganciare GUI -> Zack
234 (**********************************************************************)
237 - interattivi (solo da gui)
238 - Macro/Comandi (check, print, hint, undo, locate, match)
239 potrebbero anche non avere sintassi concreta, del tipo che
240 check e' solo un bottone che apre una finetra in cui puoi
241 scrivere un termine o selezionarlo dalla prova corrente
242 - batch (sono gli unici che stanno nel .ma)
243 - Tattiche, theorem, alias (cambiano la prova)
247 -------------------------------------------+
248 gui (macro: hint) | SHELL
250 +-----------------+---------------+-----------------------------------
251 | matita (status) | | matitac
252 | (log) (sync) | but2log | fold ( fun s l -> engine l s) file
253 +-----------------+---------------+-----------------------------------
254 | lingua:/sintassi concreta non ambigua delle tattiche+Qed,Thm,alias/
255 +----------------------------------------------------------
256 | engine: TacticAst (cic) -> status -> status
257 | ma non usa il campo alias dello status
258 ---------+----------------------------------------------------------
260 --------------------------------------------------------------------
264 - accetta solo linee non ambigue
266 alias ident nat = "cic:/matita/gares/nat.ind#(1/1)".
267 alias number = (natural|real|positive|integer).
272 - mantiene uno stack di stati
273 - mantiene un log sync con gli stati
274 - offre delle api per generare la sintassi concreta che puo' servire
275 alla gui (la gui fa una chiamata a funzione e matita genera "auto."
276 cosi' la sintassi la gui non la vede mai e la tratta al massimo come un
277 testo semplice e basta (insomma, metterei in matita il generatore di
278 sintassi concreta) but2log
279 - ha il controllo... ovvero anche la gui viene usata da matita, o per sapere
280 la prossima azione o per chidere di scegliere il termine tra una lista
282 (stato :: tl) (log , (start,end) :: tl)
294 - proof status option
295 - metadati relativi allo script per il sync
296 - settings "baseuri/url/" eccc
302 engine prende in input
303 - AST di Cic (tactic ast)
306 - presi 2 stati fa il diff e lo somma/sottrae al DB
308 (**********************************************************************)
311 - ad ogni script sul quale l'utente sta lavorando corrispondono
312 - un modello (vedi sotto)
313 - un buffer di testo gtk + attributi (usati principalmente per distinguere la
314 parte di testo immodificabile da quella modificabile)
315 - una lista di observer che vengono notificati ad ogni cambiamento di stato
316 - un modello di script e' composto da:
317 - una lista di stringhe (inizialmente vuota) detta "statement list". Ogni
318 elemento della lista corrisponde ad uno statement (nel senso di
319 TacticAst.statement) gia' valutato dall'engine. La parte immodificabile del
320 buffer di testo corrisponde con le stringhe contenute nella lista
321 - una lista di stati (inizialmente contenente lo stato vuoto) detta "state
322 list". Si ha l'invariante che la lunghezza di tale lista e' uguale alla
323 lunghezza della statements list + 1. Lo stato i-esimo della lista di stati
324 e' lo stato di matita _prima_ dell'esecuzione dell i-esimo statement
325 - una stringa, detta "future text", corrispondente alla parte di testo dello
326 script non ancora valutata. L'ultimo stato della state list e' lo stato
328 - relazione tra modello e buffer di testo gtk
329 - le modifiche al testo del buffer sono possibili solo nella parta non ancora
330 valutata. Ognuna di esse viene apportata _anche_ al future text
331 - invariante: e' sempre possibile riscrivere ("redraw") l'intero contenuto del
332 buffer di testo a partire dal modello, attributi compresi
335 - new: gtk_text_buffer -> script
336 - redraw: unit (* ridisegna il contenuto del buffer di testo *)
337 - advance: ?statement:string -> unit -> unit
338 (* valuta il primo statement del future text (usando eval_statement
339 (puo' fallire con una eccezione)), rimuove il testo corrispondente dal
340 future text, aggiunge alla statement list una entry per ogni statement
341 ritornato da eval_statement, aggiunge il nuovo stato alla state list,
342 invoka tutti gli observer
343 Se c'e' l'argomento opzionale statement, quello e' il testo che viene
344 passato ad eval_statement, se ha successo nessuna rimozione dal future
345 text viene effettuata *)
346 - retract: unit -> unit
347 (* sposta l'ultimo statement della statement list al future text, toglie
348 l'ultimo stato della state list, MatitaSync.time_travel
349 ~present:ultimo_stato ~past:stato_precedente *)
350 - private eval_statement: string -> MatitaTypes.status * string list
351 (* parsa lo statement
352 - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine
353 passando lo stato corrente
354 - se e' una Macro la gestisce (= tutte le Macro sono implementate qua)
355 Ritorna una lista di coppie <stato, statement>. La proiezione sulla
356 prima componente rappresenta gli stati da aggiungere alla state list;
357 quella sulla seconda gli statement da aggiungere alla statement list.
359 (* gestione degli observer *)
360 - add_observer: (MatitaTypes.status -> unit) -> observer_id
361 - remove_observer: observer_id -> unit
362 (* gestione del salvataggio *)
363 - save_to: string -> unit (* ridisegna su file *)
364 - load_from: string -> unit
365 (* retract fino allo stato zero, nuovo stato con future text pari al
366 contenuto del file passato *)