Move MMIO.v about bedrock2 HOT 3 CLOSED

This is actually a pretty big issue, and is causing fiat-crypto to fail on Coq's CI with

COQNATIVE /builds/coq/coq/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo
ocamlopt.opt got signal and exited
Error: Native compiler exited with status 2 (in case of stack overflow,
       increasing stack size (typicaly with "ulimit -s") often helps)

(c.f. zulip thread)
(We want the native compiler in fiat-crypto, but apparently native compilation is sort-of incompatible with bedrock2 examples?)

from bedrock2.

i support moving this file out of examples to just compiler, and i imagine a change that even left a deprecated compat Export on the old path would be relatively painless. @samuelgruetter ?

from bedrock2.

i support moving this file out of examples to just compiler, and i imagine a change that even left a deprecated compat Export on the old path would be relatively painless. @samuelgruetter ?

That sounds good, I guess if you move that file and then put just Require Export compiler.MMIO. in compilerExamples/MMIO.v, then every file that requires or imports compilerExamples.MMIO won't notice any difference?

from bedrock2.