oldenv2newenv cache

uri and references(uri)

uri -> reference (2)

uri -> reference

lower bound for neper's constant

sad snapshot

snapshot

snapshot

Improved approximations for A and prim.

Some improvement.

very bad bug found, asert false in cicReduction when a clear is performed

One Obj.magic implemented, trust changed to false.

Transformation back and forth between old and new representation

snapshot

new uri defined

Square root added.

snapshot]

snapshot

added meta for the new kernel

stub functions to make all compile

basic organization of the new kernel

Improved approximations

New approximtions.

...

snapshot with more duality, almost where we left without duality

...

Bertrand's conjecture (weak), some work in progress

snapshot

Matitac now accepts multiple targets :-) (but only in the same root :-(

Hack for code extraction re-linked, but disactivated.

Old tiny freescale experiment get rid of.
New shiny freescale formalization by Cosimo Oliboni <oliboni@cs.unibo.it>,
described in his Laurea Thesis.

Typo fixed.

snopshot before isabellization

snapshot

3.27 ok

yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

update: upper bound for prim

more lemmas, til 3.26

new deps

first lemma

fixed a pulback and proved 3.17

added some doc

user time is now printed correctly

better parsing of the root file

fixed uris

Chebyshev's upper bound on prim

removed path for contribs

added a warning when a file is not compiled cause its buri is readonly

Make does not even try to build files that would be compiled in read-only
baseuris

I'll talk again with ferruccio, for the moment this is the right
way to allow every user that does and svn co to compile everithing.

another fix to make it more resistant

many sed to use notation for rewriting

.opt before .byte

ugly hack to make matitac not exit when called on a readonly baseuri, but just fail

added a warning if the baseuri we want to clean is read-only

-dot fixed, now the .dot file contains also edges

increased timout

removed useless assertion

increased a timeout, matitac (not .opt) should be able to do it in time

added Sys.catch_break true

cache for mtime of files is not polluted with None, minimal speedup

Make was caching too much, thus some targets were not rebuild properly

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.

implementation of the make algorithm, still unfinished.
to be integrated with matitac to drop our beloved developments.

* use findlib to pass -I flags down to ocamldoc, instead of relying on
  hard-coded paths

* bump standards-version, no changes needed

* convert the package to a non-native Debian package

* debian/rules: instead of passing explicit -I flags to ocamldoc, do them
  via ocamlfind and OCAML_OCAMLDOC_OCAMLFIND_FLAGS

overwrite old symlink upon dist

ignore tons of generated stuff

* convert package to a non-native one (closes: #457353)

* promote Vcs-* fields to real debian/control fields
* update standards-version, no changes needed

beginning proof of chebyshev's bound on prim.

accepts the poly shape for gviz maps

upper bound for logarithmic summation

A few more lemmas.

Much more verbose statistics.

Bug fixed: \n prevented recognition.

Some inequalities.

Progress.

add support for adding identifiers instead of only changing them (enabled per default)

Partial progress.

more chosmetic

Main result for e.

sandeich lemma makeup

Restructuring.

Main inequalities for e.

Added summation formula for the power of a binomial.

the is_structure is a bad idea if you don't have canonical structures.

Binomial coefficients and costant e.

A few more theorems.

dump spurious errors max

excede->excess

excedence -> excess

weight -> value

dump result table in \TeX format

...

Repeated errors are not duplicated.

Even if the error is not localized, it was not a good idea to make the unification error
escape.

refactoring of some lemmas, shorter proofs