]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agothe tactic now returns as open goals the open metas in the proof
Enrico Tassi [Wed, 5 Apr 2006 12:07:51 +0000 (12:07 +0000)]
the tactic now returns as open goals the open metas in the proof
subsumption is now used correctly in given_clause_fullred

18 years agosubsumption fixed and called in given_clause_fullred.
Enrico Tassi [Wed, 5 Apr 2006 08:06:55 +0000 (08:06 +0000)]
subsumption fixed and called in given_clause_fullred.

18 years agoNaif substitution. Removed local context in metas during relocation.
Andrea Asperti [Tue, 4 Apr 2006 15:01:30 +0000 (15:01 +0000)]
Naif substitution. Removed local context in metas during relocation.
Removed apply_theorems in saturate, replaced by a local check for
identity.

18 years agoUseless code simplified out.
Claudio Sacerdoti Coen [Mon, 3 Apr 2006 13:12:21 +0000 (13:12 +0000)]
Useless code simplified out.

18 years agoNew benchmark after removal of some profiling code.
Claudio Sacerdoti Coen [Fri, 31 Mar 2006 11:02:29 +0000 (11:02 +0000)]
New benchmark after removal of some profiling code.

18 years agoLess profiling.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 16:40:50 +0000 (16:40 +0000)]
Less profiling.

18 years agoProfiling code for merge_ugraphs commented out (since profiling is much more
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 16:21:45 +0000 (16:21 +0000)]
Profiling code for merge_ugraphs commented out (since profiling is much more
expensive than the profiled code).

18 years agoA few benchmarks on the library of Coq committed.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 14:28:28 +0000 (14:28 +0000)]
A few benchmarks on the library of Coq committed.

18 years agoAdded deadline (now 30s) to each test.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 11:40:40 +0000 (11:40 +0000)]
Added deadline (now 30s) to each test.

18 years agoSys.Break used to be captured.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 11:15:52 +0000 (11:15 +0000)]
Sys.Break used to be captured.

18 years agoBug fixed: terms with a Cast used to raise assert false when whd was avoided
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 11:12:53 +0000 (11:12 +0000)]
Bug fixed: terms with a Cast used to raise assert false when whd was avoided
by the conversion strategy.

18 years agoHuge speed-up in conversion: the old conversion strategy is set back.
Claudio Sacerdoti Coen [Wed, 29 Mar 2006 16:26:32 +0000 (16:26 +0000)]
Huge speed-up in conversion: the old conversion strategy is set back.
 1. try to "convert" the two terms recursively without performing reduction
 2. if it fails, do a whd and try again
The overall result on the library of Coq is really remarkable.

18 years ago#### EXPERIMENTAL COMMIT ####
Claudio Sacerdoti Coen [Wed, 29 Mar 2006 14:44:00 +0000 (14:44 +0000)]
#### EXPERIMENTAL COMMIT ####
Added a potentially dangerous ~expand_beta_redexes flag to
CicSubstitution.subst. If used carefully, it enormously speeds up
the type-checking of many theorems (since a very frequent conversion test
happens between a beta-redex and its contractum).

18 years agoDebugging code added.
Claudio Sacerdoti Coen [Wed, 29 Mar 2006 13:34:55 +0000 (13:34 +0000)]
Debugging code added.

18 years agoremoved unif_ty ref
Enrico Tassi [Wed, 29 Mar 2006 12:18:56 +0000 (12:18 +0000)]
removed unif_ty ref

18 years agoreverted the addition of _ to mistyped names
Enrico Tassi [Wed, 29 Mar 2006 12:13:16 +0000 (12:13 +0000)]
reverted the addition of _ to mistyped names

18 years agofew bits to debug the benchmark system
Enrico Tassi [Wed, 29 Mar 2006 12:07:55 +0000 (12:07 +0000)]
few bits to debug the benchmark system

18 years agodeals with colors
Enrico Tassi [Tue, 28 Mar 2006 08:41:01 +0000 (08:41 +0000)]
deals with colors

18 years agomore profiling and fixes for paramod
Enrico Tassi [Tue, 28 Mar 2006 08:22:51 +0000 (08:22 +0000)]
more profiling and fixes for paramod

