Makefile missing in previous commit

New developement LOGIC about the cut elimination of implication for Sambin's basic logic; one of the rules must be corrected (work is in progress)

added test about dependent coercions

Prototype of min_aux changed.
Now (min_aux off n f) find the smallest i such that
* f i = true or i = n+off
* \forall j,  n <= j <= n+off,  f j = false

The new function does no longer compute with off. Thus we obtain
for free a great computational speed-up in every function defined
in terms of it.

auto vs autobatch fixed

autobatch parameters reajusted

fixed makefiles to make it compile cleanly again

Procedural: the statement body and it inner types must satisfy the Barendregt
            convenction on bound variables

Another nicer version.

Even nicer script.

The nicest script obtained so far.
What is left, is a bunch of change/normalize/whd/simplify that are difficult
to control precisely.

acic_procedural: bug fix:
                 sometimes whd is not enough, we need normalize ...

More simplification due to the new conversion strategy.

Script simplification due to the new efficient conversion strategy.

Tentative bug fix for diverging pretty-printing function.

Initialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit
(so that ocamlc now works again).

cicUtil        : new test function "is_sober" to test the integrity of a term
                 now fails when fake applications are detected
acic_procedural: some bug fix

Convertibility now converts machines in place of terms.
Actually, the heads of the machines (i.e. everything but the stack) are
still unwinded and converted as terms. Thus there is much space for
improvement.

map_unicode_to_tex is no longer optional and it always refers to the current
user choice.

paste_unicode_as_tex is now false by default; moreover the flag is used
everywhere (but in patterns, I do not know why)

COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.

the cade was escaping the table name and not the uri

fixed escaping for sqlite

fixed an escaping error, added more infos to the generic error, callback catches and prints exceptions

Typo fixed.

Super-nice notation for the assembly stuff.

the predicate for elim was not built correctly when more than one right parameter was found

recursive argument in let rec is not printed explicitly.
I let to ferruccio optimize the case in which there is only one argument or the recno is 0 and thus can be omitted

fixed coercion graph print, moved coercion graph and auto gui to the view menu, added a mini test about coercions

added missing parenthesis

fixed includes and added notation for bytes

More lemmas.

More daemons closed. A couple left in byte and many in extras.

More daemons/axioms closed.

One daemon less.

More daemons got rid of (and more extra axioms to be proved).

Last daemon killed :-)

One less daemon (about "update"s).

All sub-proofs about "update" closed.

assembly.ma splitted into many files

* NOT RELEASED YET

* NOT RELEASED YET

proper path for ps.gz doc

texlive-base-bin, texlive-latex-extra

  - add build-dep for doc generation: graphviz, texlive-latex-recommended,

  - add build-dep for doc generation: graphviz, texlive-latex-base,
    texlive-base-bin

* debian/rules
  - build ocamldoc documentation at package build time
  - add build-dep on graphviz

invoke make doc after build to create ocamldoc docs

* debian/svn-deblayout
  - add repository layout information

