Demodulate and applyS moved form saturation to auto.

Major changes to auto, documented on the helm mailing list.

Minor changes.

a. uniform mangement for context and library
b. collapsing flexible terms (X args) into a single meta. Metas in
   head position give arity problems with discrimination trees.
c. Even terms with a single meta as conlcusion (e.g. elimination
   principles) get indexed.

The type of universe_of_goals has slightly changed, omitting
to pass a useless proof. A few prerr_endline have been removed.

This is only a temporary patch. The typecheker raises a
CicUniv.UniverseInconsistency that should be properly
captured and transformed into a tyepchecking error.

The function exists_a_meta has been modified to capture also
flexible arguments instead of metas.

New function pack_coercion_metasenv, used in auto after try_candidates
to clean up the metasenv (othewise application could fail).

Up to f_algebras.

1. developed up to algebras
2. some lemmas commented out because of a new bug in rewrite

Serious bug fixed: without a Lazy.force the user obtained an error comparing
two functional values.

Disambiguation errors are now compressed in a maybe better way.

Bug fixed: when trying to insert coercions after an Uncertain, a RefineFailure
was raised (instead of re-raising an Uncertain).

Potential performance improvement + better disambiguation error messages:
the delift functions used to raise Uncertain every time it failed; now it
raises Failure when the local context contains no Metas (that means that
for every future subst it will not contain new Rels).
Note: if we are working up to conversion (I do not think so), we should check
that the local context is Meta-closed, that is a weaker check.

Missing optimization implemented: before starting to analyze the disambiguation
domain we try first without interpreting any symbol. This way we can avoid
lot of refinements when the information in the uninterpreted term already
tells us that every instance will not be well typed.

- Disambiguation error exception enriched with more information
  (the same returned in case of correct disambiguation)
- The disambiguation error interface now shows the complete environment
  in which the error occurs. I am not sure if this is better or worst than
  showing only the diffs.

Bug fixed: the diff component of the exception raised when the term cannot
be disambiguated used to lack the last choice in case of the look-ahead
optimization.

EXPERIMENTAL: new interface for disambiguation errors.

[ Moreover, a dead dialog window has been removed ]

Dead dialog window removed.

Dead dialog window removed.

Disambiguation errors now carry more information (i.e. the patches to apply to
the current interpretation to re-obtain the refinement errors).

Dama is now in the night benchmarks.

Too verbose error message (probably activated by Enrico without really wanting
it) removed.

new objects for the LambdaDelta development (4th conjecture proved)

more new objects for the LambdaDelta contribution

Beginning of the development of integration algebras.

Content level representation of LetRec changed.

Content level representation of LetRec changed.

New content level representations for LetRec, Inductive and CoInductive.
For LetRec the pretty-printer is now in sync with the parser.

files with newest objects (to be included in the respective developments)

carr_of_term now returns Fun if a Prod is encountered

fixed defaultauto behaviour. not the cache is preserveed

timeout if unspecfied should be set to infinity, not 0, since the timeout inside the flagfs structure is a time in the future, not a decreasing quantity.
every loop of auto the check gettimeofday() > timeout raise Fail

The default for paramodulation is now back to false (I set it to true
by mistake).

auto => auto new.
There is still one auto left that does not work with the new implementation
(because of implicative hypothesis for local lemmas?)

Inclusion "improved".

CoRN integrated in the night benchmarks.

Manual porting of CoRN to Matita.
The current version shows a bug in coercions to function classes.

Bug fixed: the conversion was done with the wront argument (a sort of typo).

Some hocus-pocus to avoid a common race condition (Gtk/??? code not
reentrant). I bet the "avoided" problem will surface again...

Unlocking the interface was not performed as the last action of the callback.

The RELATIONAL contrib must be compiled before the others since the others
depend on it.

My previous commit changed the regular timeout of paramodulation from
infinity to 30s. Old behaviour restored.

makefiles fixups

fguidi removed from RT in makefiles

Implemented:
 "by ... we proved ... that is equivalent to ... done"
and
 "we need to prove ... that is equivalent to ..."

auto => auto new

auto => auto new
added depth=4 to some file in order to make it pass

I do not understand at all why Enrico removed the contribs from the bench!

Sorry, bug introduced by me yesterday now fixed.
auto should be the new one even when the paramodulation flag is given.

Bugs fixed in merging of composite coercions. In particular the imperative
status was not handled properly and letins were handled inefficiently.

One auto modified in an apply since auto is no longer supposed to apply
elimination principles automatically.

added to applyS in nat/gcd.ma a timeout large enough for compilation in bytecode
mode.

1. applyS now uses its ~params
2. autoTactic.ml* is going to be deprecated.
   auto.ml* has now the expected interface (that of a tactic)
   and it is almost ready to replace autoTactic.ml

applyS now receives the same parameters that auto receives.
The parameters are not used yet.

Theorems from the library and from the context are indexed also in "unfolded"
version.

auto => auto new and other minor changes to make it compile.

auto => auto new everywhere + minor updates to make more tests pass

Comments updated with new reflections.

The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during
qed. In particular, checking composition calls unification, that calls reductions,
that is problematic when there are a lot of lein in the context (as is it the case
with proofs generated by TPTP: see eg GRP486-1.p.ma )

More work to handle -debug properly.

Factorized "find_equalities" in demodulation_tac.

added support for short name targets

resumed ol auto

fixed all (that now uses long paths)

now the makefile for developments requires the depend file
that now has correct dependencies.

1. some "try ... with _ " removed
2. type inference of LetIn terms is now closer than the kernel
3. LetIn code fixed to add the type to the Defs in the environment
4. some typos fixed

reduced timeout to 100s

commented out are_convertible in is_identity
fixed metadataquery so that only are calculated without the DB (but are calculated)
removed is_meta_convertible left right in is_weak_identity
added extra dependencies between gcd < relevant_equations < ord to make
paramodulation happy. In the past this used to be the order used by make.
added an hack in applys.ma, since it used to work due to convertibility.

Some declarative tactics did not allow the "done" option in place
of "(id)". Fixed.

Inline command implemented.

Syntax of paramodulation parameters changed.

Fixed handling of exceptions by the worker threads: the exception is not
notified to the user and the thread exits gracefully.

Removed /home/tassi from the makefile!

Query fixed to handle the cases where 0 tests are failures or successfull.

Changed auto from implicit to option and renamed a few functions.

Regular expression fixed to allow '-' into test names.

sacerdot is now the user for the daily bench.

Crontab updated

No more benches without gc.

sequent_viewer.xml & co are now generated in /tmp if necessary!

updated to use destruct instead of disciminate/injection

Bug fixed: the script Menu was not locked as expected.

The Abort button is now working properly. Cool.

Xavier code for killing a thread commented out for a while since it interacts badly with (labl?)Gtk.

This commit implements the Abort button for the GUI using a clever trick by Xavier Leroy.

restored is_identity instead of is_weak_identity

**** EXPERIMENTAL ****
The GUI of Matita is now thread-based.
In principle Ctr-C works unreliably.
In practice it works reasonably well.

added a subtle List.rev that makes the order of the equalities taken from the library as it used to be. In this way the applys test works, but is not clear why the other order does not produce a solution in decent time

...

auto always uses the context (even if paramodulation) to try to close goals left open by paramod

returns the right list of goals

50 steps on goal are fine for irrat2

removed only made with the DB

removed a pointless call to auto

...

added tests for paramod

...

added missing *)

restored old (r6662) behaviour