18 years agoargs removed from equalities.
Andrea Asperti [Mon, 27 Mar 2006 15:02:32 +0000 (15:02 +0000)]
args removed from equalities.
New selection strategy. De morgan: 253 s.

18 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 14:14:52 +0000 (14:14 +0000)]
Debugging code commented out.

18 years ago* trust = true
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 14:10:47 +0000 (14:10 +0000)]
* trust = true
* better pretty-printing of type-checking exceptions

18 years ago"Performance bug" fixed: I removed a whd in the does_not_occur function.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 14:01:26 +0000 (14:01 +0000)]
"Performance bug" fixed: I removed a whd in the does_not_occur function.
Consequences:
  1. incredible speed-up in the type-checking of certain inductive types
  2. "dummy" occurrences (i.e. occurrences that are doomed to disappear because
     of reduction) are now rejected (they used to be accepted). Coq has the
     same behaviour.

18 years agoSeveral "try ... with _ -> " specialized.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 12:21:48 +0000 (12:21 +0000)]
Several "try ... with _ -> " specialized.

18 years agoMore robust handling of Control-C.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 11:28:06 +0000 (11:28 +0000)]
More robust handling of Control-C.

18 years agoFlush stdout added in proper position.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 08:33:25 +0000 (08:33 +0000)]
Flush stdout added in proper position.

18 years agoignoring test_library{,.opt}
Stefano Zacchiroli [Fri, 24 Mar 2006 20:45:13 +0000 (20:45 +0000)]
ignoring test_library{,.opt}

18 years agoRecently introduced bug fixed in the kernel: a stack was "forgot" during
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 18:33:30 +0000 (18:33 +0000)]
Recently introduced bug fixed in the kernel: a stack was "forgot" during
reduction of a MutCase.

18 years agoUnable to parse my own output. Fixed.
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 18:02:18 +0000 (18:02 +0000)]
Unable to parse my own output. Fixed.

18 years ago% forgot in the output
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:57:58 +0000 (17:57 +0000)]
% forgot in the output

18 years agoSerious test for the Coq library added (name test_library).
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:56:35 +0000 (17:56 +0000)]
Serious test for the Coq library added (name test_library).
Input: a file that holds a list of URIs.
Output: the benchmark; the output file is also a valid input.
        In this case the output also prints the differences w.r.t. the
        last execution.
Ctrl-break can be used to interrupt the type-checking of a single URI.
An interactive question is posed to the user to decide if proceeding with
the next URIs or not.

18 years agomore error messages were on stdout :-(
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:54:21 +0000 (17:54 +0000)]
more error messages were on stdout :-(

18 years agoerror message was printed on stdout
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:52:05 +0000 (17:52 +0000)]
error message was printed on stdout

18 years agoColors are back! :-)
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 16:07:10 +0000 (16:07 +0000)]
Colors are back! :-)

18 years agoNew unification and new matching.
Andrea Asperti [Fri, 24 Mar 2006 16:01:08 +0000 (16:01 +0000)]
New unification and new matching.

18 years agoLegend for profiling printed iff something is profiled.
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 15:36:03 +0000 (15:36 +0000)]
Legend for profiling printed iff something is profiled.

18 years agofix
Enrico Tassi [Thu, 23 Mar 2006 11:12:15 +0000 (11:12 +0000)]
fix

18 years agofix
Enrico Tassi [Thu, 23 Mar 2006 10:49:30 +0000 (10:49 +0000)]
fix

18 years agoBest parameter setting for de morgan.
Andrea Asperti [Thu, 23 Mar 2006 10:33:41 +0000 (10:33 +0000)]
Best parameter setting for de morgan.
-- This line, and those below, will be ignored--

M    tactics/paramodulation/saturation.ml

18 years agofix
Enrico Tassi [Thu, 23 Mar 2006 09:06:06 +0000 (09:06 +0000)]
fix

18 years agoif DISTRIBUTED all targets require a depend-stamp
Enrico Tassi [Wed, 22 Mar 2006 14:29:21 +0000 (14:29 +0000)]
if DISTRIBUTED all targets require a depend-stamp

18 years ago:
Andrea Asperti [Wed, 22 Mar 2006 13:47:39 +0000 (13:47 +0000)]
:
This line, and those below, will be ignored--

