mm0-c error when verifying peano.mmb against peano.mm0

[jiaminglimjm]

After compiling mm0-c with the command gcc main.c -o mm0-c, when I run ./mm0-c ../examples/peano.mmb < ../examples/peano.mm0 I get this error

stmt: 4120A
cmd: 41224: End

at opab: variable type does not match theorem

--| `(a,b) e. Xp A B` iff `a e. A` and `b e. B`.
def Xp (A B: set) (.x .y: nat): set = $ X\ x e. A, B $;
                  ^

cmds:
  4120C: Dummy 1  // = nat
  4120E: Ref 0  // = expr v2:wff
  4120F: Ref 1  // = expr expr out of range
  41211: Ref 3  // = expr expr out of range
  41213: Ref 0  // = expr v2:wff
  41214: Ref 1  // = expr expr out of range
  41216: Term 61  // = pr
  41218: Term 10  // = eq
  4121A: Ref 2  // = expr expr out of range
  4121C: Term 2  // = an
  4121E: Term 9  // = ex
  41220: Term 9  // = ex
  41222: Term 14  // = ab

Do you think it's something wrong with my setup or did something go wrong elsewhere? I get the same error using gcc9.3.0 and gcc10.2.0. My only guess is that my computer possibly messed up some limits like g_store_size when compiling. I have no luck with mm0-hs either but that's another issue for another day :( mm0-hs verify hello.mm0 hello.mmu was the only one that worked )

[digama0]

I don't actually keep peano.mmb up to date because it's a binary file and it causes a lot of churn in git to keep updated. Work to improve CI to keep these build output files available for download but not checked in to source control is still unfinished, but in the meantime, the way to generate the file is using mm0-rs compile peano.mm1 peano.mmb. The CI script does this, so as long as you see the green checkmark on the latest commit then this procedure should work.

mm0-hs is also quite out of date, and probably can't parse any of the mm1 files anymore. Maybe I will eventually bring it back to parity but keeping two proof assistants up to date is a bit too much for me to do on my own. I recommend just using mm0-rs for the time being.

[jiaminglimjm]

I see, thank you very much!