Loc.report_position adds a colon and a newline at the end.

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

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

Scheduler : Schedule the call, precompute the
buffer in advance.

if the extension or the format is not recognised