ada_spark_workflow icon indicating copy to clipboard operation
ada_spark_workflow copied to clipboard

Move `gnatprove` dependency to nested crate

Open mosteo opened this issue 1 year ago • 3 comments

To avoid making clients of a SPARK library depend on gnatprove itself, we should move that dependency to a nested prover crate.

mosteo avatar Dec 18 '23 18:12 mosteo

Is there an example at any other place on how to do this in that recommended way?

mgrojo avatar Aug 24 '24 19:08 mgrojo

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.

mgrojo avatar Aug 24 '24 21:08 mgrojo

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).

mosteo avatar Aug 26 '24 10:08 mosteo