]>
matita.cs.unibo.it Git - helm.git/log
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.
Claudio Sacerdoti Coen [Thu, 31 May 2007 14:57:52 +0000 (14:57 +0000)]
More exceptions pretty-printed.
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!!!
Enrico Tassi [Wed, 30 May 2007 08:33:54 +0000 (08:33 +0000)]
now the window can be closed also using X
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.
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
Enrico Tassi [Tue, 29 May 2007 15:30:53 +0000 (15:30 +0000)]
added some lines to compile for debugging
Enrico Tassi [Tue, 29 May 2007 11:03:51 +0000 (11:03 +0000)]
added pruning option in autogui
Andrea Asperti [Tue, 29 May 2007 09:26:02 +0000 (09:26 +0000)]
Corrected version od meta_convertibnility_subst.
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.
Andrea Asperti [Mon, 28 May 2007 13:20:33 +0000 (13:20 +0000)]
Improved pruning (no propress).
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.
Stefano Zacchiroli [Mon, 28 May 2007 09:22:25 +0000 (09:22 +0000)]
removed spurious br
Stefano Zacchiroli [Mon, 28 May 2007 09:09:07 +0000 (09:09 +0000)]
added abstract toggling
Stefano Zacchiroli [Mon, 28 May 2007 09:01:38 +0000 (09:01 +0000)]
added missing PDFs and spurious error papers
Enrico Tassi [Mon, 28 May 2007 08:52:07 +0000 (08:52 +0000)]
aded papers
Enrico Tassi [Mon, 28 May 2007 08:49:18 +0000 (08:49 +0000)]
...
Enrico Tassi [Mon, 28 May 2007 08:46:11 +0000 (08:46 +0000)]
...
Enrico Tassi [Mon, 28 May 2007 08:38:05 +0000 (08:38 +0000)]
...
Enrico Tassi [Mon, 28 May 2007 08:18:41 +0000 (08:18 +0000)]
...
Enrico Tassi [Mon, 28 May 2007 08:18:27 +0000 (08:18 +0000)]
more local modifications
Enrico Tassi [Mon, 28 May 2007 08:13:23 +0000 (08:13 +0000)]
local modifications
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) :-|
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).
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).
Claudio Sacerdoti Coen [Fri, 25 May 2007 09:57:34 +0000 (09:57 +0000)]
Yet another assert failure fixed.
Claudio Sacerdoti Coen [Fri, 25 May 2007 09:31:46 +0000 (09:31 +0000)]
More warnings.
More bugs detected by warnings fixed.
auto => autobatch.
Enrico Tassi [Fri, 25 May 2007 09:10:00 +0000 (09:10 +0000)]
added $Revision$
Enrico Tassi [Fri, 25 May 2007 08:27:39 +0000 (08:27 +0000)]
auto --> autobatch
Enrico Tassi [Fri, 25 May 2007 08:17:37 +0000 (08:17 +0000)]
auto --> autobatch
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.
Enrico Tassi [Thu, 24 May 2007 15:54:36 +0000 (15:54 +0000)]
auto and autogui... some work
Enrico Tassi [Thu, 24 May 2007 15:54:08 +0000 (15:54 +0000)]
auto and autogui... some work
Enrico Tassi [Thu, 24 May 2007 15:53:33 +0000 (15:53 +0000)]
fixed a when that was causing backtrace loss
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.
Enrico Tassi [Thu, 24 May 2007 15:52:48 +0000 (15:52 +0000)]
added some flags to render subproofs (an hack)
Claudio Sacerdoti Coen [Thu, 24 May 2007 13:52:29 +0000 (13:52 +0000)]
All known bugs fixed.
Compilation is now in nativecode.
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.
Claudio Sacerdoti Coen [Thu, 24 May 2007 12:43:28 +0000 (12:43 +0000)]
Still bugged.
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.
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.
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
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.
Claudio Sacerdoti Coen [Wed, 23 May 2007 15:58:53 +0000 (15:58 +0000)]
HSql.Error ==> HSql.Error of string
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:58:59 +0000 (14:58 +0000)]
prerr_endine ==> debug_print everywhere
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:57:20 +0000 (14:57 +0000)]
Reindented.
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:30:42 +0000 (14:30 +0000)]
Even more color (for new nodes).
Enrico Tassi [Wed, 23 May 2007 14:29:40 +0000 (14:29 +0000)]
deps fixed
Claudio Sacerdoti Coen [Wed, 23 May 2007 14:25:29 +0000 (14:25 +0000)]
Use different colors to understand what is going on.
Enrico Tassi [Wed, 23 May 2007 14:13:22 +0000 (14:13 +0000)]
makefile reworked to make debian package possible
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.
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
Enrico Tassi [Wed, 23 May 2007 14:08:27 +0000 (14:08 +0000)]
MATITA_* env variable preserved when publishing a development
Enrico Tassi [Wed, 23 May 2007 14:07:24 +0000 (14:07 +0000)]
changed the way environment variable can interfere with the registry.
Enrico Tassi [Wed, 23 May 2007 14:05:40 +0000 (14:05 +0000)]
added is_writabledir to extlib
Enrico Tassi [Wed, 23 May 2007 14:05:15 +0000 (14:05 +0000)]
added some hacks for the debian package
Enrico Tassi [Wed, 23 May 2007 14:04:08 +0000 (14:04 +0000)]
debian package for matita
Claudio Sacerdoti Coen [Wed, 23 May 2007 13:36:39 +0000 (13:36 +0000)]
xxx.dot improved
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.
Claudio Sacerdoti Coen [Tue, 22 May 2007 14:39:12 +0000 (14:39 +0000)]
Slightly more efficient patch.
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
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
lzingare [Fri, 18 May 2007 14:45:00 +0000 (14:45 +0000)]
added alternative implementation for hMysql relying
on sqlite3.
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.
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 ;-)
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.
Enrico Tassi [Thu, 17 May 2007 15:17:39 +0000 (15:17 +0000)]
OPT tests restored
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
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).
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.
Ferruccio Guidi [Sun, 13 May 2007 20:25:44 +0000 (20:25 +0000)]
library-auto removed from tests (too slow even in native code)
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
Ferruccio Guidi [Thu, 10 May 2007 12:59:52 +0000 (12:59 +0000)]
Procedural: clear tactics added
Ferruccio Guidi [Wed, 9 May 2007 19:36:00 +0000 (19:36 +0000)]
PrimitiveTactics: intros _ now aveilable
GrafiteAst : some refactoring
Andrea Asperti [Wed, 9 May 2007 10:55:32 +0000 (10:55 +0000)]
A few extensions for the moebius inversion theorem
Andrea Asperti [Wed, 9 May 2007 10:53:28 +0000 (10:53 +0000)]
Proof of the moebius inversion theorem
Ferruccio Guidi [Tue, 8 May 2007 19:04:10 +0000 (19:04 +0000)]
DoubleTypeInference: added a comment on "does_not_occur"
GrafiteAstPp: rendering of clear tactic fixed
Enrico Tassi [Mon, 7 May 2007 13:36:14 +0000 (13:36 +0000)]
...
Enrico Tassi [Mon, 7 May 2007 11:38:56 +0000 (11:38 +0000)]
a bit of sharing and the optimization of not folding trough the metasenv if the to_be_restrincted list is empty
Enrico Tassi [Mon, 7 May 2007 11:37:10 +0000 (11:37 +0000)]
some minor fixes done in cividale (bugfix coming from andrea's branch)
Ferruccio Guidi [Thu, 3 May 2007 17:17:40 +0000 (17:17 +0000)]
elim with a pattern now works correctly (hopefully)
Ferruccio Guidi [Thu, 3 May 2007 12:09:48 +0000 (12:09 +0000)]
library-auto is only tested in native code (in byte code it's too slow)
Ferruccio Guidi [Wed, 2 May 2007 09:53:20 +0000 (09:53 +0000)]
some improvements
Ferruccio Guidi [Tue, 1 May 2007 16:15:58 +0000 (16:15 +0000)]
SubstTactic: bug fix
RELATIONAL : some improvements on integers
Andrea Asperti [Mon, 30 Apr 2007 10:51:14 +0000 (10:51 +0000)]
Even if we are at depth 0, we first check in the cache for a solution,
before failing. In the other case the assert false at line 76 of
autocache may fail.
Andrea Asperti [Mon, 30 Apr 2007 10:31:15 +0000 (10:31 +0000)]
Removed an assert false; everything works again, but something
is clearly wrong (to be fixed).
Ferruccio Guidi [Sun, 29 Apr 2007 15:41:14 +0000 (15:41 +0000)]
GrafiteAstPp: \n's finally fixed
acic_procedural:
- elimination patterns are generated correctly
- comments on elimination cases added
Ferruccio Guidi [Sat, 28 Apr 2007 12:17:50 +0000 (12:17 +0000)]
AMBDA-TYPES: some improvements. subst now fully exploited
developments.txt: added library_auto
RELATIONAL: some improvements. subst now fully exploited
cic_procedural: a List.rev was missing :-p
substTactic: tacticals are now exploited properly
Ferruccio Guidi [Fri, 27 Apr 2007 19:08:54 +0000 (19:08 +0000)]
LAMBDA-TYPES: some improvements
Andrea Asperti [Fri, 27 Apr 2007 14:00:24 +0000 (14:00 +0000)]
Subst is passed in input to apapluy, so no need to concatenate the results
Andrea Asperti [Fri, 27 Apr 2007 13:46:36 +0000 (13:46 +0000)]
Apply_with_subst now returns a subst with a correct type for the meta.
Ferruccio Guidi [Thu, 26 Apr 2007 19:06:42 +0000 (19:06 +0000)]
procedural: bug fixes
matita: some \n rearranged
GrafiteAstPp: some \n rearranged
GrafiteParser: added callback
Ferruccio Guidi [Thu, 26 Apr 2007 13:05:48 +0000 (13:05 +0000)]
bug fix in subst tactic
Claudio Sacerdoti Coen [Tue, 24 Apr 2007 15:06:19 +0000 (15:06 +0000)]
goal ==> focus
Andrea Asperti [Tue, 24 Apr 2007 13:54:10 +0000 (13:54 +0000)]
Subsumption_subst re-added to initial.
Andrea Asperti [Tue, 24 Apr 2007 13:42:00 +0000 (13:42 +0000)]
@
Claudio Sacerdoti Coen [Mon, 23 Apr 2007 13:40:00 +0000 (13:40 +0000)]
Deprecated "goal" removed.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 15:39:16 +0000 (15:39 +0000)]
A new test on some non punctuation tacticals.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 15:33:27 +0000 (15:33 +0000)]
The declarative rewriting step now tries auto timeout=3 before
auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:47:25 +0000 (14:47 +0000)]
added skip, removed end