Degraded performance of `auto-invert-solve` in OCaml 5.0.0

The t/harpoon/nats_and_bools_tps_auto_invert.input test case using the auto-invert-solve tactic takes ~80 seconds to succeed when Harpoon is compiled using OCaml 5.0.0. That test case is reported to fail with the upgraded OCaml compiler because the TEST.sh script has a 10 seconds time limit for each test case.

With OCaml 4.14.1, that same test case succeeds in ~0.07 seconds. This seems to suggest that some optimizations done during the compilation of the Logic module with OCaml 4.14.1 are not performed in OCaml 5.0.0.

Load the signature t/harpoon/nats_and_bools_tps_auto_invert.input in Harpoon and input the commands in t/harpoon/nats_and_bools_tps_auto_invert.input. The degraded performance happens specifically when inputting auto-invert-solve in the following Harpoon states:

Theorem: tps
intros <- split x (case e_if_then_else)
Meta-context:
  M1 : ( |- term)
  M3 : ( |- term)
  M4 : ( |- term)
  M2 : ( |- term)
  A : ( |- tp)
  S : ( |- step M1 M2)
Computational context:
  x : [ |- step (if_then_else M1 M3 M4) (if_then_else M2 M3 M4)]
  x1 : [ |- hastype (if_then_else M1 M3 M4) A]

--------------------------------------------------------------------------------
[ |- hastype (if_then_else M2 M3 M4) A]

Theorem: tps
intros <- split x (case e_if_false)
Meta-context:
  M1 : ( |- term)
  N : ( |- term)
  A : ( |- tp)
Computational context:
  x : [ |- step (if_then_else false M1 N) N]
  x1 : [ |- hastype (if_then_else false M1 N) A]

--------------------------------------------------------------------------------
[ |- hastype N A]

Theorem: tps
intros <- split x (case e_if_true)
Meta-context:
  N : ( |- term)
  M2 : ( |- term)
  A : ( |- tp)
Computational context:
  x : [ |- step (if_then_else true N M2) N]
  x1 : [ |- hastype (if_then_else true N M2) A]

--------------------------------------------------------------------------------
[ |- hastype N A]

Beluga-lang / Beluga

Degraded performance of `auto-invert-solve` in OCaml 5.0.0 #267