Support for idempotent operations about aac-tactics HOT 7 CLOSED

Thanks for opening the issue @damien-pous. I agree idempotence is a valuable feature, and there is no need to revert anything. Moreover, I can take care of updating the 8.13.2 release (and merge the package to the opam archive) once we reach some fixpoint in the discussion.

I propose the following plan:

• For the v8.13 branch, all that is needed is to update the documentation to mention idempotence. What I think would be really nice to include (but not mandatory), is some small example (3-10 lines) using idempotence for the README. Do you maybe have some small example like that?
• We urgently need to port the idempotence to the v8.14 branch and make a corresponding release for Coq 8.14 (even though only 8.14+rc1 is out currently). Is this something you could take a look at @damien-pous? If so, you can make a pull request with that targeting the v8.14 branch. It may work to just cherry-pick the commit 74899ac in that branch and go from there.
• We need to port idempotence to master, but this is less urgent. This is something I could do after the 8.13 and 8.14 releases are done.

Does this sound reasonable?

from aac-tactics.

from aac-tactics.

I've done a PR on branch v8.14, which seems to compile fine according to the CI.
It contains a cherry pick of commit 74899ac, as well as another commit adding some more documentation.

I can either push this second commit to v8.13, or turn it into another PR. As you prefer @palmskog.

from aac-tactics.

@damien-pous thanks for the PR and the documentation. There are some additional changes that have to be made in both the v8.13 and v8.14 branch to be able to auto-generate README.md and some other boilerplate from our templates. However, I think it's easiest if I do them, so I can take it from here. I will flag up and close this issue when the releases are done.

from aac-tactics.

Great, thanks a lot @palmskog .

from aac-tactics.

Releases are now done and merged in the Coq opam archive, and the idempotence changes and documentation updates have been applied to the master branch, so let's close this.

@damien-pous to help us promote AAC Tactics to Coq users, we would appreciate if you update the link on your website to go to https://github.com/coq-community/aac-tactics (same goes for other projects in Coq-community such as graph-theory)

from aac-tactics.

@palmskog : I updated the link to aac-tactics...
Thanks for everything, once again!

from aac-tactics.