smoke detection in ide
This issue is to record discussion about smoke detector on why3-club. smoke detector is a transformation that can be launched on any goal: using it may lead to an inconsistent state.
People want to keep usability of this transformation in the IDE. Several solutions exist to prevent errors:
- do nothing: the transformation is already described in the IDE
- allow using it only on proof nodes
- raise a warning when this transformation is called
- treat the smoke detector transformation in a specific way in the IDE/session so that smoke detected transformation do not make their parent goal appear proved. Adding an "inconsistent if reachable" value ?
[EDIT: Also make sure that the exact same smoke from why3replay can be used in IDE (or intentionally forbid it)?