The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

As a devoted Adamizer of proof scripts (with a summer's worth of Ltackery to prove it), I can't imagine life without info ...

I'd be interested in knowing how you use it.

I assume this is a consequence of the new proof engine?

 

This is quite accurate, indeed.
 

Is there any hope that info could be restored before the 8.4 final release? If it's a matter of manpower, is adapting info to the new engine something a lowly master's student might be helpful for? I've been toying with writing a few (very simple) ML tactics, so I've probably at least *seen* a few of the files involved :-)

Well, it's somewhat more than a matter of manpower. More important is the fact that info never really had a semantics together with an implementation that was way too deeply embedded into the tactic system. When things changed, it became unclear how to port it. It became the occasion to rethink it. However, no one has come up with a semantics yet. Also, it's been about a year since trunk users cannot use info, and I got very mild (and fairly few) complaints. An immediate consequence is that I have no idea what should be done with it. In the meantime, preferred tools for understanding what ltac does are Set Ltact Debug ( http://coq.inria.fr/distrib/V8.4beta/refman/Reference-Manual012.html#@command244 ) and debug eauto (undocumented, but works just like eauto while outputing debug information). We're lacking a debug auto, this is, I'd say, an unfortunate oversight.

So, you are unlikely to see your wishes granted for 8.4. Patches are always welcome though.



Arnaud