Michael Norrish

In Moscow ML, this code will need to use `use`. The parsing code can be kept separate, but the final stage that invokes `use` to apply the tactic (evaluate the...

A particular theory `.dat` file depends on its script file and the theory files it loads. An existing `.dat` file already records the hashes of its ancestor `.dat` files (which...

Well, the script file hashes could be the keys that you looked up in the cache... It seems a rebuild has to happen if 1. the script file is newer...

Can we please please not reinvent the wheel here? This is not so different from building/compiling in a normal PL environment so there is probably existing work to consult.

Yeah, agreed. We shouldn't do what I suggested earlier and have script-file hashes in `.dat` files. Given that the `.dat` files then contain all of the relevant hashes of their...

This seems plausible but there are some wrinkles yet, I think. In particular, while a theory file `childTheory.dat` does indeed depend on its script file (`childScript.sml`) and related ancestor `ancestorTheory.dat`...

Yes, you're right I think. Do you want to check some build hashes to make sure our current dat-hashing is doing the right thing? On 5e90404ff31 (`develop`), what is your...

> > I'm imaging Holmake will alternate these steps: calculate key, lookup cache, download, calculate key, lookup cache, download, calculate key, lookup cache (miss), run a real build, calculate key,...

Your `tracing/{yes, no}` directories should include `Tracing.sig` and `Tracing.sml` files (separating out the `structure` and `signature` declarations), and don't need `Holmakefile`s (what you've declared there is the default behaviour). Note...

There's an example of this sort of dance in the way `src/portable/Arbint` is able to use PolyML's built-in support for arbitrary ints but the Moscow ML code uses its own...