• François Bobot's avatar
    session pairing: simplify and move session pairing. · e6f52504
    François Bobot authored
      session pairing doesn't compute anymore the shape of the goal, it is
     done before. It was able to compute the shape only when the checksum
     of the task was different, but computing the checksum of the task is
     way more time consuming than computing the shape of the goal (and
     include it).
     So this commit simplify greatly the function and theoretically
     augment just a little the time spent. Experimentaly it's the inverse
     on max_matrix. Until "update_session: done" with or without modifying
     the checksums:
                before     |   after
    without : 0.21-0.22 s  | 0.16-0.17 s
    with    : 0.23-0.26 s  | 0.18-0.20 s
session.mli 14.4 KB