]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agodefault equality stuff filtered out from hint rewrite
Enrico Tassi [Tue, 31 Jul 2007 10:39:53 +0000 (10:39 +0000)]
default equality stuff filtered out from hint rewrite

17 years agoremoved comments in proof presentation
Enrico Tassi [Tue, 31 Jul 2007 10:39:31 +0000 (10:39 +0000)]
removed comments in proof presentation

17 years agorenamed generic_sigma_p.ma to generic_iter_p.ma
Cristian Armentano [Mon, 30 Jul 2007 15:01:31 +0000 (15:01 +0000)]
renamed generic_sigma_p.ma to generic_iter_p.ma

17 years agoadded 'rewrite' option to the the hint macro. a cicBrowser with all library
Enrico Tassi [Mon, 30 Jul 2007 12:00:31 +0000 (12:00 +0000)]
added 'rewrite' option to the the hint macro. a cicBrowser with all library
objects that may rewrite the goal is displayed.

17 years agoWe add a binary for computing the "heights" of helm objects
Ferruccio Guidi [Thu, 26 Jul 2007 14:35:05 +0000 (14:35 +0000)]
We add a binary for computing the "heights" of helm objects
[this is related to the height of the dependece tree]

17 years agoadded development path normalization, inclusions with '../' in the path should now...
Enrico Tassi [Thu, 26 Jul 2007 13:47:07 +0000 (13:47 +0000)]
added development path normalization, inclusions with '../' in the path should now be handled correclty

17 years agoauto -> autobatch
Enrico Tassi [Thu, 26 Jul 2007 13:46:07 +0000 (13:46 +0000)]
auto -> autobatch

17 years agoSome notation added
Wilmer Ricciotti [Thu, 26 Jul 2007 13:06:09 +0000 (13:06 +0000)]
Some notation added

17 years agomore stuff about coercions
Enrico Tassi [Thu, 26 Jul 2007 10:41:15 +0000 (10:41 +0000)]
more stuff about coercions

17 years agolittle bug in coercion generation found. it use to create more coercions that expecte...
Enrico Tassi [Thu, 26 Jul 2007 10:39:38 +0000 (10:39 +0000)]
little bug in coercion generation found. it use to create more coercions that expected (luckily convertible).

17 years agomakefiles updated
Ferruccio Guidi [Thu, 26 Jul 2007 08:58:11 +0000 (08:58 +0000)]
makefiles updated

17 years agomakefile updated
Ferruccio Guidi [Wed, 25 Jul 2007 19:05:34 +0000 (19:05 +0000)]
makefile updated

17 years agomatitac: We do not generate the .moo and .lexicon of a dumped .mma
Ferruccio Guidi [Wed, 25 Jul 2007 14:39:14 +0000 (14:39 +0000)]
matitac: We do not generate the .moo and .lexicon of a dumped .mma
Base-2 : makefile patched

17 years agoadded some notation
Enrico Tassi [Wed, 25 Jul 2007 13:55:53 +0000 (13:55 +0000)]
added some notation

17 years agoadded another example in which our coercions are powerful
Enrico Tassi [Wed, 25 Jul 2007 10:13:55 +0000 (10:13 +0000)]
added another example in which our coercions are powerful

17 years agoused ;try assumption instead of .try assumption
Enrico Tassi [Wed, 25 Jul 2007 09:43:35 +0000 (09:43 +0000)]
used ;try assumption instead of .try assumption

17 years ago; and not . after auto-paramodulation
Enrico Tassi [Wed, 25 Jul 2007 09:41:50 +0000 (09:41 +0000)]
; and not . after auto-paramodulation

17 years agoreverted previous fix
Enrico Tassi [Wed, 25 Jul 2007 09:40:14 +0000 (09:40 +0000)]
reverted previous fix

17 years agorestored compaction of metas at the end of given_clause
Enrico Tassi [Wed, 25 Jul 2007 09:18:36 +0000 (09:18 +0000)]
restored compaction of metas at the end of given_clause

17 years agoMakefile missing in previous commit
Ferruccio Guidi [Tue, 24 Jul 2007 11:54:28 +0000 (11:54 +0000)]
Makefile missing in previous commit

17 years agoNew developement LOGIC about the cut elimination of implication for Sambin's basic...
Ferruccio Guidi [Tue, 24 Jul 2007 11:52:05 +0000 (11:52 +0000)]
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)

17 years agoadded test about dependent coercions
Enrico Tassi [Tue, 24 Jul 2007 08:58:16 +0000 (08:58 +0000)]
added test about dependent coercions

17 years agoPrototype of min_aux changed.
Claudio Sacerdoti Coen [Mon, 23 Jul 2007 15:14:29 +0000 (15:14 +0000)]
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.

