proof-state recorder tweaks and fixes (!117) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis · GitLab

Snippets Groups Projects

Merged Björn Brandenburg requested to merge bbb/prosa:proof-state-rec-fixes into master 4 years ago

Sep 22, 2020
- proof state recorder: add more out-of-sync checks · bd37be63
  Björn Brandenburg authored 4 years ago
  
  bd37be63
- proof state recorder: don't trip over vernacular commands · fa25f0dc
  Björn Brandenburg authored 4 years ago
  
  The vernacular commands Opaque / Transparent change coqtop's prompt counter without generating a prompt (for whatever reason). The proof state recorder needs to be aware of this to avoid a out-of-sync assertion false positive.
  fa25f0dc
- proof state recorder: handle multiple closing '}' · 4d2930e4
  Björn Brandenburg authored 4 years ago
  
  4d2930e4
- proof state recorder: fix double prompt detection · 062a16aa
  Björn Brandenburg authored 4 years ago
  
  062a16aa
- proof state recorder: add --pause option · c3308947
  Björn Brandenburg authored 4 years ago
  
  For debugging purposes, slow down the interaction with coqtop to maybe trigger some potential races more reliably.
  c3308947
- proof state recorder: check expected interaction number · 5c6d8f41
  Björn Brandenburg authored 4 years ago
  
  If coqtop reports a different number of interactions in its prompt than we provided, we're out of sync.
  5c6d8f41