Michael Norrish

Isabelle has much more experience with multi-core Poly/ML. Many of [Makarius’ papers](https://dblp.org/pid/w/MarkusWenzel.html) are likely relevant. But my recollection is that Isabelle also has trouble keeping things busy past 8 cores....

The link above has bit-rotted. The relevant language from the 2022 Isabelle release says: > The datatype command introduces various constants in addition to the constructors. With each datatype are...

The `pairarg_tac` tactic does this for unbound arguments.

But not available to `cexp` programs, as those primitive ops are for `exp` only.

We're using such an old version of MiniSAT that no-one other than us will ever fix it. Is there an obvious test-case we can feed into minisat to demonstrate the...

``` Inductive fib: [~zero:] fib 0 1 /\ [~one:] fib 1 1 /\ [~recursive:] !r n s. 2 fib(n-2) r ==> fib (n-1) s ==> fib n (r + s)...

Message is: ``` Exception raised at IndDefLib.Hol_reln: at IndDefLib.Hol_mono_reln: at InductiveDefinition.new_inductive_definition: at InductiveDefinition.derive_nonschematic_inductive_relations: at InductiveDefinition.derive_canon_inductive_relations: at Term.list_mk_binder: expected list of variables Exception- HOL_ERR {message = "at IndDefLib.Hol_mono_reln:\nat InductiveDefinition.new_inductive_definition:\nat InductiveDefinition.derive_nonschematic_inductive_relations:\nat InductiveDefinition.derive_canon_inductive_relations:\nat...

Closed by #1213

It's an experiment worth doing. But it certainly belongs to another issue.

The gmane link is no good; [this one at `mail-archive.com`](https://www.mail-archive.com/[email protected]/msg01462.html) is probably/possibly what I linked to earlier.