GitLab

- create_env_of_loadpath is now provided in Env instead of Lexer
- find_channel functions now depend on format to determine the
  suitable extensions

	 of a file into a driver

include "toto.drv.import"

with the task pretty printed, it reduce the set of axioms to a minimal
 set of declaration which still prove the goal and pretty print it.

Currently it does the bisection on the goal already prepared for the prover

"%h:%m:%s:%i" (i for mIlliseconds)

Spass does'nt give cputime but wallclock.
eprover doesn't always give time. so use cpulimit_time for them.

add %b for the memlimit in bytes

from the prover output the time used by the prover.

An intermediate format "h:m:s" is used to accept more output
than only seconds.

tested in the same order as they appear in the file.

also, add some (*commented*) memoization debugging output

- bring driver syntax closer to that of theories
- some simple API improvements

- everything is converted to the new shiny way of doing things.
  Well, everything except Gappa, which seems very unifinished anyway,
  and Encoding_instantiate, which is too complex and would like to 
  update it with François.

Also, I commented a little piece of exception reporting in manager/,
will see it with Claude.

THIS IS STILL A WORK IN PROGRESS!
Please inform me about any bugs, ugly APIs, and proposed corrections.

All the non-implemented things, mentioned in the previous commit
message are still in the TODO list and will be done soon.

- dependent transformations (ones that depend on cloning history
  and/or metaproperties) have now the same type Trans.trans and
  can be registered via Trans, too.
- load_driver accumulates appropriate tdecls to be appended to
  tasks before transformation/printing.

At this moment, we have almost everything in place and are ready
to remove Register module (subsumed by Trans and Printer in core/)
and Prover module (its functions will move to Driver), and convert
all printers and transformations to use the new infrastructure. 

Not implemented yet:
- appending driver-imposed tdecls to tasks - when and where?
- metas-options - what is the best way to implement them?
- syntax/typing for metas in theories and drivers.

- introduce a new Theory.tdecl "Meta" to be used for tags
- simplify cloning procedure, get rid of the th_clone field
- when a goal proposition is discarded during cloning, 
  it's still keeped in the theory as a "skip proposition",
  this is needed to preserve/clone every local identifier.
  Skip propositions are eliminated during task formation.
- get rid of a separate Task.tdecl type
- reorganize the Task.task_hd record:
  * use/clone history is cached in a theory-keyed map;
  * meta-properties are cached in a tagname-keyed map.
  This is done to simplify the fine-grained configuration
  of transformations.

- convert Trans and Register to use weak memoization

Driver : fix compose dans le bon sens

- apply transformations in Driver at print_task/prove_task