Move MMIO.v

[JasonGross]

Unfortunately, the MMIO.v file that is extremely helpful for instantiating the compiler proof is in the compiler's "examples" folder, meaning we have to build all the examples from both bedrock2/bedrock2 and bedrock2/compiler. Could it be moved?

Originally posted by @jadephilipoom in mit-plv/fiat-crypto#1045 (comment)

[JasonGross]

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?)

[andres-erbsen]

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 ?

[samuelgruetter]

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?