* rebuild against OCaml 3.10 and ocamlnet 2.2
* add preliminary support for cookies (new "cookies" method added to an
  - use ocaml.mk CDBS class
  - add build-dep on camlp4, which is now in a separate package
- bump debhelper dep and compatibility level to 5

* debian/*.install.in
  - do not attempt to instal *.ml files in target lib directory since they
    are no longer installed by Makefile

* rebuild with OCaml 3.10
* bump debhelper deps and compatibility level to 5
  - s/Source-Version/binary:Version

corrected axiom mod_plus

new definitions and new theorems

More conjectures closed.

1. requires the new pretty printer for natural numbers
2. important properties of plusbyte proved
3. all important conjectures almost proved

Dirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers. Eureka.

Last crazy commit reverted.

Final theorem proved. Many many conjectures left. I am unsure of one of them.

The loop invariant I chosed was not correct!

1. statement to be fixed
2. is the new loop invariant strong enough?
3. lot of daemons here and there
4. two conjectures I am not sure of:
   plusbytenc (x*n) x = byte_of_nat (x*S n)
   plusbytec  (x*n) x = plusbytec (x*S n)

Getting close to the final result.
The showstopper now is the GtkMathView/Pango bug!
Moreover, unification has become mostly useless (and rewriting with it).

1. loop invariant stated, but not proved
2. final theorem stated and proved

native dependences fixed

1. status factorized out in tick
2. 0*0=0, 0*2=0, x*1=x, x*2=x+x proved
3. still way too slow!

auto new => autobatch

auto new => autobatch

0. less nice solution by Enrico reverted
1. some bug fixes in assembly code
2. test program simplified
3. reduction now works as expected, thanks to the new reduction strategy
4. BIG BUG SOMEWHERE: (270 \mod 256) reduces to 14 instead of 4!!!
5. requires primitive addition over exadecimal numbers and bytes to
   avoid representing 0+x as byte_of_nat (nat_of_byte x) that does not
   reduce

New reduction strategy: the new reduction strategy behaves as the previous
one (performing both CVN and CBV in parallel), but it is much more lazy.
In particular, unwinding is never performed twice on the same term.
On assembly/assembly.ma this seems to solve every performance problem.
Let's see what happens this night with the benchmarks.

La programmazione funzionale e' come TeX, funziona meglio se la prendi a calci.

persistent inner types are now generated in publishing mode

fixed a bug in the cleanup ofsedir that was not properly catching #xpointer

...

1. bug fixed in tick
2. added notation for some big number
3. the whd CBN is responsible for the huge timing;
   reduce works since it is CVB

signal hadler restored after runnig external 'make'

Interesting theorem added (but still to be proved).

added few more fun to this test

new configuration file sample

tassi: ported to the new DB architecture.
since the 'user' db is mandatory, a fake one should be provided

auto->autobatch

inclusion of div_and_mod

maxipatch for support of multiple DBs.

new 3 different kind of BD can coexist:
user) the user db, where his stuff is stored
   tables are named foo_user
library) the library db, a read only database where the standard library should be
   installed and that is the target of the publish act
legacy) a legacy database (not mandatory) where really read only data is stored

every db can be implement with an sqlite file or a mysql database.

the default configuration file sets 1 and 2 to be the mysql matita database on mowgli,
thus nothing should change for mowgli users. database 3 is not used if you are on mowgli.

the way it should be used by matita users out of the unibo network is commented in the config file:
1) file://~/.matita/user.db for his development
2) file:///usr/share/matita/metadata.db for the matita precompiled standard library
3) mysql://mowgli.cs.unibo.it for the legacy coq stuff, both queries and xml are fetched trough
   the net

this allows us to really distribute matita in a rather sane way, with a
precompiled library visible systemwide and having all per user data and
metadata in ~/.matita. There is no need for the user to install and configure
mysql, and can use mowgli just decommenting few lines in the config file.

Exadecimal numbers are now used. This is a great speed-up.
Moreover, byte_of_nat is now modulo 256. Thus ADDd is now implemented
correctly.

Example program executed for x,y=0.
It works (slowly, much slowly)!

Quick hack: matita natural numbers are now accepted by the parser/disambiguator.
If nat/nat.ma is not compiled yet, I do not know what happens.

Bug fixed: a ~with_cast is now inserted when appropriate to avoid translation
of a bottom-up conversion into a top-down conversion.

In place of conclude, obtain FIXMEXXX is now generated when required.

1. Code simplification
2. Bug fixed: do not anticipate justification for rewritingLR or rewriting RL
   if justification is "exact"

is_top_down was not propageted correctly under a bottom-up conversion.

1. "by proof" now allowed as a justification in equality chains.
   It opens a side-proof to be proved immediately.
2. Side proofs restored in equality chains in content2pres.ml

Added ~with_cast to the change tactic.
When with_cast is true, a cast is recorded in the lambda term.

Bug fixed: name in letin was printed as "previous" even if given.

More opcodes (badly) implemented.

List.ma: added function nth (with default value in case of failure)
Assembly: a toy example on proving properties of assembly programs.
 It should be moved somewhere else. It shows HUGE problems with
 simplification and display of (very very large) terms.

New definition of Euler's totient function.
New theorems about sigma_p (invoked with an always true predicate).
Theorem about the sum of totient invocations on the divisors of a natural number.

In order to generate executable declarative scripts, we are now splitting
the "Rewrite" content-level method into "RewriteRL" and "RewriteLR".

Bug fixed in bottom-up conversion.
Since the bottom-up conversion body is put in the applicative context and since
applicative contexts get flattened the test for being in a bottom-up conversion
must be rather complex.

BU Conversion was not generated for Rels fixed. I wonder why...

Nicer layout but possibly more bugged.
We need continuations here to do a good job.

Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
generated.

generic version, specializing generic_sigma_p.ma