M    tactics/paramodulation/utils.ml

18 years agoprofiler on steroids. added -profile-only to specify a regex to choose the profilings...
Enrico Tassi [Wed, 22 Mar 2006 12:27:01 +0000 (12:27 +0000)]
profiler on steroids. added -profile-only to specify a regex to choose the profilings to print

18 years agoremoved mysql_escape that should be ok.... but adds some \ that make mysql
Enrico Tassi [Wed, 22 Mar 2006 09:18:47 +0000 (09:18 +0000)]
removed mysql_escape that should be ok.... but adds some \ that make mysql
complain

18 years agoadded calls number
Enrico Tassi [Tue, 21 Mar 2006 17:40:53 +0000 (17:40 +0000)]
added calls number

18 years agoremoved mention of the "library" target, no longer needed for the installation
Stefano Zacchiroli [Tue, 21 Mar 2006 16:50:37 +0000 (16:50 +0000)]
removed mention of the "library" target, no longer needed for the installation

18 years agofixed timestamp issue on tactics.mli
Enrico Tassi [Tue, 21 Mar 2006 16:18:45 +0000 (16:18 +0000)]
fixed timestamp issue on tactics.mli

18 years agomock-up code for tactics contextual menu in the gui
Stefano Zacchiroli [Tue, 21 Mar 2006 15:21:28 +0000 (15:21 +0000)]
mock-up code for tactics contextual menu in the gui

18 years agoChanged the type of compute-equality_weight that now takes also
Andrea Asperti [Tue, 21 Mar 2006 15:11:34 +0000 (15:11 +0000)]
Changed the type of compute-equality_weight that now takes also
in input the ordering

18 years agogo
Enrico Tassi [Tue, 21 Mar 2006 14:01:53 +0000 (14:01 +0000)]
go

18 years agogo
Enrico Tassi [Tue, 21 Mar 2006 13:58:58 +0000 (13:58 +0000)]
go

18 years agogo
Enrico Tassi [Tue, 21 Mar 2006 13:47:26 +0000 (13:47 +0000)]
go

18 years agoadded raw query form
Enrico Tassi [Tue, 21 Mar 2006 13:39:27 +0000 (13:39 +0000)]
added raw query form

18 years agodone
Enrico Tassi [Tue, 21 Mar 2006 09:00:58 +0000 (09:00 +0000)]
done

18 years agofix
Enrico Tassi [Mon, 20 Mar 2006 16:39:57 +0000 (16:39 +0000)]
fix

18 years agoRenamed SK.ma into bool.ma
Andrea Asperti [Mon, 20 Mar 2006 16:32:32 +0000 (16:32 +0000)]
Renamed SK.ma into bool.ma

18 years agoEsempi di auto.
Andrea Asperti [Mon, 20 Mar 2006 16:31:08 +0000 (16:31 +0000)]
Esempi di auto.

18 years agoSnapshot.
Andrea Asperti [Mon, 20 Mar 2006 16:30:08 +0000 (16:30 +0000)]
Snapshot.

18 years agoremoved \t
Enrico Tassi [Mon, 20 Mar 2006 13:41:54 +0000 (13:41 +0000)]
removed \t

18 years agogo
Enrico Tassi [Fri, 17 Mar 2006 10:06:45 +0000 (10:06 +0000)]
go

18 years agogo
Enrico Tassi [Fri, 17 Mar 2006 10:04:13 +0000 (10:04 +0000)]
go

18 years agogo
Enrico Tassi [Fri, 17 Mar 2006 10:01:15 +0000 (10:01 +0000)]
go

18 years agofixed wrong log name
Enrico Tassi [Fri, 17 Mar 2006 09:51:48 +0000 (09:51 +0000)]
fixed wrong log name

18 years agoahh.....
Enrico Tassi [Fri, 17 Mar 2006 09:37:02 +0000 (09:37 +0000)]
ahh.....

18 years agotests are now handled with a standard Makefile that does not use do_tests.sh
Enrico Tassi [Fri, 17 Mar 2006 09:36:38 +0000 (09:36 +0000)]
tests are now handled with a standard Makefile that does not use do_tests.sh

