Automatically generate the MM0 file from the MM1 file

[segf00lt]

I've been playing around a little bit in the language and, as far as I've understood, the only difference between an mm0 file and mm1 is the absence of proofs. This makes me wonder: could a simple text substitution be used to create an mm0 file from an mm1 file? Why must the 2 files be written separately? So for example, could one extract all lines from peano.mm1 that start with 'axiom' 'pub theorem' etc and write them to peano.mm0 (with the 'pub' stripped off and such), and get a valid mm0 file?

[digama0]

Yes, MM1 was at least in part designed to support that. There are some features you shouldn't use in public theorems if you want it to work though: generating statements or entire (pub) theorems by metaprogramming is out. Inside mm0-rs you could even handle that though, by generating the appropriate statement when one is not provided. A tool to spit out an mm0 file from mm1 would be nice, I just never got around to it.

One reason not to do this (that is, even if the tool existed you should be careful using it) is that you generally want to make sure the mm0 file is available and readable, and when it's a build artifact people will want to not check it in. Seeing changes to the mm0 file in git is a good way to be appraised of "important" changes in the development. Readability can in theory be handled by a good formatter, but it is easier to have control over that by manually writing the file and checking it against the MM1 file instead of just generating it. (We also need better support for that; I'm using mm0-c for this in CI but mm0-rs should support it natively.)

[timotree3]

I think it's valuable to maintain separate .mm0 and .mm1 files, but I don't like the duplication between them. (All the axioms, sorts, terms, and public definitions have to be redeclared in the .mm1 file.) Instead of generating .mm0 from .mm1, would it be possible to allow importing .mm0 files into .mm1 files? e.g. the first line of peano.mm1 could be import "peano.mm0"; and then it could omit all the redundant declarations. I guess the problem would be that you still need to duplicate statements of public theorems and abstract definitions.

[digama0]

You still have to position the non-public definitions and theorems relative to the public ones, since they are in general interleaved (and this is important, since you might be using a public definition in a private theorem on the way to proving a public theorem). But the mm1 file could have an abbreviated version of the declaration which inherits all the properties from the mm0 file, e.g. import def foo; and put the doc comment on the def foo = ... in the mm0 file.

I don't think this import "peano.mm0"; is an "import" relationship per se; but there are also other reasons to want to explicitly or implicitly declare the relationship between the MM0 file and the MM1 file, since if they get out of sync you want something to be able to validate this (e.g. if a theorem declared in the MM0 file is not proved in the MM1 file).