search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Build runproof and owise removal #266

Closed nishantjr closed 3 years ago

nishantjr commented 3 years ago

LGT Does this solve a prover issue you're having?

Yes, the owise rule was causing theprover to crash

hjorthjort commented 3 years ago

Are you thinking we'll change the CI staging back after the project is done? If so, makes sense to me, but lets record it in an issue.

nishantjr commented 3 years ago

Are you thinking we'll change the CI staging back after the project is done? If so, makes sense to me, but lets record it in an issue.

I think this change should be permanent. Because, in general most changes we make will be to the semantics and proofs. Changes to Tezos, such as updating to a new version, or changing how the compatibility tests are run should be relatively rare.