Speedup spec all

[ordinarymath]

Note that reusing set from hyp_frees is actually slower.
times using time bin/build
before
real 10m37.510s
user 21m43.869s
sys 3m12.949s
reusing set from hyp_frees
real 10m40.847s
user 21m49.628s
sys 3m16.913s
without reusing set from hyp_frees
real 10m29.285s
user 21m9.849s
sys 3m10.606s
note depends on #1623

[ordinarymath]

I think why reusing the set from hyp_frees is slower is that the vars from strip_forall is already guaranteed to be fresh in the term and that sorting the list makes it so that the loop check here https://github.com/HOL-Theorem-Prover/HOL/blob/24e40cd1c7f7e235a5c9f32f692c0d9ae04ddb2b/src/0/Term.sml#L345C1-L347C25 is slower

[ordinarymath]

note time from docker-ci stdknl 3076.5s

[ordinarymath]

I wanted to see if I could speed it up even more by using gen_variant with a predicate check but the issue is that you can't lookup a string using the HOLset produced by FVL and recreating a new set is slower. #1642 is going to be needed for the further improvement.

[mn200]

It seems as if this code should actually be using thm_frees : thm -> term list entrypoint, perhaps after modifying the implementation of that to use FVL internally.

[ordinarymath]

reusing the same set from hyp_frees is actually slower

[ordinarymath]

I still suspect the same thing

I think why reusing the set from hyp_frees is slower is that the vars from strip_forall is already guaranteed to be fresh in the term and that sorting the list makes it so that the loop check here https://github.com/HOL-Theorem-Prover/HOL/blob/24e40cd1c7f7e235a5c9f32f692c0d9ae04ddb2b/src/0/Term.sml#L345C1-L347C25 is slower

[mn200]

But the "new" code is calling hyp_frees.

[ordinarymath]

Making it call thm_frees as the vars in the hyps and thm mix when they end up sorted from HOLset.listItems and it will be slower. making it call hyp_frees is faster

[mn200]

I suspect it doesn't help that thm_frees is not using FVL. Perhaps worse, the fold over prim_variant is gross as well because each call to prim_variant involves a new calculation of the free names of the list, using a list again. The kernel should provide a gen/prim_variants function.

[ordinarymath]

A better way would be if strip_forall has a additional parameter for names it should avoid.