search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Coq's bullet behavior is not strict. #1823

Open scuellar opened 1 year ago

scuellar commented 1 year ago

Coq's bullet behavior is strict by default, but in Heapster and saw-core-coq they don't focus the current subgoal and allow for the wrong number of bullets to be added. This is prone to errors and makes tracking changes harder.

This behavior was leaked into Heapster by the use of the coq-bits which in turn was infected by it's use of ssreflect. As you can see in this issue ssreflect's use of bullets predates the introduction of bullets in Coq 8.4. In fact, I think the non-strict use of bullets was probably introduced by the Coq team to support ssreflect. Unfortunately they opted for setting the behavior globally, which leaks into other projects). As Ralf (under)states in the same issue, that is slightly irritating.

There are two ways to solve this problem. In order of preference:

  1. Wrap all the imports of Bits into a single file that sets Bullet Behavior back to "Strict Subproofs"
  2. Add Set Bullet Behavior "Strict Subproofs". at the top of every file that imports Bits
scuellar commented 1 year ago

@m-yac @eddywestbrook @RyanGlScott , I'm happy to implement a solution once I get input from you.

RyanGlScott commented 1 year ago

I recall running into this same thing a while back, and I remember @eddywestbrook and I both being annoyed by it. I agree that we should do something about it.

One more option, which might be worth considering: what if we made a patch to coq-bits instead? If I'm reading this comment correctly, then it is possible to prevent ssreflect imports from changing the bullet behavior by importing it in a certain way. If we could make coq-bits use this import style whenever it brings in ssreflect, then that ought to stop the issue at its source.