BIG FAT WARNING: DEVELOPMENTS DIE HERE

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.