Formula for cm2mlb

[jonsterling]

[I don't know if I am filing this ticket in the right place, so feel free to close it if not.]

It would be very nice if there were an easy way to download and install the cm2mlb utility, without having to manually build from the source distribution. Perhaps this could be included in the Homebrew formula (or in a separate formula)?

We are switching to using MLton as the primary compiler for Red JonPRL (the next version of the JonPRL proof assistant), but would still like to be able to compile with SML/NJ, in order to get a faster development cycle as well as proper exhaustiveness/redundancy checks for definitions inside un-applied functors. As such, it would be very useful for us to be able to write just a .cm file, and have it automatically converted in our build script; (even better would be to have the reverse translation, since ML Basis seems superior, but I don't know if that is feasible).

[MatthewFluet]

Thanks for the suggestion.

I'm new to Homebrew; this repository was created in response to a discussion on the mlton-user mailing list; see MLton Homebrew package (Mac OS X).

The minor complication that I can see with cm2mlb is that it does not exist in its own repository; that seems to be an informal assumption of Homebrew. Of course, since it seems that one can execute arbitrary code via a formula, it should be possible. Other alternatives are to extract cm2mlb to its own repo and then git submodule to it from the main MLton repo.

With regards to an mlb2cm tool, it should be possible, but I haven't worked on one before; one difficulty is that the are some scoping/renaming features of MLB files that I do not believe can be handled within a single .cm file, so a tool might need to generate some intermediate .cm and .sml files. Of course, most developments seem not to need to full power of either MLB or CM, so I haven't found keeping both .cm and .mlb files in sync to be that difficult. But, I can see that it would be nice for it to be completely automated.

[jonsterling]

@MatthewFluet I see! Yes, my only experience with Homebrew is as a user, so I don't have much of an idea of what it assumes about repositories.

• Does cm2mlb share much in dependencies with MLton itself? I guess I'm wondering how difficult it would be to break it into a new repository.
• Regarding mlb2cm, I think it would indeed have to translate a number of Basis constructs into intermediary files. I am not sure the effort is really worth it, but it would be so nice to be able to just use a single thing (I would honestly be happy with either CM or MLB, but I think the latter has a more user-friendly interface, and I appreciate the fact that it has an elaboration semantics).

Maybe it would be more worthwhile to see if we can lobby the SML/NJ folks to adopt MLB (or at least, implement support for it). Both systems have things to recommend them, but since they are both quite good, I think maybe the most important thing is that the SML community standardize on something.

[MatthewFluet]

cm2mlb has no dependencies with MLton itself; its a SML/NJ-only program. I've tried running cm2mlb on the cm2mlb .cm file, but it very quickly gets into the internals of SML/NJ.

Matthias Blume had once proposed "Portable Graph Libraries" as a standard intermediate format; the semantics of PGLs are close to MLBs. In fact, the way the cm2mlb tool works is to convert the CM project to a PGL and then transcribe the PGL to an MLB. But, AFAIK, Matthias only ever implemented the CM to PGL conversion. That said, somewhere in the SML/NJ internals there should be the moral equivalent of a "compile this file in this environment" function which could be leveraged to compile outside the CM framework.