Michael Norrish

Holmake chews its way through the dependency graph by using `fork` and `exec` to create jobs to execute script files which have no dependencies. It's doing a traversal of the...

@totorigolo Sorry not to have answered your questions earlier! Holmake does indeed know everything about the dependency graph before it starts. Since Oct/Nov 2019, this extends to knowing everything over...

To make a cache work on tactic text at the REPL level, you'd have to make a version of `e` that actually took a string as argument. The editor modes...

Sorry to have left this so long!

Hmm, I suppose a definition setting something like `LOCAL_CLINE_OPTIONS` might work. You only pick up `CLINE_OPTIONS` if you start the make in that directory, but `LOCAL_CLINE_OPTIONS` are always applied, but...

The original post's behaviour isn't visible in standard core HOL. It can be seen by first doing something like ``` Overload "++" = “SUM_MAP”; ``` so as to guarantee an...

In general, it shouldn't because the failure of the dependency analysis means that Holmake doesn't have a correct picture of what the dependency graph is, and it is this that...

I think you're right that there is a reasonable behaviour here.

One issue with this is that you don't want to have to maintain multiple “alias of” pieces of information, but you do perhaps want to the information appearing in two...

I like idea № 1 (warning about redundant `INCLUDES`), but cannot abide the idea of `Holmake` making in-places changes to `Holmakefiles` for the user. The warning could be turned off...