* 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
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).
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.
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.
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
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.
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.
Enrico Tassi [Wed, 13 Jun 2007 13:01:32 +0000 (13:01 +0000)]
many changes:
1) fixed many bugs and added support for implicit detection in
cic -> declarative
2) added a tactic to find a proof rewriting n times with a given universe
used instead of auto_paramodulation in the declarative language
(here you know that 1 rewriting step with that lemma is enough)
3) added ESCAPE to sql queries using LIKE, to make sqlite and mysql compatible
I do not know why, but
(Helm_registry.get_list Helm_registry.string "matita.includes")
is extremely slow! Removing it from the inner loop really improves performances!
DOOMSDAY 1.0:
this is the commit that (partially) allows Matita to understand its own
output. I.e. the natural language generated is now the declarative language.
This is probably still highly bugged in most cases.
Ferruccio has changed the semantics of the old ~pattern argument of elim_tac.
However, he did not fix by_induction_tac accordingly. For now I comment out
the ~pattern application. To be fixed.