search

flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Update snapshots #109

Closed wilcoxjay closed 1 year ago

wilcoxjay commented 1 year ago

It turns out that the examples/ directory tests weren't being run, and a few other tests weren't being run, because of paths not existing and the tests silently passing. I fixed this.

I had to move the examples/ directory into the temporal-verifier crate because I couldn't get cargo insta review to recognize snapshots outside any crate.

~I also added a lint to check that the committed snapshots can be regenerated from scratch.~

I regenerated all snapshots.

wilcoxjay commented 1 year ago

I cannot for the life of me figure out what is going on with github CI here. ./tools/ci-check.sh --ci passes on my macbook and my linux workstation, but fails mysteriously on github.

Anybody have ideas?

tchajed commented 1 year ago

I think I saw a linefeed character in one of the logs, maybe you need to set LANG=en_US.UTF-8 or LC_ALL=C.UTF-8?

tchajed commented 1 year ago

Sorry for all your debugging troubles!

It seems like cargo insta test --unreferenced=auto is the correct way to run insta in CI to also check for unused snapshots (the docs do highlight some differences in a CI environment). There's no need to delete and regenerate them from scratch, since cargo insta is already doing that (and in fact the code as written is running snapshot tests twice).

wilcoxjay commented 1 year ago

Ah, good find. Does that also handle the problem we were seeing where the header of the snapshot files was out of date?

tchajed commented 1 year ago

I'm not sure about the header, that one seems like a bug in insta. I'm okay with not handling that in CI.

wilcoxjay commented 1 year ago

Ok I'll do that.

wilcoxjay commented 1 year ago

Ok after a bunch of churn and discussing with @tchajed, I'm giving up on the lint that checks whether snapshots can be regenerated. We should occasionally run

cargo insta test --unreferenced=auto

to remove snapshots that are no longer used.

tchajed commented 1 year ago

Thanks for fixing this! The cargo insta test situation is unfortunate but now that we know an easy way to check I hope this problem is mitigated.