Proposal: add `mm0-rs mm1-to-mm0 <input.mm1> [<output.mm0>] [--strip-comments] [--no-inline-imports]`

[srghma]

Problem:

mm0 files are often go out of sync with mm1. E.g. if user adds new pub theorem or a comment (and wants this comment to be in mm0), etc

Solution:

instead of putting .mm0 and .mm1 on equal footing; lets think from now on about .mm1 files as a source of truth, and all other files .mm0, .mmb, .mmu - derived from it

lets add command:

mm0-rs mm1-to-mm0 <input.mm1> [<output.mm0>] [--strip-comments] [--no-inline-imports]

Here I have already implemented MVP and regenerated mm0 files (can see the difference)

$ ./mm0-rs/target/release/mm0-rs mm1-to-mm0 --help
Command line arguments for `mm0-rs mm1-to-mm0` subcommand

Usage: mm0-rs mm1-to-mm0 [OPTIONS] <INPUT> [OUTPUT]

Arguments:
  <INPUT>   Sets the input file (.mm1)
  [OUTPUT]  Sets the output file (.mm0), or defaults to same path as input with .mm0 extension if omitted

Options:
      --strip-comments     Strip comments from the output
      --no-inline-imports  Do not inline imports. If you use this, you probably want to use the `join` command later to inline the imports, since conforming MM0 verifiers (like `mm0-c`) do not support `import` statements
  -h, --help               Print help

[digama0]

Thank you, I have wanted to write this for some time and I'm glad you worked out how to do it.

That said, I do not want mm0 files to become pure build outputs. This tool will be helpful for preparing .mm0 files, but they are intended for human consumption, and we should preserve presentation choices made in the .mm0 files. An alternative command which will help here is a merge tool which acts like this one but also takes an .mm0 file as input and effectively constructs a minimal diff on the .mm0 file to make it consistent with the .mm1 output. This mm1-to-mm0 command would then be the special case where the starting .mm0 file is empty.