]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

17 years agoProcedural: clear tactics added
Ferruccio Guidi [Thu, 10 May 2007 12:59:52 +0000 (12:59 +0000)]
Procedural: clear tactics added

17 years agoPrimitiveTactics: intros _ now aveilable
Ferruccio Guidi [Wed, 9 May 2007 19:36:00 +0000 (19:36 +0000)]
PrimitiveTactics: intros _ now aveilable
GrafiteAst      : some refactoring

17 years agoA few extensions for the moebius inversion theorem
Andrea Asperti [Wed, 9 May 2007 10:55:32 +0000 (10:55 +0000)]
A few extensions for the moebius inversion theorem

17 years agoProof of the moebius inversion theorem
Andrea Asperti [Wed, 9 May 2007 10:53:28 +0000 (10:53 +0000)]
Proof of the moebius inversion theorem

17 years agoDoubleTypeInference: added a comment on "does_not_occur"
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

17 years ago...
Enrico Tassi [Mon, 7 May 2007 13:36:14 +0000 (13:36 +0000)]
...

17 years agoa bit of sharing and the optimization of not folding trough the metasenv if the to_be...
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

17 years agosome minor fixes done in cividale (bugfix coming from andrea's branch)
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)

17 years agoelim with a pattern now works correctly (hopefully)
Ferruccio Guidi [Thu, 3 May 2007 17:17:40 +0000 (17:17 +0000)]
elim with a pattern now works correctly (hopefully)

17 years agolibrary-auto is only tested in native code (in byte code it's too slow)
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)

17 years agosome improvements
Ferruccio Guidi [Wed, 2 May 2007 09:53:20 +0000 (09:53 +0000)]
some improvements

17 years agoSubstTactic: bug fix
Ferruccio Guidi [Tue, 1 May 2007 16:15:58 +0000 (16:15 +0000)]
SubstTactic: bug fix
RELATIONAL : some improvements on integers

17 years agoEven if we are at depth 0, we first check in the cache for a solution,
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.

17 years agoRemoved an assert false; everything works again, but something
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).

17 years agoGrafiteAstPp: \n's finally 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

17 years agoAMBDA-TYPES: some improvements. subst now fully exploited
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

17 years agoLAMBDA-TYPES: some improvements
Ferruccio Guidi [Fri, 27 Apr 2007 19:08:54 +0000 (19:08 +0000)]
LAMBDA-TYPES: some improvements

17 years agoSubst is passed in input to apapluy, so no need to concatenate the results
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

17 years agoApply_with_subst now returns a subst with a correct type for the meta.
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.

17 years agoprocedural: bug fixes
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

17 years agobug fix in subst tactic
Ferruccio Guidi [Thu, 26 Apr 2007 13:05:48 +0000 (13:05 +0000)]
bug fix in subst tactic

17 years agogoal ==> focus
Claudio Sacerdoti Coen [Tue, 24 Apr 2007 15:06:19 +0000 (15:06 +0000)]
goal ==> focus

17 years agoSubsumption_subst re-added to initial.
Andrea Asperti [Tue, 24 Apr 2007 13:54:10 +0000 (13:54 +0000)]
Subsumption_subst re-added to initial.

17 years ago@
Andrea Asperti [Tue, 24 Apr 2007 13:42:00 +0000 (13:42 +0000)]
@

17 years agoDeprecated "goal" removed.
Claudio Sacerdoti Coen [Mon, 23 Apr 2007 13:40:00 +0000 (13:40 +0000)]
Deprecated "goal" removed.

17 years agoA new test on some non punctuation tacticals.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 15:39:16 +0000 (15:39 +0000)]
A new test on some non punctuation tacticals.

17 years agoThe declarative rewriting step now tries auto timeout=3 before
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.

17 years agoadded skip, removed end
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:47:25 +0000 (14:47 +0000)]
added skip, removed end

17 years agoMuch ado about nothing:
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:46:36 +0000 (14:46 +0000)]
Much ado about nothing:
 1) repeat tac end ==> repeat tac
 2) do n tac end   ==> do n tac
 3) "goal n" finally dropped (deprecated, semantics no longer clear)
 4) the AST (in grafiteAst) has been changed to better reflect the
    distinction between tactics (including h.o. tactics, i.e. tacticals),
    punctuational tinycals and non punctuation tinycals (i.e. skip, focus,
    unfocus)
 5) all tacticals are now running properly in every condition;
    but tacticals argument (i.e. tactics occurring in tacticals) are
    disambiguated eagerly and not lazily (to be changed)

WARNING: the code in proceduralTypes.ml has been commented out since I am
not able to figure out how to fix it properly

17 years agoBug fixed: off by one array access in the last patch.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:31:25 +0000 (14:31 +0000)]
Bug fixed: off by one array access in the last patch.

17 years agodevelopments root are now part of default inclusion paths;
Enrico Tassi [Fri, 20 Apr 2007 13:30:16 +0000 (13:30 +0000)]
developments root are now part of default inclusion paths;
incluson path used to include something is printed (to understand what is gouing on)