18 years agoanother step roward the removal of do_tests.sh
Enrico Tassi [Thu, 16 Mar 2006 14:02:42 +0000 (14:02 +0000)]
another step roward the removal of do_tests.sh

18 years agoremoved php-shell scripts
Enrico Tassi [Thu, 16 Mar 2006 14:00:40 +0000 (14:00 +0000)]
removed php-shell scripts

18 years agomoved to the new table
Enrico Tassi [Thu, 16 Mar 2006 14:00:09 +0000 (14:00 +0000)]
moved to the new table

18 years agofix
Enrico Tassi [Thu, 16 Mar 2006 13:04:42 +0000 (13:04 +0000)]
fix

18 years agofixed a bug in the Makefile, generatedGui.mli no more there
Enrico Tassi [Thu, 16 Mar 2006 09:50:06 +0000 (09:50 +0000)]
fixed a bug in the Makefile, generatedGui.mli no more there

18 years agoone more step toward release and bench reorganization
Enrico Tassi [Thu, 16 Mar 2006 09:39:00 +0000 (09:39 +0000)]
one more step toward release and bench reorganization

18 years agofix
Enrico Tassi [Wed, 15 Mar 2006 15:54:16 +0000 (15:54 +0000)]
fix

18 years agomore work for the release
Enrico Tassi [Wed, 15 Mar 2006 15:51:25 +0000 (15:51 +0000)]
more work for the release

18 years agosnapshot for release
Enrico Tassi [Wed, 15 Mar 2006 11:27:02 +0000 (11:27 +0000)]
snapshot for release

18 years agoadded elp to distribution
Enrico Tassi [Tue, 14 Mar 2006 10:43:59 +0000 (10:43 +0000)]
added elp to distribution

18 years agoadded check to not clean the standard library, a confirmation is required
Enrico Tassi [Mon, 13 Mar 2006 12:48:17 +0000 (12:48 +0000)]
added check to not clean the standard library, a confirmation is required

18 years agoHuge commit for the release. Includes:
Enrico Tassi [Mon, 13 Mar 2006 12:20:25 +0000 (12:20 +0000)]
Huge commit for the release. Includes:
- getter_storage modifications to honor multiple (overlapping)
  ro/rw repositories
- removes of ~basedir
- addition of the 'publish' matitamake command used to install in system
  tables/directory a development (that is compiling with -system)
- removal of .build,.user,.devel config files (only one is needed)
- fixed make dist/install to strip binaries, install the library with the new
  method
- fixed compilation of the getter daemon
- deletion of grafite misc that is no more needed

18 years agoAdded inversion principle creation for inductive predicates.
marangon [Fri, 10 Mar 2006 12:59:53 +0000 (12:59 +0000)]
Added inversion principle creation for inductive predicates.

18 years agoInversion code cleaning.
marangon [Fri, 10 Mar 2006 12:20:41 +0000 (12:20 +0000)]
Inversion code cleaning.

18 years agouse the statusbar to display hyperlink targets
Stefano Zacchiroli [Wed, 8 Mar 2006 15:32:26 +0000 (15:32 +0000)]
use the statusbar to display hyperlink targets

18 years agoDebugging code removed.
Claudio Sacerdoti Coen [Wed, 8 Mar 2006 14:53:13 +0000 (14:53 +0000)]
Debugging code removed.

