]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agoBug fixed in bottom-up conversion.
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:20:10 +0000 (12:20 +0000)]
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.

17 years agoBU Conversion was not generated for Rels fixed. I wonder why...
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:16:20 +0000 (12:16 +0000)]
BU Conversion was not generated for Rels fixed. I wonder why...

17 years agoNicer layout but possibly more bugged.
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:11:01 +0000 (12:11 +0000)]
Nicer layout but possibly more bugged.
We need continuations here to do a good job.

17 years agoSpurious "we need to prove" at the beginning of Intros+LetTac are no longer
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:10:09 +0000 (12:10 +0000)]
Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
generated.

17 years agogeneric version, specializing generic_sigma_p.ma
Cristian Armentano [Fri, 29 Jun 2007 16:30:31 +0000 (16:30 +0000)]
generic version, specializing generic_sigma_p.ma

17 years agogeneric version
Cristian Armentano [Fri, 29 Jun 2007 14:33:37 +0000 (14:33 +0000)]
generic version

17 years agotheorems about sigma_p proved using sigma_p_gen
Cristian Armentano [Fri, 29 Jun 2007 14:12:07 +0000 (14:12 +0000)]
theorems about sigma_p proved using sigma_p_gen

17 years agosvn:ignore property set
Ferruccio Guidi [Wed, 27 Jun 2007 20:59:41 +0000 (20:59 +0000)]
svn:ignore property set

17 years agonew gcd properties, and theorems for totient, and theorems for totient1
Cristian Armentano [Wed, 27 Jun 2007 18:05:37 +0000 (18:05 +0000)]
new gcd properties, and theorems for totient, and theorems for totient1

--this line, and those below, will be ignored--

M    minus.ma
M    le_arith.ma
M    lt_arith.ma
M    div_and_mod.ma
M    div_and_mod_new.ma
M    orders.ma
A    propr_div_mod_lt_le_totient1_aux.ma
A    gcd_properties1.ma

17 years agosome old auto yurned into autobatch
Ferruccio Guidi [Tue, 26 Jun 2007 17:58:16 +0000 (17:58 +0000)]
some old auto yurned into autobatch

17 years ago(no commit message)
Cristian Armentano [Tue, 26 Jun 2007 08:47:26 +0000 (08:47 +0000)]

17 years agogeneric sommatory.
Cristian Armentano [Tue, 26 Jun 2007 08:14:09 +0000 (08:14 +0000)]
generic sommatory.

17 years agoremoved ugly printings
Enrico Tassi [Sat, 23 Jun 2007 14:31:12 +0000 (14:31 +0000)]
removed ugly printings

17 years agoPoplMark challenge part 1a: new, shorter version w/o equivariance proofs.
Wilmer Ricciotti [Thu, 21 Jun 2007 16:33:15 +0000 (16:33 +0000)]
PoplMark challenge part 1a: new, shorter version w/o equivariance proofs.

17 years agobetter description
Enrico Tassi [Thu, 21 Jun 2007 14:45:04 +0000 (14:45 +0000)]
better description

17 years agobetter description
Enrico Tassi [Thu, 21 Jun 2007 13:09:44 +0000 (13:09 +0000)]
better description

17 years agohere we are, a version that compiles and seems to run
Enrico Tassi [Thu, 21 Jun 2007 12:38:34 +0000 (12:38 +0000)]
here we are, a version that compiles and seems to run

17 years agoIncompatible syntax problem between MySql e Sqlite3 fixed.
Claudio Sacerdoti Coen [Thu, 14 Jun 2007 11:07:45 +0000 (11:07 +0000)]
Incompatible syntax problem between MySql e Sqlite3 fixed.

17 years agocut is now implemented building a letin and not a beta redex
Enrico Tassi [Wed, 13 Jun 2007 13:09:20 +0000 (13:09 +0000)]
cut is now implemented building a letin and not a beta redex

17 years agomany changes:
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

17 years agosort_new_elems on prop_only
Enrico Tassi [Wed, 6 Jun 2007 17:12:39 +0000 (17:12 +0000)]
sort_new_elems on prop_only

17 years agofixed to allow make-dist
Enrico Tassi [Wed, 6 Jun 2007 13:52:49 +0000 (13:52 +0000)]
fixed to allow make-dist

17 years agoadded doc for compose
Enrico Tassi [Wed, 6 Jun 2007 09:07:33 +0000 (09:07 +0000)]
added doc for compose

