[isabelle-dev] Inconsistent output on Isabelle/Scala message buses with parallel proofs [51069:2f50ddd3b586]

[Avi Knoll]

Hi all,

Using: changeset 51069:2f50ddd3b586
http://isabelle.in.tum.de/repos/isabelle/rev/2f50ddd3b586

I have subscribed an actor instance to the `session.all_messages` Event_Bus. The actor presently just collects output in memory, and begins processing the output after the prover has finished evaluating all input theories (in a related question, does anyone know how the output signals that it is finished processing all supplied input?). I am mostly interested in "entity" type messages.

When I run the prover normally (i.e. with default settings), sometimes the set of entities produced is a strict subset of those produced at other times. It seems that the prover non-deterministically fails to output some entities, and the problem increases in frequency with larger sets of input theories.

Switching off PARALLEL_PROOFS appears to solve the problem, although as the problem seems non-deterministic I can't say for sure if I've just encountered an accidental string of complete output sets. Adding any sort of slow activity (e.g. printing output to terminal with System.err.println) inline with the prover output collection also reintroduces the problem. As such, I suspect the issue is timing-related.

Here is an example of what might be missing (the output has been parsed into a local datatype, but otherwise unmodified). Note that the lemmas from the theory "move_from_b" are simply missing in the second run:

Run 1:
List(
Entity(move_from_a,[0:3],-4,end,command),
Entity(move_from_a,[6:13],-2,local.move_me,fact),
Entity(move_from_a,[6:13],-2,move_from_a.move_me,fact),
Entity(move_from_a,[3:7],-3,HOL.simp,method),
Entity(move_from_b,[0:3],-20,end,command),
Entity(move_from_b,[6:34],-18,local.name_clash_waiting_to_happen,fact),
Entity(move_from_b,[6:34],-18,move_from_b.name_clash_waiting_to_happen,fact),
Entity(move_from_b,[3:7],-19,HOL.simp,method),
Entity(move_from_b,[0:2],-19,by,command),
Entity(move_from_b,[37:41],-18,HOL.True,constant),
Entity(move_from_b,[0:5],-18,lemma,command),
Entity(move_from_a,[0:2],-3,by,command),
Entity(move_from_b,[0:4],-17,done,command),
Entity(move_from_b,[13:20],-16,move_from_b.move_me,fact),
Entity(move_from_b,[7:12],-16,Pure.erule,method),
Entity(move_from_b,[0:5],-16,apply,command),
Entity(move_from_a,[18:19],-2,==>,constant),
Entity(move_from_b,[13:18],-15,HOL.conjE,fact),
Entity(move_from_b,[7:12],-15,Pure.erule,method),
Entity(move_from_b,[0:5],-15,apply,command),
Entity(move_from_a,[0:5],-2,lemma,command),
Entity(move_from_b,[19:20],-14,==>,constant),
Entity(move_from_b,[9:10],-14,HOL.conj,constant),
Entity(move_from_b,[14:15],-14,HOL.conj,constant),
Entity(move_from_b,[0:5],-14,lemma,command),
Entity(move_from_b,[6:13],-12,local.move_me,fact),
Entity(move_from_b,[6:13],-12,move_from_b.move_me,fact),
Entity(move_from_b,[3:7],-13,HOL.simp,method),
Entity(move_from_b,[0:2],-13,by,command),
Entity(move_from_b,[24:25],-12,==>,constant),
Entity(move_from_b,[19:20],-12,HOL.conj,constant),
Entity(move_from_b,[0:5],-12,lemma,command),
Entity(move_from_b,[7:18],-11,move_from_b,theory),
Entity(move_from_b,[32:39],-11,move_to,theory),
Entity(move_from_b,[27:31],-11,Main,theory),
Entity(move_from_b,[0:6],-11,theory,command),
Entity(move_from_a,[7:18],-1,move_from_a,theory),
Entity(move_from_a,[32:39],-1,move_to,theory),
Entity(move_from_a,[27:31],-1,Main,theory),
Entity(move_from_a,[0:6],-1,theory,command),
Entity(move_to,[0:3],-10,end,command),
Entity(move_to,[6:34],-8,local.name_clash_waiting_to_happen,fact),
Entity(move_to,[6:34],-8,move_to.name_clash_waiting_to_happen,fact),
Entity(move_to,[3:7],-9,HOL.simp,method),
Entity(move_to,[0:2],-9,by,command),
Entity(move_to,[45:46],-8,==>,constant),
Entity(move_to,[40:41],-8,HOL.conj,constant),
Entity(move_to,[0:5],-8,lemma,command),
Entity(move_to,[6:22],-6,local.leave_this_alone,fact),
Entity(move_to,[6:22],-6,move_to.leave_this_alone,fact),
Entity(move_to,[3:7],-7,HOL.simp,method),
Entity(move_to,[0:2],-7,by,command),
Entity(move_to,[25:29],-6,HOL.True,constant),
Entity(move_to,[0:5],-6,lemma,command),
Entity(move_to,[7:14],-5,move_to,theory),
Entity(move_to,[23:27],-5,Main,theory),
Entity(move_to,[0:6],-5,theory,command))

Run 2:
List(
Entity(move_from_a,[0:3],-4,end,command),
Entity(move_from_a,[6:13],-2,local.move_me,fact),
Entity(move_from_a,[6:13],-2,move_from_a.move_me,fact),
Entity(move_from_a,[3:7],-3,HOL.simp,method),
Entity(move_from_a,[0:2],-3,by,command),
Entity(move_from_a,[18:19],-2,==>,constant),
Entity(move_from_a,[0:5],-2,lemma,command),
Entity(move_from_b,[7:18],-11,move_from_b,theory),
Entity(move_from_b,[32:39],-11,move_to,theory),
Entity(move_from_b,[27:31],-11,Main,theory),
Entity(move_from_b,[0:6],-11,theory,command),
Entity(move_from_a,[7:18],-1,move_from_a,theory),
Entity(move_from_a,[32:39],-1,move_to,theory),
Entity(move_from_a,[27:31],-1,Main,theory),
Entity(move_from_a,[0:6],-1,theory,command),
Entity(move_to,[0:3],-10,end,command),
Entity(move_to,[6:34],-8,local.name_clash_waiting_to_happen,fact),
Entity(move_to,[6:34],-8,move_to.name_clash_waiting_to_happen,fact),
Entity(move_to,[3:7],-9,HOL.simp,method),
Entity(move_to,[0:2],-9,by,command),
Entity(move_to,[45:46],-8,==>,constant),
Entity(move_to,[40:41],-8,HOL.conj,constant),
Entity(move_to,[0:5],-8,lemma,command),
Entity(move_to,[6:22],-6,local.leave_this_alone,fact),
Entity(move_to,[6:22],-6,move_to.leave_this_alone,fact),
Entity(move_to,[3:7],-7,HOL.simp,method),
Entity(move_to,[0:2],-7,by,command),
Entity(move_to,[25:29],-6,HOL.True,constant),
Entity(move_to,[0:5],-6,lemma,command),
Entity(move_to,[7:14],-5,move_to,theory),
Entity(move_to,[23:27],-5,Main,theory),
Entity(move_to,[0:6],-5,theory,command))

Thanks,
Avi