Generate Kani Metrics

[carolynzech]

Add a new "Kani Metrics" workflow (that runs every week) that calls ./scripts/run-kani --run metrics, then creates a pull request to this repository with the computed metrics. See here for an example of what the pull request will look like. Also update our "Build Book" workflow to publish graphs of the metrics.

Callouts:

• This is a separate workflow from the Kani workflow because it is a cronjob instead of running on every pull request. I thought the plots would be too noisy if we ran on every PR.
• See the "Notes" section of kani_std_analysis.py for other callouts.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

LGTM modulo minor fixes.

[celinval]

Thank you for holding off the merge. I don't think we should upload images to our repo to avoid unnecessarily growing its size. Per our offline discussion, I think we can keep running this weekly job to collect the metrics, and we can plot those metrics as part of building our book.

[carolynzech]

Per our offline discussion, I think we can keep running this weekly job to collect the metrics, and we can plot those metrics as part of building our book.

@celinval I've made these changes. The kani-metrics workflow now only changes one file, metrics-data.json, and creates a weekly pull request to update it. See the updated PR on my fork.

Separately, the "Build Book" workflow reads from that file, plots the data, then puts it in the book. See the book on my fork to see what it'll look like.

[celinval]

This should be a mdbook pre-processor. Can you make sure we can still build the book if the png files are not there?

[carolynzech]

Done (sort of). I got it working for mdbook build doc but not mdbook build inside the doc/ directory. At the moment, I can't really see a way around it because we need to pass a --manifest-path to the preprocessor (this is how the example does it too).

[carolynzech]

See my fork book.