17 years agocompose now returns a good metasenv
Enrico Tassi [Wed, 6 Jun 2007 08:35:33 +0000 (08:35 +0000)]
compose now returns a good metasenv

17 years agotentative fix
Enrico Tassi [Mon, 4 Jun 2007 16:06:10 +0000 (16:06 +0000)]
tentative fix

17 years agoAnother optimization, already done for geq.
Claudio Sacerdoti Coen [Mon, 4 Jun 2007 13:24:09 +0000 (13:24 +0000)]
Another optimization, already done for geq.

17 years agoauto proof are printed in procedural style
Enrico Tassi [Mon, 4 Jun 2007 13:02:02 +0000 (13:02 +0000)]
auto proof are printed in procedural style

17 years agonew more flexible compose, see matita/tests/compose.ma for a sample
Enrico Tassi [Mon, 4 Jun 2007 12:20:18 +0000 (12:20 +0000)]
new more flexible compose, see matita/tests/compose.ma for a sample

17 years agowrong assertion was inserted, now just a warning to know when it happens
Enrico Tassi [Sat, 2 Jun 2007 09:38:35 +0000 (09:38 +0000)]
wrong assertion was inserted, now just a warning to know when it happens

17 years agoSome interesting optimizations to prevent many bad checks.
Claudio Sacerdoti Coen [Fri, 1 Jun 2007 22:08:43 +0000 (22:08 +0000)]
Some interesting optimizations to prevent many bad checks.

17 years agoProfiling enabled again.
Claudio Sacerdoti Coen [Fri, 1 Jun 2007 19:32:06 +0000 (19:32 +0000)]
Profiling enabled again.

17 years agoremoved some refinement_toolkit
Enrico Tassi [Fri, 1 Jun 2007 15:05:06 +0000 (15:05 +0000)]
removed some refinement_toolkit

17 years agonew compose tactic, still undocumented.
Enrico Tassi [Fri, 1 Jun 2007 14:58:50 +0000 (14:58 +0000)]
new compose tactic, still undocumented.
moved from library to tactics the code for composing coercions.

17 years agoI do not know why, but
Claudio Sacerdoti Coen [Fri, 1 Jun 2007 13:20:21 +0000 (13:20 +0000)]
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!

17 years agohacks for paramodulation declarative proofs
Enrico Tassi [Fri, 1 Jun 2007 07:35:59 +0000 (07:35 +0000)]
hacks for paramodulation declarative proofs

17 years agoFinal (???) bug fixed.
Claudio Sacerdoti Coen [Thu, 31 May 2007 18:04:22 +0000 (18:04 +0000)]
Final (???) bug fixed.
The fixpoint for n=1 is now reached in 22s.

17 years agoDOOMSDAY 1.0:
Claudio Sacerdoti Coen [Thu, 31 May 2007 15:06:22 +0000 (15:06 +0000)]
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.

17 years agoBug fixed: wrong id.
Claudio Sacerdoti Coen [Thu, 31 May 2007 15:02:52 +0000 (15:02 +0000)]
Bug fixed: wrong id.

17 years agoFerruccio has changed the semantics of the old ~pattern argument of elim_tac.
Claudio Sacerdoti Coen [Thu, 31 May 2007 15:02:14 +0000 (15:02 +0000)]
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.

17 years agoMore exceptions pretty-printed.
Claudio Sacerdoti Coen [Thu, 31 May 2007 14:57:52 +0000 (14:57 +0000)]
More exceptions pretty-printed.

17 years agotheory_explorer now communicates directly with matitawiki.opt.
Claudio Sacerdoti Coen [Wed, 30 May 2007 18:05:53 +0000 (18:05 +0000)]
theory_explorer now communicates directly with matitawiki.opt.
Overall time to reach the fixpoint for m=1 changed from 91m to 11m!!!

17 years agonow the window can be closed also using X
Enrico Tassi [Wed, 30 May 2007 08:33:54 +0000 (08:33 +0000)]
now the window can be closed also using X

17 years ago1. Profiling enabled.
Claudio Sacerdoti Coen [Tue, 29 May 2007 17:29:19 +0000 (17:29 +0000)]
1. Profiling enabled.
2. Dotfile inserted into log.ma for debugging pourposes.

17 years agohSqlite3.ml used create_fun_2 to define REGEXP.
Enrico Tassi [Tue, 29 May 2007 16:22:49 +0000 (16:22 +0000)]
hSqlite3.ml used create_fun_2 to define REGEXP.
this functions is not official, patch sent upstream