18 years agoReduction trick added to simplify (greatly speeding up some examples
Claudio Sacerdoti Coen [Wed, 8 Mar 2006 14:47:37 +0000 (14:47 +0000)]
Reduction trick added to simplify (greatly speeding up some examples
in library/algebra. For instance, a simplification that used to be performed
in more than 4h now takes less than 1s).

The idea is simply to avoid delta-reduction of a constant applied to
arguments that are not "active" (i.e. they cannot create a redex when
substituted in the body of the constant).

18 years agohand-like cursor when the cursor is on an href in a clickable math view
Stefano Zacchiroli [Tue, 7 Mar 2006 21:13:19 +0000 (21:13 +0000)]
hand-like cursor when the cursor is on an href in a clickable math view

18 years ago- added an hack to load sequents viewer's mathml from file
Stefano Zacchiroli [Tue, 7 Mar 2006 19:39:36 +0000 (19:39 +0000)]
- added an hack to load sequents viewer's mathml from file
- tried organizing entries of the debug menu

18 years agoThis simplify seems to diverge!
Claudio Sacerdoti Coen [Tue, 7 Mar 2006 18:21:39 +0000 (18:21 +0000)]
This simplify seems to diverge!

18 years agoFirst theorems proved on left cosets.
Claudio Sacerdoti Coen [Tue, 7 Mar 2006 17:31:09 +0000 (17:31 +0000)]
First theorems proved on left cosets.

18 years agoadded the creation of system_tables to the db when creating the user environment
Enrico Tassi [Tue, 7 Mar 2006 15:57:31 +0000 (15:57 +0000)]
added the creation of system_tables to the db when creating the user environment

18 years agoPP of Refine.RefineFailure.
marangon [Fri, 3 Mar 2006 17:12:41 +0000 (17:12 +0000)]
PP of Refine.RefineFailure.

18 years agoUse reference counting to keep track of camlp4 extensions so that the same
Stefano Zacchiroli [Fri, 24 Feb 2006 00:18:04 +0000 (00:18 +0000)]
Use reference counting to keep track of camlp4 extensions so that the same
grammar rules are not added several times. (closes: #147)

18 years agoadded a generic (yet rather trivial) module for reference counting
Stefano Zacchiroli [Fri, 24 Feb 2006 00:15:53 +0000 (00:15 +0000)]
added a generic (yet rather trivial) module for reference counting

18 years agobugfix: use utf8-aware substring function
Stefano Zacchiroli [Thu, 23 Feb 2006 22:30:23 +0000 (22:30 +0000)]
bugfix: use utf8-aware substring function

18 years agoadded "gragrep", grep-like tool over a bunch of grafite scripts
Stefano Zacchiroli [Thu, 23 Feb 2006 21:35:38 +0000 (21:35 +0000)]
added "gragrep", grep-like tool over a bunch of grafite scripts

18 years agoadded capability to specify externally extra command line arguments so that we
Stefano Zacchiroli [Thu, 23 Feb 2006 21:34:45 +0000 (21:34 +0000)]
added capability to specify externally extra command line arguments so that we
are no longer constrained to have all command line tools share the same command
line interface

18 years agoAdded module GrafiteWalker, which implements traversals (recursive and not) over
Stefano Zacchiroli [Thu, 23 Feb 2006 21:33:34 +0000 (21:33 +0000)]
Added module GrafiteWalker, which implements traversals (recursive and not) over
grafite scripts. Useful for grep/sed like operations over a bunch of scripts.

18 years agofactorized an ast_statement type which is (now) used from outside this module
Stefano Zacchiroli [Thu, 23 Feb 2006 21:32:24 +0000 (21:32 +0000)]
factorized an ast_statement type which is (now) used from outside this module

18 years ago- added src_root build time configuration value
Stefano Zacchiroli [Thu, 23 Feb 2006 21:31:23 +0000 (21:31 +0000)]
- added src_root build time configuration value
- added the disclaimer "ComponentsConf should not be here"

18 years agoinformation on current compilation state added in each file
Ferruccio Guidi [Thu, 23 Feb 2006 18:15:29 +0000 (18:15 +0000)]
information on current compilation state added in each file

18 years ago64 "change" here and there in the library are now simplify/unfold as they
Claudio Sacerdoti Coen [Thu, 23 Feb 2006 13:16:39 +0000 (13:16 +0000)]
64 "change" here and there in the library are now simplify/unfold as they
should have been. This has been possible because of some bugs fixed.

18 years agoDuring simplify, reduction of the argument of a Fix and of a MutCase is now
Claudio Sacerdoti Coen [Thu, 23 Feb 2006 13:13:04 +0000 (13:13 +0000)]
During simplify, reduction of the argument of a Fix and of a MutCase is now
performed using simplify. (It used to be performed by whd).
Pros: sometimes you should get simpler terms (but not so far)
Cons: sometimes simplification could simplify less than expected (but not so far)

18 years agoimproved comment of HExtlib.find
Stefano Zacchiroli [Wed, 22 Feb 2006 23:22:09 +0000 (23:22 +0000)]
improved comment of HExtlib.find