The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 09/08/2017 21:46, Abhishek Anand wrote:
> I am wondering whether someone has written a more lenient version of
> vm_compute (or native_compute) that plows through stuck proofs,
> similar to the way extracting to OCaml and then evaluating would.
> 
> I understand that such an evaluator may in general diverge and produce
> results that disagree
> with Coq's reduction semantics. However, it seems possible to have the 
> evaluator
> agree with the result of evaluating the OCaml extract, at least for
> programs of "simple" non-propositional types such as nat.

Some times ago I did work on a version of vm_compute that skips proofs
(rather than plows through them). So it is not quite the same as what
you expect. In particular, if my version gets a reduced term at the end,
then it is necessarily the reduced term (so the system stays
consistent), contrarily to what an extraction-based mechanism would provide.

https://github.com/silene/coq/tree/VMaccu

Unfortunately, more pressing matters happened and I never got to
complete the work. It is still on my todo list and I hope to free some
time during Fall. As far as I remember, the back-end was complete. There
were three small pieces missing from the middle-end:

1. Mark some opaque symbols as absorbing. While the performance gain is
already noticeable as it stands, it is nowhere near what one expects
until this part is implemented.

2. Add a compile-time optimization to mark match constructs with only
absorbing branches as absorbing. This is helpful for not wasting time
when evaluating things like proofs by contradiction.

3. Be a bit more user- and ltac-friendly when an absorbing element
remains after a reduction and thus causes vm_compute to abort (what you
call a "disagreement").

Best regards,

Guillaume