17 years agoadded some lines to compile for debugging
Enrico Tassi [Tue, 29 May 2007 15:30:53 +0000 (15:30 +0000)]
added some lines to compile for debugging

17 years agoadded pruning option in autogui
Enrico Tassi [Tue, 29 May 2007 11:03:51 +0000 (11:03 +0000)]
added pruning option in autogui

17 years agoCorrected version od meta_convertibnility_subst.
Andrea Asperti [Tue, 29 May 2007 09:26:02 +0000 (09:26 +0000)]
Corrected version od meta_convertibnility_subst.

17 years agoBug fixed (hopefully without introducing new ones): when the user clicked in
Claudio Sacerdoti Coen [Mon, 28 May 2007 17:16:43 +0000 (17:16 +0000)]
Bug fixed (hopefully without introducing new ones): when the user clicked in
AutoWin on a theorem that does not generate new goals, the hint was never
found and auto "immediately" failed.

17 years agoImproved pruning (no propress).
Andrea Asperti [Mon, 28 May 2007 13:20:33 +0000 (13:20 +0000)]
Improved pruning (no propress).

17 years agoAdded a new version of meta_convertibnility that returns the
Andrea Asperti [Mon, 28 May 2007 13:18:32 +0000 (13:18 +0000)]
Added a new version of meta_convertibnility that returns the
variant substitution.

17 years ago1. Now I save a log.ma file that is exactly what is proved!
Claudio Sacerdoti Coen [Sat, 26 May 2007 23:19:47 +0000 (23:19 +0000)]
1. Now I save a log.ma file that is exactly what is proved!
2. Only three arcs missing in 61s (with a low depth) :-|

17 years agolog.ma is now created. But it does not contain the exact sequence of things
Claudio Sacerdoti Coen [Sat, 26 May 2007 15:48:12 +0000 (15:48 +0000)]
log.ma is now created. But it does not contain the exact sequence of things
proved by auto.
width=2 does not seem to hurt!
the graph is now really acyclic (I swear).

17 years agolog.ma is now created. It records all the tests (both failure and successes).
Claudio Sacerdoti Coen [Fri, 25 May 2007 17:52:39 +0000 (17:52 +0000)]
log.ma is now created. It records all the tests (both failure and successes).

17 years agoYet another assert failure fixed.
Claudio Sacerdoti Coen [Fri, 25 May 2007 09:57:34 +0000 (09:57 +0000)]
Yet another assert failure fixed.

17 years agoMore warnings.
Claudio Sacerdoti Coen [Fri, 25 May 2007 09:31:46 +0000 (09:31 +0000)]
More warnings.
More bugs detected by warnings fixed.
auto => autobatch.

17 years agoadded $Revision$
Enrico Tassi [Fri, 25 May 2007 09:10:00 +0000 (09:10 +0000)]
added $Revision$

17 years agoauto --> autobatch
Enrico Tassi [Fri, 25 May 2007 08:27:39 +0000 (08:27 +0000)]
auto --> autobatch

17 years agoauto --> autobatch
Enrico Tassi [Fri, 25 May 2007 08:17:37 +0000 (08:17 +0000)]
auto --> autobatch

17 years agoNew asserts.
Claudio Sacerdoti Coen [Thu, 24 May 2007 16:37:41 +0000 (16:37 +0000)]
New asserts.
Saner invariant: a not-yet-located node is now put both in the inf and sup
lists.

17 years agoauto and autogui... some work
Enrico Tassi [Thu, 24 May 2007 15:54:36 +0000 (15:54 +0000)]
auto and autogui... some work

17 years agoauto and autogui... some work
Enrico Tassi [Thu, 24 May 2007 15:54:08 +0000 (15:54 +0000)]
auto and autogui... some work

17 years agofixed a when that was causing backtrace loss
Enrico Tassi [Thu, 24 May 2007 15:53:33 +0000 (15:53 +0000)]
fixed a when that was causing backtrace loss

17 years agoMore assert failures and some bugs (detected by assert failure) fixed.
Claudio Sacerdoti Coen [Thu, 24 May 2007 15:53:29 +0000 (15:53 +0000)]
More assert failures and some bugs (detected by assert failure) fixed.

17 years agoadded some flags to render subproofs (an hack)
Enrico Tassi [Thu, 24 May 2007 15:52:48 +0000 (15:52 +0000)]
added some flags to render subproofs (an hack)