17 years agoauto vs autobatch fixed
Ferruccio Guidi [Mon, 23 Jul 2007 13:22:22 +0000 (13:22 +0000)]
auto vs autobatch fixed

17 years agoautobatch parameters reajusted
Ferruccio Guidi [Mon, 23 Jul 2007 13:12:40 +0000 (13:12 +0000)]
autobatch parameters reajusted

17 years agofixed makefiles to make it compile cleanly again
Enrico Tassi [Mon, 23 Jul 2007 09:14:53 +0000 (09:14 +0000)]
fixed makefiles to make it compile cleanly again

17 years agoProcedural: the statement body and it inner types must satisfy the Barendregt
Ferruccio Guidi [Sun, 22 Jul 2007 18:33:38 +0000 (18:33 +0000)]
Procedural: the statement body and it inner types must satisfy the Barendregt
            convenction on bound variables

17 years agoAnother nicer version.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 16:59:27 +0000 (16:59 +0000)]
Another nicer version.

17 years agoEven nicer script.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 16:53:33 +0000 (16:53 +0000)]
Even nicer script.

17 years agoThe nicest script obtained so far.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 16:20:30 +0000 (16:20 +0000)]
The nicest script obtained so far.
What is left, is a bunch of change/normalize/whd/simplify that are difficult
to control precisely.

17 years agoacic_procedural: bug fix:
Ferruccio Guidi [Fri, 20 Jul 2007 14:48:36 +0000 (14:48 +0000)]
acic_procedural: bug fix:
                 sometimes whd is not enough, we need normalize ...

17 years agoMore simplification due to the new conversion strategy.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 14:28:55 +0000 (14:28 +0000)]
More simplification due to the new conversion strategy.

17 years agoScript simplification due to the new efficient conversion strategy.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 14:26:01 +0000 (14:26 +0000)]
Script simplification due to the new efficient conversion strategy.

17 years agoTentative bug fix for diverging pretty-printing function.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 09:58:30 +0000 (09:58 +0000)]
Tentative bug fix for diverging pretty-printing function.

17 years agoInitialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 09:32:39 +0000 (09:32 +0000)]
Initialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit
(so that ocamlc now works again).

17 years agocicUtil : new test function "is_sober" to test the integrity of a term
Ferruccio Guidi [Thu, 19 Jul 2007 18:00:55 +0000 (18:00 +0000)]
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

17 years agoConvertibility now converts machines in place of terms.
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 17:54:40 +0000 (17:54 +0000)]
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.

17 years agomap_unicode_to_tex is no longer optional and it always refers to the current
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 12:07:44 +0000 (12:07 +0000)]
map_unicode_to_tex is no longer optional and it always refers to the current
user choice.

17 years agopaste_unicode_as_tex is now false by default; moreover the flag is used
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 10:19:28 +0000 (10:19 +0000)]
paste_unicode_as_tex is now false by default; moreover the flag is used
everywhere (but in patterns, I do not know why)

17 years agoCOERCIONS: tentative addition of an equivalence relation over coercion source
Enrico Tassi [Thu, 19 Jul 2007 10:03:42 +0000 (10:03 +0000)]
COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.

17 years agothe cade was escaping the table name and not the uri
Enrico Tassi [Thu, 19 Jul 2007 10:02:11 +0000 (10:02 +0000)]
the cade was escaping the table name and not the uri

17 years agofixed escaping for sqlite
Enrico Tassi [Thu, 19 Jul 2007 10:01:40 +0000 (10:01 +0000)]
fixed escaping for sqlite

17 years agofixed an escaping error, added more infos to the generic error, callback catches...
Enrico Tassi [Thu, 19 Jul 2007 10:01:13 +0000 (10:01 +0000)]
fixed an escaping error, added more infos to the generic error, callback catches and prints exceptions

17 years agoTypo fixed.
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 09:17:32 +0000 (09:17 +0000)]
Typo fixed.

17 years agoSuper-nice notation for the assembly stuff.
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 09:15:31 +0000 (09:15 +0000)]
Super-nice notation for the assembly stuff.

17 years agothe predicate for elim was not built correctly when more than one right parameter...
Ferruccio Guidi [Wed, 18 Jul 2007 16:07:11 +0000 (16:07 +0000)]
the predicate for elim was not built correctly when more than one right parameter was found

17 years agorecursive argument in let rec is not printed explicitly.
Enrico Tassi [Wed, 18 Jul 2007 11:17:46 +0000 (11:17 +0000)]
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

17 years agofixed coercion graph print, moved coercion graph and auto gui to the view menu, added...
Enrico Tassi [Wed, 18 Jul 2007 10:46:11 +0000 (10:46 +0000)]
fixed coercion graph print, moved coercion graph and auto gui to the view menu, added a mini test about coercions

17 years agoadded missing parenthesis
Claudio Sacerdoti Coen [Tue, 17 Jul 2007 11:41:07 +0000 (11:41 +0000)]
added missing parenthesis

