Compilation broken in git branch v8.5 about coq-ext-lib HOT 5 CLOSED

Fixed in: 5541581

from coq-ext-lib.

Thanks! If you are interested jsCoq ships MirrorCore now, you can try it at:
https://x80.org/rhino-coq/examples/mirrorcore.html

from coq-ext-lib.

This is cool. I tried out the demo but I got an anomaly when running

Eval vm_compute in 1 + 2.

MirrorCore makes heavy use of vm_compute to make reduction fast, does it work in jsCoq?

A better example might be the setoid demo https://github.com/gmalecha/mirror-core/blob/master/examples/Cancel/RtacDemo.v which actually uses a reflective procedure implemented in Rtac.

from coq-ext-lib.

Most uses cases for jsCoq (documentation, tutorials) don't need vm_compute so unfortunately it is not ported yet as it depends on C code. We could however port it if there's a need.

The example is noted thanks! Actually we generate pages from CoqDoc scripts so even the docs could be runnable.

from coq-ext-lib.

RtacDemo.v added at https://x80.org/rhino-coq/examples/mirror-core-rtac-demo.html.

Unfortunately until we don't port vm_compute indeed the tactic is quite slow.

from coq-ext-lib.