Open joliss opened 2 years ago
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.
While browsing the examples, I noticed that some of them don't seem to compile with mm0-rs:
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
examples/lean.mm1
examples/string.mm0
examples/verifier.mm1