17 years agoAll known bugs fixed.
Claudio Sacerdoti Coen [Thu, 24 May 2007 13:52:29 +0000 (13:52 +0000)]
All known bugs fixed.
Compilation is now in nativecode.

17 years agoIt no longer generates double arcs between nodes.
Claudio Sacerdoti Coen [Thu, 24 May 2007 13:07:34 +0000 (13:07 +0000)]
It no longer generates double arcs between nodes.
Bug: it does not put ii in the same equivalence class as i.

17 years agoStill bugged.
Claudio Sacerdoti Coen [Thu, 24 May 2007 12:43:28 +0000 (12:43 +0000)]
Still bugged.

17 years agotheory_explorer_do_not_trust_auto.ml is the version that does not trust
Claudio Sacerdoti Coen [Thu, 24 May 2007 10:56:33 +0000 (10:56 +0000)]
theory_explorer_do_not_trust_auto.ml is the version that does not trust
 auto. The algorithm is exponential.

theory_explorer.ml trusts auto and requires only quadratic time. Not working
 properly yet.

17 years agoI am now using tred to remove transitive dependencies from the graph before
Claudio Sacerdoti Coen [Wed, 23 May 2007 17:48:21 +0000 (17:48 +0000)]
I am now using tred to remove transitive dependencies from the graph before
displaying it.

17 years ago1. generation of log file commented out (it gets too big too early)
Claudio Sacerdoti Coen [Wed, 23 May 2007 17:33:24 +0000 (17:33 +0000)]
1. generation of log file commented out (it gets too big too early)
2. bug fixed in highlighting of the red node

17 years agoYet another patch to LibraryClean.
Claudio Sacerdoti Coen [Wed, 23 May 2007 16:19:35 +0000 (16:19 +0000)]
Yet another patch to LibraryClean.
Now we look for URIs to remove both in the filesystem and in the objectName
table of the DB.

17 years agoHSql.Error ==> HSql.Error of string
Claudio Sacerdoti Coen [Wed, 23 May 2007 15:58:53 +0000 (15:58 +0000)]
HSql.Error ==> HSql.Error of string

17 years agoprerr_endine ==> debug_print everywhere
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:58:59 +0000 (14:58 +0000)]
prerr_endine ==> debug_print everywhere

17 years agoReindented.
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:57:20 +0000 (14:57 +0000)]
Reindented.

17 years agoEven more color (for new nodes).
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:30:42 +0000 (14:30 +0000)]
Even more color (for new nodes).

17 years agodeps fixed
Enrico Tassi [Wed, 23 May 2007 14:29:40 +0000 (14:29 +0000)]
deps fixed

17 years agoUse different colors to understand what is going on.
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:25:29 +0000 (14:25 +0000)]
Use different colors to understand what is going on.

17 years agomakefile reworked to make debian package possible
Enrico Tassi [Wed, 23 May 2007 14:13:22 +0000 (14:13 +0000)]
makefile reworked to make debian package possible

17 years agoUnlinked nodes are now printed.
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:13:17 +0000 (14:13 +0000)]
Unlinked nodes are now printed.
The algorithm works only if - is considered immediately. Fixed.

17 years agomade matita.runtime_base_dir overridable setting MATITA_RUNTIME_BASE_DIR env variable
Enrico Tassi [Wed, 23 May 2007 14:09:35 +0000 (14:09 +0000)]
made matita.runtime_base_dir overridable setting MATITA_RUNTIME_BASE_DIR env variable

17 years agoMATITA_* env variable preserved when publishing a development
Enrico Tassi [Wed, 23 May 2007 14:08:27 +0000 (14:08 +0000)]
MATITA_* env variable preserved when publishing a development

17 years agochanged the way environment variable can interfere with the registry.
Enrico Tassi [Wed, 23 May 2007 14:07:24 +0000 (14:07 +0000)]
changed the way environment variable can interfere with the registry.

17 years agoadded is_writabledir to extlib
Enrico Tassi [Wed, 23 May 2007 14:05:40 +0000 (14:05 +0000)]
added is_writabledir to extlib

17 years agoadded some hacks for the debian package
Enrico Tassi [Wed, 23 May 2007 14:05:15 +0000 (14:05 +0000)]
added some hacks for the debian package

17 years agodebian package for matita
Enrico Tassi [Wed, 23 May 2007 14:04:08 +0000 (14:04 +0000)]
debian package for matita

