TODO
NUCLEO
- - CRITICO (trovato anche da Ferruccio): typechecking di
- cic:/Coq/ring/Ring_normalize/index_eq_prop.con
- asserzione del nucleo (applicazione senza argomenti)
+ - 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
- riattaccare hbugs (brrr...) -> Zack
GUI LOGICA
+ - 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!!!)
- - verificare se tutte le query sono ora ottimizzate (usando il comando
- explain) e usano gli indici in maniera ottimale; inoltre migliorare gli
- indici sulle tabelle hits and count
- - ???????????? Perche'?
- mowgli:~# du -s /var/lib/mysql/mowgli/
- 250696 /var/lib/mysql/mowgli/
- mowgli:~# du -s /var/lib/mysql/matita/
- 455096 /var/lib/mysql/matita/
- - integrare nuova contrib ferruccio nel bench notturno; guardare bug
- generazione principi di eliminazione
+ - integrare nuova contrib ferruccio nel bench notturno e rilocarla in
+ contribs o qualcosa del genere
- 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
i demoni scopiazzano venti righe per via del getter embedded :-(
DONE
+- 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
+- verificare se tutte le query sono ora ottimizzate (usando il comando
+ explain) e usano gli indici in maniera ottimale; inoltre migliorare gli
+ indici sulle tabelle hits and count -> CSC
+- ???????????? Perche'?
+ mowgli:~# du -s /var/lib/mysql/mowgli/
+ 250696 /var/lib/mysql/mowgli/
+ mowgli:~# du -s /var/lib/mysql/matita/
+ 455096 /var/lib/mysql/matita/ -> CSC
- library/nat/primes.ma: ex_prime ci mette un secolo il db (binding) a fare
la Mysql.exec che ritorna una lista vuota di risultati. Investigare.
Anche peggio in library/nat/minimization/f_max_true. -> CSC