search

coq-community / aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
https://coq-community.org/aac-tactics
Other
29 stars 21 forks source link

Support for idempotent operations #90

Closed damien-pous closed 3 years ago

damien-pous commented 3 years ago

Commit 082ed3cc71 in branch v8.13 adds support for idempotent operations. How show we integrate this into the various branches / coq version?

palmskog commented 3 years ago

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:

Does this sound reasonable?

damien-pous commented 3 years ago

Thanks for opening the issue @damien-pous https://github.com/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.

ok

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?

I did include an example in Tutorial.v, I can add something in the README, but for now it's rather minimalistic (a single example with an AC operation) and it points to Tutorial.v for more examples. Maybe I should just mention idempotency in the README and elaborate a bit more in Tutorial.v ? I'll do that for now. -> with a pull request or a second commit in 8.13?

ok, I'll try to do that now.

  • 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 done.

Does this sound reasonable?

yes, thanks !

damien-pous commented 3 years ago

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.

palmskog commented 3 years ago

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

damien-pous commented 3 years ago

Great, thanks a lot @palmskog .

palmskog commented 3 years ago

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)

damien-pous commented 3 years ago

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