Monad-thunk every nontrivial nontac_expr

SkySkimmer / coq-ltac2-compiler

GNU Lesser General Public License v2.1

5 stars 0 forks source link

Closed SkySkimmer closed 12 months ago

SkySkimmer commented 12 months ago

Fix #17

I am not fully sure that this is a compiler bug as the

  let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in

in the implementation of dispatch could also be blamed for not thunking properly (ie should be

  let l = List.map (fun f -> tclUNIT () >>= fun () -> tclIGNORE (thaw f)) l in

) but it does seem hard or impossible to trigger a bug with non compiled ltac2.

This change does cause some slowdown (bug_10107 goes from 0.04s to 0.06s, non compiled baseline being 0.25s)

SkySkimmer commented 12 months ago

This change does cause some slowdown

also about doubles timings in tests/minibench (still much faster than non compiled)

Janno commented 12 months ago

Would fixing the code in Coq reduce the performance overhead of this change?

SkySkimmer commented 12 months ago