search

mit-pdos / perennial

Verifying concurrent crash-safe systems
MIT License
156 stars 33 forks source link

Check print assumptions in CI #70

Open upamanyus opened 4 months ago

upamanyus commented 4 months ago

Currently, make ci does not build the various print_assumptions.v files and check them. It would be nicer if it were easy to build them and validate that the axioms are unchanged.

As a concrete problem, I introduced admitted specs for waitgroup while changing the naming convention for sync, and nothing failed in CI due to those admits.

tchajed commented 4 months ago

In general we don't have printing tests but we should copy that infrastructure from stdpp/Iris and then use it in a few places, including for print_assumptions.v. It would also be good to track regressions in printing GooseLang expressions, and other notations that are important for readability.