17 years agofixed includes and added notation for bytes
Enrico Tassi [Tue, 17 Jul 2007 10:00:30 +0000 (10:00 +0000)]
fixed includes and added notation for bytes

17 years agoMore lemmas.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 22:20:08 +0000 (22:20 +0000)]
More lemmas.

17 years agoMore daemons closed. A couple left in byte and many in extras.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 21:39:13 +0000 (21:39 +0000)]
More daemons closed. A couple left in byte and many in extras.

17 years agoMore daemons/axioms closed.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 20:48:20 +0000 (20:48 +0000)]
More daemons/axioms closed.

17 years agoOne daemon less.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 17:51:02 +0000 (17:51 +0000)]
One daemon less.

17 years agoMore daemons got rid of (and more extra axioms to be proved).
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 17:35:38 +0000 (17:35 +0000)]
More daemons got rid of (and more extra axioms to be proved).

17 years agoLast daemon killed :-)
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:10:40 +0000 (16:10 +0000)]
Last daemon killed :-)

17 years agoOne less daemon (about "update"s).
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:07:42 +0000 (16:07 +0000)]
One less daemon (about "update"s).

17 years agoAll sub-proofs about "update" closed.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:04:05 +0000 (16:04 +0000)]
All sub-proofs about "update" closed.

17 years agoassembly.ma splitted into many files
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 14:51:18 +0000 (14:51 +0000)]
assembly.ma splitted into many files

17 years ago* NOT RELEASED YET
Stefano Zacchiroli [Mon, 16 Jul 2007 14:34:55 +0000 (14:34 +0000)]
* NOT RELEASED YET

17 years ago* NOT RELEASED YET
Stefano Zacchiroli [Mon, 16 Jul 2007 14:33:30 +0000 (14:33 +0000)]
* NOT RELEASED YET

17 years agoproper path for ps.gz doc
Stefano Zacchiroli [Mon, 16 Jul 2007 14:30:27 +0000 (14:30 +0000)]
proper path for ps.gz doc

17 years ago texlive-base-bin, texlive-latex-extra
Stefano Zacchiroli [Mon, 16 Jul 2007 14:21:44 +0000 (14:21 +0000)]
texlive-base-bin, texlive-latex-extra

17 years ago - add build-dep for doc generation: graphviz, texlive-latex-recommended,
Stefano Zacchiroli [Mon, 16 Jul 2007 14:17:45 +0000 (14:17 +0000)]
  - add build-dep for doc generation: graphviz, texlive-latex-recommended,

17 years ago - add build-dep for doc generation: graphviz, texlive-latex-base,
Stefano Zacchiroli [Mon, 16 Jul 2007 14:12:20 +0000 (14:12 +0000)]
  - add build-dep for doc generation: graphviz, texlive-latex-base,
    texlive-base-bin

17 years ago* debian/rules
Stefano Zacchiroli [Mon, 16 Jul 2007 14:09:23 +0000 (14:09 +0000)]
* debian/rules
  - build ocamldoc documentation at package build time
  - add build-dep on graphviz

17 years agoinvoke make doc after build to create ocamldoc docs
Stefano Zacchiroli [Mon, 16 Jul 2007 14:05:57 +0000 (14:05 +0000)]
invoke make doc after build to create ocamldoc docs

17 years ago* debian/svn-deblayout
Stefano Zacchiroli [Mon, 16 Jul 2007 13:59:36 +0000 (13:59 +0000)]
* debian/svn-deblayout
  - add repository layout information

17 years ago* rebuild against OCaml 3.10 and ocamlnet 2.2
Stefano Zacchiroli [Mon, 16 Jul 2007 13:56:27 +0000 (13:56 +0000)]
* 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

