eg https://travis-ci.com/github/coq-community/aac-tactics/jobs/360133083
cc @Zimmi48

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

The following lemma should be transferred to Coq's Stdlib:

  Lemma Pmult_1_l (x : positive) : 1 * x = x.
  Proof. reflexivity. Qed.

The Coq team released Coq 8.14+rc1 on September 17, 2021
and plans to release Coq 8.14.0 before October 31, 2021.
A corresponding Coq Platform releases should be released before November 30, 2021.
It can be dealyed in case of difficulties until January 31, 2022, but this should be an exception.

Coq CI is currently testing commit 16d30ab
on branch https://github.com/coq-community/aac-tactics/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Coq Platform is currently not testing this package!

Could you please create a tag, or communicate us any existing tag that works with
Coq branch v8.14, preferably 15 days before November 30, 2021
or earlier? In case we might have to delay the Coq Platform release cause of issues with
your project, we would prefer to be informed about the situation as early as possible.

Thanks!

P.S.: this issue has been creates semi-automatically.

CC: coq/platform#139

I am currently preparing the Coq platform 8.12.0.

In order to include aac-tactics as planned, I need a tagged release of aac-tactics and an opam package.

I confirmed that the latest commit of the v8.12 branch, that is "ba10dce9877626608ccdf67daee6852b4d896ac0" works. As far as I can tell this is also what is in the Windows installer of Coq 8.12.0. So I would suggest to release this as V8.12.

Like mentioned in #13 , we would like to have opam files for 8.9 and master.

[ERROR] At ~/.opam/repo/coq-released/packages/coq-aac-tactics/coq-aac-tactics.8.5.0/opam:14:45:
Not a recognised version-control URL
[ERROR] At ~/.opam/repo/coq-released/packages/coq-aac-tactics/coq-aac-tactics.8.5.1/opam:14:45:
Not a recognised version-control URL

Debian uses this repository as the upstream of AAC tactics.
To switch to Coq 8.6 we'd like to have a tag for AAC tactic pointing to a commit that compiles with 8.6.

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-aac-tactics.8.16.0
from official repository https://coq.inria.fr/opam/extra-dev/packages/coq-aac-tactics/coq-aac-tactics.8.16.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0.

Coq Platform CI is currently testing opam package coq-aac-tactics.8.18.0
from official repository https://coq.inria.fr/opam/released/packages/coq-aac-tactics/coq-aac-tactics.8.18.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10, please inform us as soon as possible and before October 31st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372

findlib: [WARNING] Interface rewrite.cmi occurs in several directories: /usr/lib/coq/ltac, .

The OCaml part of the project uses several functions in the Pervasives module, which has been deprecated in OCaml 4.08 and later.

I think the current README file is in need of an update, for example:

• does not use Markdown syntax
• does not mention the namespace of the plugin (AAC_tactics)
• does not give a small example
• does not explain manual building and installation
• does not link to the paper describing the underlying theory and implementation

@fakusb does an update like this sound good to you?

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.19.0.

Coq Platform CI is currently testing opam package coq-aac-tactics.8.19.0
from official repository https://coq.inria.fr/opam/released/packages/coq-aac-tactics/coq-aac-tactics.8.19.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2024.01, please inform us as soon as possible and before March 31st, 2024!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

Hi there -- I want to know if the following is possible:

Instance cat_assoc t : Associative (@Permutation t) cat.
    econstructor.
    rewrite catA.
    done.
    done.
Qed.

Instance cat_comm t : Commutative (@Permutation t) cat.
    econstructor.
    done.
    apply Permutation_app_comm.
Qed.

Instance cat_unit t : Unit (@Permutation t) cat nil.
    constructor; intros.
    done.
    rewrite cats0; done.
Qed.

Goal forall T,  forall (x y z a b c : seq T), Permutation (x ++ z ++ y ++ b ++ a ++ c)
                                                  (z ++ a ++ b ++ y ++ x ++ c).
  intros.
  aac_reflexivity.
Fail Qed.

The above fails due to a universe constraint issue between aac_reflexivity and the type introduced in the goal. Is there a workaround for this? Unfortunately, I cannot just force T : Set in my use case (which would solve the problem).

