Michael Norrish

I've been testing a futures-based `THEN1` on cakeml's `compiler/parsing/proofs`. The “sequential THEN1” (which reports failure early rather than when a justification function is applied) is needed in two places: 1....

I can build at selftest level 2 with the futures-based `THEN1` on the branch concurrent-thens. The `sTHEN1` variant was needed in `ARM/arm6-verification/correctness/multScript.sml` (see 262ed734722).

A naive handling of `THEN` further improves pegSound with 4 threads to 30s, and pegComplete to 121s. I say naive because what I'm playing with can cause large overheads on...

A chunking strategy gets the times to (27s,30s,26s) and (110s,112s,111s) respectively. This looks like an improvement, but it still is a significant downgrade on the 8192-way split in the core...

`Holmake --mt=8` on `concurrent-thens` (with some additional locking on `computeLib` that is not yet committed) on `real_topology` takes 94s for the whole file; on `master` (1fb7e0979a1), purely sequential HOL takes...

The existing code in `src/real` might be a guide to achieving this for the rationals. There are a surprisingly large number of rewrite theorems required to capture the various combinations...

This is code in `Holdep`.

Though we might not want to normalise `SUC x` to `x + 1` in general, in cases like this, where it will produce a substantial simplification. Perhaps `SUC (x -...

For example, it would be nice to be able to do ``` overload_on("Foo", ``λ(x,y). x + y * 2``) ``` and then have occurrences of the pattern get printed as,...

This session shows that things are still not quite right: ``` > overload_on("Foo", ``λ(x,y). x + y * 2``); val it = (): unit > ``2 + 3 * 2``;...