Unfold tactic generalized to perform zeta-reduction.
WARNING: the tactic is bugged since it tries to zeta-expand a term that lives
in the context of the goal, not in the context of the pattern!
New strategy for let-in unfolding (aka zeta reduction): a reference to a
let-bound variable is expanded if and only if the simplified form of its definiendum (applied to the actual arguments) is different from the
non-simplified form.
LAMBDA-TYPES moved under contrib, fixed (to use the library of Coq even if
the library of matita is already compiled) and added to the daily benchmark.
bug fix for IDA: uses remote names (i.e. http://..) when patching xml bases so that external links like images gets valid URIs instead of invalid local ones like /tmp/...
Since several weeks whelp did not compile any longer. Fixed:
1. the new getter implementation by Zack does not implement yet remote
calls. I have changed the (sample) configuration file to use an internal
getter (maybe also speeding up the tool?)
2. the new parser implementation does not have hard-coded notation. The
notation is now loaded from two files on disk (core_notation.moo and
coq.moo). I have added to entries in the configuration file to hold the
path to the two moo files.
3. Whelp needs to parse and pretty-print the alias definitions. The old
parser and pretty-printer was removed from CVS. I have re-used the new
pretty-printer, but no parser was available. I have reimplemented it
(in DisambiguatePp :-). The file should probably be renamed. Moreover,
the code implemented is very redundant with the corresponding one in
MatitaEngine
WARNING: this commit changes the DB representation; you need to alter the
DB by hand after this commit
- h_position: varchar(255) -> varchar(62)
- h_sort: varchar(255) -> varchar(6)
- several indexes have been redesigned from scratch.
Motivation: MySql is not able to exploit two indexes (on columns c1 and c2)
in a query of type "select ... from table where c1 = x and c2 = y".
Only one of the two indexes is exploited; the other test is done on each line. My commit introduces a single index on c1 AND c2 in place of two indexes.
WARNING: it is sure that a few queries (e.g. match) are greatly optimized by
this commit. On the contrary I ignore if the performance of other queries drops.Moreover, I have not optimized yet the indexes over the hits and count tables.
WARNING: this commit changes the DB representation; you need to alter the
DB by hand after this commit
- h_position: varchar(255) -> varchar(62)
- h_sort: varchar(255) -> varchar(6)
- several indexes have been redesigned from scratch.
Motivation: MySql is not able to exploit two indexes (on columns c1 and c2)
in a query of type "select ... from table where c1 = x and c2 = y".
Only one of the two indexes is exploited; the other test is done on each line.
My commit introduces a single index on c1 AND c2 in place of two indexes.
WARNING: it is sure that a few queries (e.g. match) are greatly optimized by
this commit. On the contrary I ignore if the performance of other queries drops.
Moreover, I have not optimized yet the indexes over the hits and count tables.
Partial bug fix: every inner type is now added to the selection roots.
However, the inner types are not closed terms! They live in the context of
their terms. Right now there is a bug in locating subterms of a proof.
Thus I do not even try to fix inner types selection properly.
0. core_notation.ma splitted into coq.moo and core_notation.moo
1. 'include "coq.ma"' is now explicitly required to activate the notation of Coq
2. 'include "coq.ma"' added here and there in the tests
3. .ma headers updated
projects / helm.git / log