17 years ago* debian/*.install.in
Stefano Zacchiroli [Mon, 16 Jul 2007 13:49:22 +0000 (13:49 +0000)]
* debian/*.install.in
  - do not attempt to instal *.ml files in target lib directory since they
    are no longer installed by Makefile

17 years ago* rebuild with OCaml 3.10
Stefano Zacchiroli [Mon, 16 Jul 2007 13:31:55 +0000 (13:31 +0000)]
* rebuild with OCaml 3.10
* bump debhelper deps and compatibility level to 5
  - s/Source-Version/binary:Version

17 years agocorrected axiom mod_plus
Wilmer Ricciotti [Mon, 16 Jul 2007 13:07:53 +0000 (13:07 +0000)]
corrected axiom mod_plus

17 years agonew definitions and new theorems
Ferruccio Guidi [Sat, 14 Jul 2007 14:37:11 +0000 (14:37 +0000)]
new definitions and new theorems

17 years agoMore conjectures closed.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 22:04:05 +0000 (22:04 +0000)]
More conjectures closed.

17 years ago1. requires the new pretty printer for natural numbers
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 18:08:28 +0000 (18:08 +0000)]
1. requires the new pretty printer for natural numbers
2. important properties of plusbyte proved
3. all important conjectures almost proved

17 years agoDirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers...
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 18:04:35 +0000 (18:04 +0000)]
Dirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers. Eureka.

17 years agoLast crazy commit reverted.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 09:56:42 +0000 (09:56 +0000)]
Last crazy commit reverted.

17 years agoFinal theorem proved. Many many conjectures left. I am unsure of one of them.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 08:35:47 +0000 (08:35 +0000)]
Final theorem proved. Many many conjectures left. I am unsure of one of them.

17 years agoThe loop invariant I chosed was not correct!
Claudio Sacerdoti Coen [Thu, 12 Jul 2007 18:38:04 +0000 (18:38 +0000)]
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)

17 years agoGetting close to the final result.
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 17:10:26 +0000 (17:10 +0000)]
Getting close to the final result.
The showstopper now is the GtkMathView/Pango bug!
Moreover, unification has become mostly useless (and rewriting with it).

17 years ago1. loop invariant stated, but not proved
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 14:54:04 +0000 (14:54 +0000)]
1. loop invariant stated, but not proved
2. final theorem stated and proved

17 years agonative dependences fixed
Ferruccio Guidi [Wed, 11 Jul 2007 12:23:14 +0000 (12:23 +0000)]
native dependences fixed

17 years ago1. status factorized out in tick
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 10:52:49 +0000 (10:52 +0000)]
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!

17 years agoauto new => autobatch
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 09:16:43 +0000 (09:16 +0000)]
auto new => autobatch

17 years agoauto new => autobatch
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 09:11:18 +0000 (09:11 +0000)]
auto new => autobatch

17 years ago0. less nice solution by Enrico reverted
Claudio Sacerdoti Coen [Tue, 10 Jul 2007 22:06:50 +0000 (22:06 +0000)]
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

17 years agoNew reduction strategy: the new reduction strategy behaves as the previous
Claudio Sacerdoti Coen [Tue, 10 Jul 2007 18:48:14 +0000 (18:48 +0000)]
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.

17 years agoLa programmazione funzionale e' come TeX, funziona meglio se la prendi a calci.
Enrico Tassi [Tue, 10 Jul 2007 17:11:56 +0000 (17:11 +0000)]
La programmazione funzionale e' come TeX, funziona meglio se la prendi a calci.

17 years agopersistent inner types are now generated in publishing mode
Ferruccio Guidi [Tue, 10 Jul 2007 15:42:40 +0000 (15:42 +0000)]
persistent inner types are now generated in publishing mode

17 years agofixed a bug in the cleanup ofsedir that was not properly catching #xpointer
Enrico Tassi [Tue, 10 Jul 2007 15:15:33 +0000 (15:15 +0000)]
fixed a bug in the cleanup ofsedir that was not properly catching #xpointer

17 years ago...
Enrico Tassi [Tue, 10 Jul 2007 08:15:09 +0000 (08:15 +0000)]
...

17 years ago1. bug fixed in tick
Enrico Tassi [Mon, 9 Jul 2007 17:47:31 +0000 (17:47 +0000)]
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

17 years agosignal hadler restored after runnig external 'make'
Enrico Tassi [Mon, 9 Jul 2007 14:40:00 +0000 (14:40 +0000)]
signal hadler restored after runnig external 'make'

17 years agoInteresting theorem added (but still to be proved).
Claudio Sacerdoti Coen [Mon, 9 Jul 2007 14:34:57 +0000 (14:34 +0000)]
Interesting theorem added (but still to be proved).

17 years agoadded few more fun to this test
Enrico Tassi [Mon, 9 Jul 2007 13:32:17 +0000 (13:32 +0000)]
added few more fun to this test

17 years agonew configuration file sample
Ferruccio Guidi [Mon, 9 Jul 2007 13:04:18 +0000 (13:04 +0000)]
new configuration file sample

17 years agotassi: ported to the new DB architecture.
Ferruccio Guidi [Mon, 9 Jul 2007 13:01:25 +0000 (13:01 +0000)]
tassi: ported to the new DB architecture.
since the 'user' db is mandatory, a fake one should be provided

17 years agoauto->autobatch
Enrico Tassi [Mon, 9 Jul 2007 09:58:45 +0000 (09:58 +0000)]
auto->autobatch

17 years agoinclusion of div_and_mod
Enrico Tassi [Sat, 7 Jul 2007 11:34:18 +0000 (11:34 +0000)]
inclusion of div_and_mod

17 years agomaxipatch for support of multiple DBs.
Enrico Tassi [Fri, 6 Jul 2007 14:49:47 +0000 (14:49 +0000)]
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.