Dear devs,

in Coq we are considering requiring plugins in the CI to use the same set of compiler flags for warnings than the main Coq tree (c.f. coq/coq#9605 ), in particular, this means that the plugins should now compile warning-free, except for deprecation notices.

Note that some of the raised warnings are really fatal, [like missing match cases].

Please, try to fix OCaml warnings present in your codebase, thanks!

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.17+rc1.

Coq Platform CI is currently testing opam package coq-aac-tactics.8.17.0
from official repository https://coq.inria.fr/opam/extra-dev/packages/coq-aac-tactics/coq-aac-tactics.8.17.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03, please inform us as soon as possible and before March 21st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

I recently found this library and found it to be very useful and wish I knew about it years ago.
Is it possible/easy to implement aac_congruence using the machinery defined here?
For example, before calling congruence, one could put in some uniquish normal form expressions containing associative and commutative operators, similar to what ring_simplify does.
If anyone has thought about writing aac_congruence or aac_normalize I would love to know their thoughts and experiences.

The ocaml-function Coq.retype (and Coq.tclRETYPE in #34 ) are used at various points. This has to do with the plugin building coq-terms without updating universe constrains (I guess?).
This seems very fishy and like an ugly hack.

I need to investigate the right methode to compose terms without breaking the universe-constrains.

This might be related with the functions used #35 , or in general with the way the ocaml-side interfaces with the coq-side.

aac-tactics fails to build with the following default.nix file

{ pkgs ? import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/aaec4a5cf80304bb3532156e61b5133c05635e60.tar.gz") {}
}:

pkgs.coqPackages.callPackage
({ lib, mkCoqDerivation, coq, version ? null }:
with lib;

mkCoqDerivation {
  pname = "aac-tactics";

  release."8.13.0".rev    = "v8.13.0";
  release."8.13.0".sha256 = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU=";

  inherit version;
  defaultVersion = with versions; switch coq.coq-version [
    { case = pred.inter (isGe "8.11") (isLe "8.13"); out = "8.13.0"; }
  ] null;

  meta = {
    description = "Coq plugin providing tactics for rewriting universally quantified equations";
    longDescription = ''
      This Coq plugin provides tactics for rewriting universally quantified
      equations, modulo associativity and commutativity of some operator.
      The tactics can be applied for custom operators by registering the
      operators and their properties as type class instances. Many common
      operator instances, such as for Z binary arithmetic and booleans, are
      provided with the plugin.
    '';
    maintainers = with maintainers; [ siraben ];
    license = licenses.gpl3Plus;
    platforms = platforms.unix;
  };
}) {}

Last few dozen lines:

CAMLDEP ra_reification.ml
CAMLDEP mrewrite.ml
CAMLDEP ra_fold.ml
*** Warning: ra_fold.mllib already found in . (discarding ./ra_fold.mllib)

*** Warning: mrewrite.mllib already found in . (discarding ./mrewrite.mllib)

CAMLDEP kat_dec.mli
CAMLDEP kat_dec.ml
CAMLDEP ra_common.ml
CAMLDEP kat_reification.ml
CAMLDEP ra_reification.ml
CAMLDEP mrewrite.ml
CAMLDEP ra_fold.ml
CAMLDEP kat_dec.mli
CAMLDEP kat_dec.ml
CAMLDEP ra_common.ml
CAMLDEP kat_reification.ml
CAMLDEP ra_reification.ml
CAMLDEP mrewrite.ml
CAMLDEP ra_fold.ml
CAMLDEP kat_dec.mli
CAMLDEP kat_dec.ml
CAMLDEP ra_common.ml
CAMLDEP kat_reification.ml
CAMLDEP ra_reification.ml
CAMLDEP mrewrite.ml
CAMLDEP ra_fold.ml
COQC common.v
COQC comparisons.v
CAMLOPT -c  ra_common.ml
CAMLOPT -c  ra_fold.ml
make[1]: *** [Makefile.coq:625: ra_fold.cmx] Error 127
make[1]: *** Waiting for unfinished jobs....
make[1]: *** [Makefile.coq:625: ra_common.cmx] Error 127

Dear AAC-tactics Team,

I added AAC instances for the sepcon type in Princeton VST - which was straight forward. Only if I use aac_reflexivity it leads to very long QED times, at least one million times slower than when directly rewriting with the one lemma required. Below please find example code (using the versions from Coq Platform 2023.11.0). I waited for QED for more than 30 minutes (embedded in a larger proof) and it did not succeed. In below example the direct proof QED time is 1ms, the aac_reflexivity QED timeouts with 10s limit.

I wrote a few reflexive tactics myself and I would expect that one can write the tactic such that the QED time is similar to the tactic run time. What I usually need to make QED fast is a specific eval lazy on the interpretation of the reified term. If I just apply the correctness lemma and leave the unification of the interpretation of the reified term with the original goal term to the unifier, I usually also experience very bad QED blow up. See e.g. metaprogramming-rosetta-stone-real-simplifier. This evaluation makes the interpretation of the reified term identical to the goal, so that unification is trivial (also for the kernel during QED). If this evaluation is removed, the tactic still works, but QED times can be very bad (also tactic run times are slower). This is just a wild guess, but maybe this is the issue with aac-tactics. Note that I would do a lazy now instead of a cbv.

Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.

Require Import AAC_tactics.AAC.

Lemma sepcon'Associative: Associative eq sepcon.
Proof.
  unfold Associative.
  intros x y z.
  symmetry.
  apply sepcon_assoc.
Qed.

Lemma sepcon'Commutative: Commutative eq sepcon.
Proof.
  unfold Commutative.
  intros x y.
  apply sepcon_comm.
Qed.

Lemma sepcon'Unit_emp: Unit eq sepcon emp.
Proof.
  constructor; intros x.
  apply emp_sepcon.
  apply sepcon_emp.
Qed.

#[export] Instance sepcon'aac_assoc : Associative eq sepcon := sepcon'Associative.
#[export] Instance sepcon'aac_comm : Commutative eq sepcon := sepcon'Commutative.
#[export] Instance sepcon'aac_emp_Unit : Unit eq sepcon emp := sepcon'Unit_emp.

Example Fast: forall {cs : compspecs} (sh : Share.t) (t : type) (gfs1 : list gfield) (v : reptype (nested_field_type t gfs1)) (p : val),
  field_at sh t gfs1 v p = (field_at sh t gfs1 v p * emp)%logic.
Proof.
  intros.
  rewrite sepcon_emp.
  reflexivity.
Time Qed. 

Example Slow: forall {cs : compspecs} (sh : Share.t) (t : type) (gfs1 : list gfield) (v : reptype (nested_field_type t gfs1)) (p : val),
  field_at sh t gfs1 v p = (field_at sh t gfs1 v p * emp)%logic.
Proof.
  intros.
  aac_reflexivity.
Timeout 10 Qed.

Coq.find_constant uses two deprecated functions (UnivGen.constr_of_global and Coqlib.find_reference).

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit 0739fe9
on branch https://github.com/coq-community/aac-tactics/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!

CC: coq/coq#12334

AAC tactics apparently don't handle goal selectors properly.

This might be an effect of #36.

Here is an example:

From Coq Require PeanoNat ZArith List Permutation Lia.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.

(** ** Introductory example 

   Here is a first example with relative numbers ([Z]): one can
   rewrite an universally quantified hypothesis modulo the
   associativity and commutativity of [Z.add]. *)

Section introduction.
  Import ZArith.
  Import Instances.Z.

  Variables a b : Z.

  Goal a + b = b + a.
    aac_reflexivity.
  Qed.

  Goal forall c: bool, a + b = b + a.
    intros c.
    destruct c.
    1,2: aac_reflexivity.
  Fail Qed. (* The command has indeed failed with message: Some unresolved existential variables remain *)
  Abort.

  Goal forall c: bool, a + b = b + a.
    intros c.
    destruct c.
    - aac_reflexivity.
    - aac_reflexivity.
  Qed.
End introduction.

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.15.0.

Coq Platform CI is currently testing opam package coq-aac-tactics.8.15.0
from official repository https://coq.inria.fr/opam/released/packages/coq-aac-tactics/coq-aac-tactics.8.15.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.02, please inform us as soon as possible and before February 14, 2022!

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#193