A formalization of modified realisability with truth as in
``Internalising modified realisability in constructive type theory'',
Erik Palmgren, Logical Methods in Computer Science, Vol 1. (2:2), 2005, pp 1--7.
Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.
Enrico Tassi [Thu, 10 Jan 2008 22:32:03 +0000 (22:32 +0000)]
BIG FAT WARNING: DEVELOPMENTS DIE HERE
What follows is the email on the helm mailing list
Riassunto:
- non esistono più i developments
- non esiste più il comando set "baseuri" "cic:/...." (non serve più)
- questa mail è parecchio lunga, ma le prossime 2 sezioni le consiglio
a _tutti_, quelle successive solo a chi aveva molti development
dipendenti luno dall'altro. Ad ogni modo, il manuale di matita (che
si apre con F1) è stato aggiornato e al posto dei developments ora
spiega come funziona ora la compilazione.
Dove sono scritte le baseuri?
- nella radice dei vostri ma (per esempio library/, tests/,
contribs/RELATIOANL etc...) c'è un file di testo chiamato 'root'.
- ad esempio il file library/root contiene una riga tipo:
baseuri = cic:/matita
- la baseuri in cui i files .ma vengono compilati si calcola guardando
il path tra la radice e il file. As esempio
library/nat/plus.ma
essendo "radicato" da library/root che definisce la baseuri a
cic:/matita verrà compilato in
cic:/matita + /nat/plus/
(esattamente dove era compilato prima, e tutti i .ma committati,
quando necessario, sono stati porati a questo schema. In tutta
library solo 1 file non lo rispettava).
Come si compila adesso che non c'è più matitamake?
- da matita non cambia nulla, ho solo tolto un paio di popup che
chiedevano sempre conferme di cose inutili (tipo se compilare il file
incluso o no... ora lo compila sempre).
- matitac ha cambiato leggermente semantica, ma potete fregarvene: la
seguente linea continua a funzionare e fa le stesse cose di prima.
cd library; make opt
- il file delle dipendenze tra i files .ma prima veniva generato a ogni
make con matitadep, ora non viene più fatto, quindi se cambiare gli
includes che fate in un file fate un make depend.opt (o make depend
se avete compilato in bytecode).
matitadep è sempre stato lento, per questo motivo non viene chiamato
tutte le volte. stamattina ho risolto un vecchissimo problema
(ricordate che ogni tanto andava in stack overflow?) e ora mi sembra
anche molto più veloce, quindi forse lo si potrebbe lanciare sempre
... vedremo
Qui finisce la parte necessaria a tutti, ci si sente coraggioso continui
pure. In generale il codice ML è diventato più semplice, matita è anche
più veloce a compilare e spero che i vari BUG dei developments siano
spariti. Chiaramente ce ne saranno di nuovi... ma spero di meno.
Dettagli del root file (dipendenze tra radici)
- il root file è una lista associative chiave -> valore le cui linee
matchano la seguente regexp:
\s*[^=]+\s*=\s*.+\s*
le chiavi utilizzabili sono: baseuri, include_paths.
- per esempio, tests/ ha bisogno di legacy/ e vari files in tests/
hanno la riga: include "coq.ma". Il root file per tests è:
baseuri=cic:/tests
include_paths=../legacy
- library/ sta sempre negli include paths, se usate files in library
non è necessario dichiarare il relativo include path
- si possono dichiarare più include_paths, separandoli da spazi. per
sempio
include_paths=../foo ../../bar/baz
- i files che includete devono esistere in uno degli include paths,
e vengono cercati:
- in / (path assoluto, da evitare possibilmente)
- in .
- in library/
- negli include_paths
- una volta scritto il root file, lanciando matitadep viene generato
un file depends. Tale processo da anche degli errori, in caso alcuni
files non riescano ad essere trovati nei paths specificati
- una volta fatto ciò matita lanciato da dentro una radice compila
tutto, quindi se serve "salta" in una delle radici specificate
dagli include_paths e compila pure li dentro
- non sono supportati (e non so nemmeno cosa voglia dire) files con lo
stesso nome (e path relativo alla radice) in radici differenti,
in tal caso include "a.ma" se a.ma esiste anche in una delle radici
da cui si dipende, include sempre quello locale (prima c'era un bug
per cui includeva quello non-locale). ho dovuto fare un po di
renaming nei files di ferruccio, da capire se vanno bene.
Dove è finito make:
- matitac ora legge il file depends e compila lui i files nell'orine
giusto (e solo se necessario).
./matitac compila tutto (nella radice della dir corrente)
./matitac foo/a.ma compila a.ma (e le sue dipendenze se necessario)
- matitadep ha bisogno di un file root, detto ciò si cerca i files con
estensione .ma e ne genera un depends, con formato:
a b c
b d
d
c
le lettere sono nomi di files (quindi .ma, niente .moo, .mo,
.mo.opt etc...). Le linee si leggono come
a deve essere compilato dopo b e c
b dopo d
d e c anche subito
i files esterni alla radice (trovati via include paths) vengono
listati anche loro, senza dipendenze (tanto salta nella loro radice e
fa "make" li dentro, dove le sue dipendenze sono note).
Mi sembra più veloce a compilare?!
- prima, per ogni file .ma, veniva lanciato matitac, ora è lo stesso
matitac a compilare tutti i files uno dopo l'altro. Il tempo speso a
creare un processo (e per matita ce ne vuole parecchio) è
risparmiato, quindi per un set di files molto piccoli si vede anche
ad occhio la differenza.
- il fatto che non venga generato un nuovo processo ha fatto si che
tutti i bug relativi all'undo (parti imperative dello stato)
venissero a galla. Ne è rimasto solo uno, che non so risolvere:
quando camlp5 stampa "<W> una regola è stata mascherata" che li pare
che tutto si inceppi.
- il nostro environment è imperativo e nessuno lo svuota mai,
risultato: non carica gli oggetti da disco quasi mai... è sia un bene
che un male... potrei resettarlo alla fine di ogni comilazione...
- Non ho mai provato a fare .ma con dipendenze circolari, magari diverge.
projects / helm.git / log