17 years agoxxx.dot improved
Claudio Sacerdoti Coen [Wed, 23 May 2007 13:36:39 +0000 (13:36 +0000)]
xxx.dot improved

17 years agoAutomatic exploration of the theory of intuitionistic interior, closure and
Claudio Sacerdoti Coen [Wed, 23 May 2007 13:28:22 +0000 (13:28 +0000)]
Automatic exploration of the theory of intuitionistic interior, closure and
complement.

17 years agoSlightly more efficient patch.
Claudio Sacerdoti Coen [Tue, 22 May 2007 14:39:12 +0000 (14:39 +0000)]
Slightly more efficient patch.

17 years agoapplyTransformation: added debugging information
Ferruccio Guidi [Sun, 20 May 2007 10:41:12 +0000 (10:41 +0000)]
applyTransformation: added debugging information
makefiles: %.mo.opt now working
developments.txt: added Base-2 devel
acic_procedural: some improvements
 new optimization: atomic let-ins are now expanded

17 years ago- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated
Ferruccio Guidi [Fri, 18 May 2007 15:55:49 +0000 (15:55 +0000)]
- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated
  procedural representation of the proofs in contribs/LAMBDA-TYPES/Base-1
- template_makefile_devel.in: %.mo.opt now works
- acic_procedural: some improvements
- PrimitiveTactics: a part of the elim tactic was factorixed for use by the
  procedural reconstruction

17 years agoadded alternative implementation for hMysql relying
lzingare [Fri, 18 May 2007 14:45:00 +0000 (14:45 +0000)]
added alternative implementation for hMysql relying
on sqlite3.

17 years agoIn some cases (e.g. JM equality) the inversion principle is not generated
Claudio Sacerdoti Coen [Fri, 18 May 2007 13:34:45 +0000 (13:34 +0000)]
In some cases (e.g. JM equality) the inversion principle is not generated
because CicRefine cannot infer a dependetly enough type. Now a warning is
raised and compilation is not stopped.

17 years agoadded a (for the moment) dummy field _subst to ProofengineTypes.proof.
Enrico Tassi [Thu, 17 May 2007 17:22:37 +0000 (17:22 +0000)]
added a (for the moment) dummy field _subst to ProofengineTypes.proof.
36 file touched ;-)

17 years agoauto rewritten with only one tail recursive function.
Enrico Tassi [Thu, 17 May 2007 15:45:59 +0000 (15:45 +0000)]
auto rewritten with only one tail recursive function.
this allows to have a GUI to drive the procedure.
a new measure size has been added, and width changed its meaning.
a bunch of unfold lt added to library_auto.

17 years agoOPT tests restored
Enrico Tassi [Thu, 17 May 2007 15:17:39 +0000 (15:17 +0000)]
OPT tests restored

17 years agomore informations on nodes, fixed a bug on conversion, we use ; instead of . whenever...
Ferruccio Guidi [Tue, 15 May 2007 17:08:57 +0000 (17:08 +0000)]
more informations on nodes, fixed a bug on conversion, we use ; instead of . whenever possible in rendering

17 years agoWrong invariant: Hypothesis (i.e. lambda-abstractions) can have no
Ferruccio Guidi [Tue, 15 May 2007 11:29:36 +0000 (11:29 +0000)]
Wrong invariant: Hypothesis (i.e. lambda-abstractions) can have no
(= None) name (if unusable).

17 years agoCSC: terrific bug fixed. Enrico commented the application of eta_fix to the body
Ferruccio Guidi [Mon, 14 May 2007 16:37:18 +0000 (16:37 +0000)]
CSC: terrific bug fixed. Enrico commented the application of eta_fix to the body
of a constant, without replacing it with Unshare.unshare (that is done inside
eta_fix). To avoid the bug to happear again, I have renamed eta_fix in
eta_fix_and_unshare.

17 years agolibrary-auto removed from tests (too slow even in native code)
Ferruccio Guidi [Sun, 13 May 2007 20:25:44 +0000 (20:25 +0000)]
library-auto removed from tests (too slow even in native code)

17 years agoCicInspect: a function for counting the nodes of a term has been activated
Ferruccio Guidi [Sun, 13 May 2007 12:59:43 +0000 (12:59 +0000)]
CicInspect: a function for counting the nodes of a term has been activated
Procedural: reports on node counting in proof terms are aveilable