ada_spark_workflow
ada_spark_workflow copied to clipboard
Move `gnatprove` dependency to nested crate
To avoid making clients of a SPARK library depend on gnatprove
itself, we should move that dependency to a nested prover crate.
Is there an example at any other place on how to do this in that recommended way?
By the way, in its current state, the README is inconsistent with the alire.toml
and the GitHub action, because it doesn't tell that you have to run alr with gnatprove
if you want SPARK proof and the GitHub action working as is.
Is there an example at any other place on how to do this in that recommended way?
It is described here: https://alire.ada.dev/docs/catalog-format-spec#using-pins-for-crate-testing , without explicitly mentioning gnatprove (but the idea is the same one).