search

alire-project / ada_spark_workflow

A demo of best practices for open-source Ada/SPARK development
MIT License
31 stars 5 forks source link

Move `gnatprove` dependency to nested crate #10

Open mosteo opened 9 months ago

mosteo commented 9 months ago

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

mgrojo commented 3 weeks ago

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

mgrojo commented 3 weeks ago

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.

mosteo commented 3 weeks ago

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