finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);

improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;

excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);