improve presup performance

[HuStmpHrrr]

The current performance of presup kills me. This is the minimal effort I can do to improve the performance. The idea is to lower the search level to reduce useless search effort.

[Ailrun]

How much time does this save (in your machine)?

I once did similar to get a better performance, but in my machine the improvement was not significant

[HuStmpHrrr]

How much time does this save (in your machine)?

I once did similar to get a better performance, but in my machine the improvement was not significant

My machine is probably too old (10 years) to a point that it has been slower than github's action runner, but these changes turn the proof checking from very long to short enough for me to stare at the buffer to wait for it to finish (but still long).

[HuStmpHrrr]

though it could have been faster before, checking the CI /~https://github.com/Beluga-lang/McLTT/actions

It was 9m ish before this change #91 making the CI above 12m. now this PR drops it down to 11m.

If you have some ideas maybe you can do something.

[Ailrun]

though it could have been faster before, checking the CI /~https://github.com/Beluga-lang/McLTT/actions

It was 9m ish before this change #91 making the CI above 12m. now this PR drops it down to 11m.

It is strange... That PR added just one module and a lemma for syntax, which should not take 2 or 3 mins. I will also try some optimizations.

My machine is probably too old (10 years) to a point that it has been slower than github's action runner, but these changes turn the proof checking from very long to short enough for me to stare at the buffer to wait for it to finish (but still long).

OK, if that's the case, let's merge this PR.

[HuStmpHrrr]

though it could have been faster before, checking the CI /~https://github.com/Beluga-lang/McLTT/actions
It was 9m ish before this change #91 making the CI above 12m. now this PR drops it down to 11m.

It is strange... That PR added just one module and a lemma for syntax, which should not take 2 or 3 mins. I will also try some optimizations.

My machine is probably too old (10 years) to a point that it has been slower than github's action runner, but these changes turn the proof checking from very long to short enough for me to stare at the buffer to wait for it to finish (but still long).

OK, if that's the case, let's merge this PR.

I know. I also find it strange, but the drop is sudden and clear. if you compare this PR and the other one, you will see that there is an improvement in this PR.

[Ailrun]

@HuStmpHrrr Actually, that added 3 min is not from library checking. It is from OCaml setup! What...

C.f. /~https://github.com/Beluga-lang/McLTT/actions/runs/9343409604/job/25712951655?pr=95 of #95

It seems like it was a problem of opam depext to do with cache. Updating cache name should fix the issue of CI.

[Ailrun]

It should be fixed in #96 (together with a bit of improvement in NatCases time)