17 years agoadded library_auto/ to tests.
Enrico Tassi [Fri, 20 Apr 2007 12:26:16 +0000 (12:26 +0000)]
added library_auto/ to tests.

17 years agofixed paths and prefixes of included files
Enrico Tassi [Fri, 20 Apr 2007 12:24:44 +0000 (12:24 +0000)]
fixed paths and prefixes of included files

17 years agoInterface of the argument to Continuationals.Make greately simplified. The
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 11:30:44 +0000 (11:30 +0000)]
Interface of the argument to Continuationals.Make greately simplified. The
following functions have been removed:
 - id_tactic
 - get_status
 - get_proof
 - set_goals

17 years agochanged base uri
Cristian Armentano [Fri, 20 Apr 2007 10:06:10 +0000 (10:06 +0000)]
changed base uri

17 years agoinitial import
Cristian Armentano [Fri, 20 Apr 2007 10:03:20 +0000 (10:03 +0000)]
initial import

17 years agoEXPERIMENTAL and _INCOMPLETE_ COMMIT:
Claudio Sacerdoti Coen [Thu, 19 Apr 2007 17:21:09 +0000 (17:21 +0000)]
EXPERIMENTAL and _INCOMPLETE_ COMMIT:

Tacticals invoked from the top-level but the ones implemented on top
of tinycals  where not working properly because of several bugs.

The current commit changes the code in quite a few places:

1) there is no longer a function Tacticals.Make since tacticals implemented
   on top of tinycals always instantiated the functor with
   Tacticals.ProofEngineStatus, and the toplevel can avoid any instantiation
   at all since it can invoke tinycals directly on the low-level machine
   (implemented by the functor Continuationals.Make)
2) when GrafiteEngine now meets a punctuation tacticals, it directly invokes
   an instantiation of Continuationals.Make, without going througw Tacticals.
   Instead, when it meets a real tactical, it directly invokes Tacticals
   (where Continuationals.Make is applied to Tacticals.ProofEngineStatus
   and not to the module defined in GrafiteEngine and used for punctuation
   tacticals)
3) most of the tacticals not implemented on top of tinycals were bugged
   (and unused). E.g.: solve always diverged unless it was applied to the
   empty list. All these bugs have been fixed.

The commit is incomplete since:

1) all tacticals not implemented on top of tactics now accept only a single
   tactic as argument (if they require a list, the list must be a singleton).
   This limitation is going to disappear again, but we must change GrafiteAst
   so that an atomic tactical becomes a recursive tactic.
2) Seq and Then are not branched (for the same reasons as 1 and a bit of
   lazyness)
3) several auxiliary functions in the argument of Continuaniolas.Make can now
   be removed since they were introduced for wrong reasons.

17 years agoThe night test now shows the last commits and blames/praises the authors.
Claudio Sacerdoti Coen [Thu, 19 Apr 2007 17:17:36 +0000 (17:17 +0000)]
The night test now shows the last commits and blames/praises the authors.

17 years agomore discriminate
Enrico Tassi [Wed, 18 Apr 2007 10:08:40 +0000 (10:08 +0000)]
more discriminate

17 years agohandles failures (sometimes you can't inject)
Enrico Tassi [Wed, 18 Apr 2007 09:20:57 +0000 (09:20 +0000)]
handles failures (sometimes you can't inject)

17 years agoNew query result diff.
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 09:15:18 +0000 (09:15 +0000)]
New query result diff.

17 years agoOnly benches with the same result are compared for timing.
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 09:10:30 +0000 (09:10 +0000)]
Only benches with the same result are compared for timing.

17 years agoAdded new query to time-diff the last mark with the previous one.
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 08:56:53 +0000 (08:56 +0000)]
Added new query to time-diff the last mark with the previous one.
The query is also the example query below in case you want to change the two
marks.

17 years agotassi/sacerdot
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 08:12:52 +0000 (08:12 +0000)]
tassi/sacerdot

17 years ago"end" keyword added
Ferruccio Guidi [Tue, 17 Apr 2007 18:51:26 +0000 (18:51 +0000)]
"end" keyword added

17 years agoone more step toward a decent destruct
Enrico Tassi [Tue, 17 Apr 2007 14:53:04 +0000 (14:53 +0000)]
one more step toward a decent destruct
lifting should now be ok, but handling of wight params is still
shaky

17 years agoRT_BASEDIR changed to a sensible path
Enrico Tassi [Tue, 17 Apr 2007 09:44:43 +0000 (09:44 +0000)]
RT_BASEDIR changed to a sensible path

17 years agobroken list fix
Enrico Tassi [Tue, 17 Apr 2007 09:22:56 +0000 (09:22 +0000)]
broken list fix

17 years agofixed a list.nth called on a too short list
Enrico Tassi [Tue, 17 Apr 2007 08:41:09 +0000 (08:41 +0000)]
fixed a list.nth called on a too short list

17 years ago...
Enrico Tassi [Tue, 17 Apr 2007 08:22:49 +0000 (08:22 +0000)]
...

17 years agoadded generation of hne and heq problems
Enrico Tassi [Tue, 17 Apr 2007 08:21:57 +0000 (08:21 +0000)]
added generation of hne and heq problems