Michael Norrish

- When Holmake runs something to get a theory built, it doesn't call `hol` _per se_, it calls `buildheap` on a set of `.uo` files, which in turn causes the...

I thought recent profiling suggested it was loading _code_ that was causing the slow-downs, but I agree that it would be nice to know just where the slowness is coming...

Loading CakeML’s `preamble` on top of the standard core HOL heap takes just over 15s on my machine. If you have preloaded this (as happens in `misc/cakeml-heap`), loading it is...

1. I don't know where you think all of `misc` is going to be upstreamed to, because there are theorems in it that are never going to make it to...

Indeed, it is only the parsing issue that bothers me. I am mostly happy with the use of `misc` to act as a simple `open` (though, strictly, it is `preamble`...

So, to answer one of @xrchz's questions: yes, I do believe some of the stuff in `misc` should be pushed back to the theories that use it. If there are...

My list wasn't exhaustive; it was meant to demonstrate the variety of ways in which things are not right for moves to HOL. Another example would be the theorem that...

The problem with having `misc` at all is that it becomes a dumping ground for random crap with the implicit suggestion that I have to sort through it looking for...

This is trickier than one might first think. In particular, the existing “monitoring” and “stopping” infrastructure only ever sees the sub-term where a reduction is about to occur. One doesn’t...

I'm afraid `EVAL`’s behaviour under the hood is terribly opaque, so it’s far from obvious to me what might be going on in your examples. I’m tempted to close this...