Some examples can't be compiled by mm0-rs

[joliss]

While browsing the examples, I noticed that some of them don't seem to compile with mm0-rs:

$ cd mm0-rs; for i in ../examples/*.mm[01]; do cargo run compile "$i" &> /dev/null && echo "    $i" || echo "ERR $i"; done
    ../examples/assembler-new.mm1
    ../examples/assembler-old.mm1
    ../examples/big_unifier.mm1
    ../examples/compiler-new.mm1
    ../examples/compiler-old.mm1
    ../examples/compiler.mm0
    ../examples/compiler.mm1
    ../examples/demo.mm1
    ../examples/do-block.mm1
    ../examples/goldbach.mm0
    ../examples/hello.mm0
    ../examples/hello_assembler.mm0
ERR ../examples/hello_assembler.mm1
    ../examples/hello_mmc.mm1
    ../examples/hol.mm0
    ../examples/hol.mm1
ERR ../examples/lean.mm1
    ../examples/miu.mm0
    ../examples/mm0.mm0
    ../examples/mm0.mm1
    ../examples/peano.mm0
    ../examples/peano.mm1
    ../examples/peano_hex.mm0
    ../examples/peano_hex.mm1
    ../examples/separation_logic.mm1
    ../examples/set.mm0
ERR ../examples/string.mm0
    ../examples/unprovable.mm0
    ../examples/verifier.mm0
ERR ../examples/verifier.mm1
    ../examples/x86.mm0
    ../examples/x86.mm1
    ../examples/x86_determ.mm1

I'm attaching a failing integration test for mm0-rs, which tries to elaborate all of the example files. I'm not sure if this is the best way to go about it, or even a good idea at all, but perhaps you find it useful.

Here's the errors I'm getting:

examples/hello_assembler.mm1

thread 'main' panicked at 'SourceAnnotation range `(21432, 21479)` is bigger than source length `0`', /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/annotate-snippets-0.9.1/src/display_list/from_snippet.rs:286:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

examples/lean.mm1

error: regular variables cannot depend on other regular variables
   --> ../examples/lean.mm1:362:53
    |
362 | term iota_epsilon2 (G: ctx) (t F: expr) (L: indspec t)
    |                                                     ^
    |

...

examples/string.mm0

error: unsupported input kind
  --> ../examples/string.mm0:28:7
   |
28 | input string: input;
   |       ^^^^^^
   |

examples/verifier.mm1

thread 'main' panicked at 'no entry found for key', components/mmcc/src/infer.rs:1002:49
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[joliss]

I had to make this pub in order to make it accessible from the test. Unfortunately this results in a bunch of warnings about missing documentation.

[digama0]

Hm, not sure exactly how to handle this. Some of the examples are known to fail, but I agree it's not a good look. (The list of files in the CI are the only ones which are really important, but of course the others can function as test cases.) It's closer to a playground folder than a curated collection of test cases. Some of these do appear to be actual bugs though.

• examples/hello_assembler.mm1: This appears to be an issue in which a span from one file is reported as if it was in another file. When you open the file in the editor there is a highlight at the very end of the file which is caused by the call to (assemble) at the top of the file (the error goes away if you comment it out).
• examples/lean.mm1: the error message is correct here, that is not legal syntax. I think the check for this didn't exist when I wrote the original file.
• examples/string.mm0: this is a feature of mm0-hs that was not ported to mm0-rs. The input command exists in mm0-rs but there are no supported input kinds so you basically can't use it at all. (This is conforming in that the set of legal input and output kinds is verifier specific - it's intended to be an extension point.) The feature is of limited usefulness and I was thinking of removing it entirely.
• examples/verifier.mm1: The panic is certainly a bug, but MMC is still quite raw and I don't really expect this file to compile. I have some more MMC files locally that could be used as test cases and a list of unresolved issues in the MMC compiler, but I don't have much time to work on it these days.

[Downchuck]

Is there an active example that does use mm0-rs compile with a main function?

I'm not clear in the hello_mmc it seems like main is empty and the verifier.mm1 the main appears to be potentially out of date?

[digama0]

@Downchuck hello_mmc.mm1 has the current testing setup for MMC compilation. (You can use mm0-rs compile to compile an MM1 file, of course; MM1 does not itself have a notion of main function because it generates MM0 proof objects .mmb corresponding to a formal development -- it's not a programming language as such.) Keep in mind that the MMC compiler is currently in the "barely works" stage, so the average example with 5 lines is likely to run into a compiler bug somewhere. But you should be able to do some hello world examples, and there are two nonempty main examples commented out in hello_mmc.mm1 (both of which seem to trigger errors in register allocation 🙃 ). I suggest opening a separate issue for this, as MMC is an experimental module, while this issue is more about repo organization.