Building from F* into OCaml or Do We Have a Quintiscential Makefile?

[briangmilnes]

Many small things, while learning F*, slowed me down. Being an out of date SMLer and not an OCamler was one of them.
Doing some testing, which deepened my understanding in multiple ways, was another one of them. I'm volunteering more actively
now and am hoping to make the next developer's (proofelvoper) path much quicker.

I looked around at quite a few of the examples makefiles and they all seem to be quite different. In our 86 projects we have
3KLOC of Makefile.

Anyone have a favorite style? I'm walking the dependencies from .fst* to .checked to the .ml but am then
building a dune and dropping my .ml files into.

It works nicely but it seems a bit overly complicated.

[aseemr]

Hi Brian:

You can look at https://github.com/FStarLang/FStar/tree/master/examples/hello/multifile which is meant to be a guide for building such makefiles.

[briangmilnes]

A good example, but it does not go all the way to running OCaml. Running C would be nice
also in a steel example. One thing that confused me, being an ML'r but not an OCaml'r,
was having to opam install fstar.opam to get OCaml to find the fstar ulib.

A more turnkey solution would help learners. Here's mine, but it has not be windowsified.
Makefile.txt