hatsugen VS sml-buildscripts

Might this help? I wrote it: https://azdavis.net/posts/define-pl-01/

Perhaps my own series of posts? It starts here.

2. Preservation states that if you have a program that type-checks _and_ that can continue evaluating, _as_ it continues to evaluate, it _continues_ to type-check.

Note that the conclusion of preservation 'feeds back' into progress: the program type-checks. And vice versa: progress may state as its conclusion that the program can continue evaluating, which then lets you apply preservation. This means you can keep applying the progress and preservation theorems in a 'loop' until the program is done evaluating.

For each of the 4 posts in my series about formal semantics, I duly translated the rules presented in the blog post into Lean code, and then proved that the rules do satisfy the safety properties. For example, for the first post linked above:

- The syntax of the language: https://github.com/azdavis/hatsugen/blob/part-01/src/syntax....

I also use .mlb files exclusively and agree with your general point - but I do make use of Poly/ML and occasionally SML/NJ against the same sources, using scripts to drive them from .mlb files: https://github.com/cannam/sml-buildscripts

These scripts are really limited. They only support the simplest .mlb files that are really just lists of other files, and the semantics are technically incorrect because they have no way to reset the environment when beginning each new .mlb file in, as the spec says they should. I use them scrappily during development and then generally use MLton for production builds. But you can get quite a lot done within those limitations, and it's very nice to have the faster compilation of Poly/ML, as well as the option of seeing error messages from more than one compiler.