[abhishek@optiplex pgissue]$ docker pull coqorg/coq:dev
dev: Pulling from coqorg/coq
Digest: sha256:899313bc37793a226d88996dfe14189e6a3c25396ce2fce5d24a7910206fd7af
Status: Image is up to date for coqorg/coq:dev
docker.io/coqorg/coq:dev
[abhishek@optiplex pgissue]$ docker run --name coqaac -d -ti coqorg/coq:dev
99313f5cc7b0f4b293d589f5ba7f0054c3d1357e41f7574ded2aee3afd86cbff
[abhishek@optiplex pgissue]$ docker exec coqaac git clone https://github.com/coq-community/aac-tactics
Cloning into 'aac-tactics'...
[abhishek@optiplex pgissue]$ docker exec -w /home/coq/aac-tactics coqaac /bin/bash -c "source ~/.profile && make"
coq_makefile -f _CoqProject -o Makefile.coq
make[1]: Entering directory '/home/coq/aac-tactics'
COQDEP VFILES
COQPP src/aac.mlg
CAMLDEP src/aac_rewrite.mli
CAMLDEP src/print.mli
CAMLDEP src/theory.mli
CAMLDEP src/matcher.mli
CAMLDEP src/search_monad.mli
CAMLDEP src/helper.mli
CAMLDEP src/coq.mli
OCAMLLIBDEP src/aac_plugin.mlpack
CAMLDEP src/aac_rewrite.ml
CAMLDEP src/print.ml
CAMLDEP src/theory.ml
CAMLDEP src/matcher.ml
CAMLDEP src/search_monad.ml
CAMLDEP src/helper.ml
CAMLDEP src/coq.ml
CAMLDEP src/aac.ml
COQC theories/Utils.v
COQC theories/Constants.v
CAMLC -c src/coq.mli
CAMLOPT -c -for-pack Aac_plugin src/coq.ml
CAMLC -c src/helper.mli
CAMLOPT -c -for-pack Aac_plugin src/helper.ml
CAMLC -c src/search_monad.mli
CAMLOPT -c -for-pack Aac_plugin src/search_monad.ml
CAMLC -c src/matcher.mli
CAMLOPT -c -for-pack Aac_plugin src/matcher.ml
CAMLC -c src/theory.mli
CAMLOPT -c -for-pack Aac_plugin src/theory.ml
CAMLC -c src/print.mli
CAMLOPT -c -for-pack Aac_plugin src/print.ml
CAMLC -c src/aac_rewrite.mli
CAMLOPT -c -for-pack Aac_plugin src/aac_rewrite.ml
CAMLOPT -c -for-pack Aac_plugin src/aac.ml
CAMLOPT -pack -o src/aac_plugin.cmx
CAMLOPT -a -o src/aac_plugin.cmxa
CAMLOPT -shared -o src/aac_plugin.cmxs
COQC theories/AAC.v
COQC theories/Instances.v
COQC theories/Tutorial.v
All solutions:
occurrence 0: transitivity through forall x : X, plus x x
1 possible(s) substitution(s)
0: [x: f (a + a); ]
occurrence 1: transitivity through forall x : X,
plus (f (x + x)) (f (a + a))
1 possible(s) substitution(s)
0: [x: a; ]
All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
3 possible(s) substitution(s)
0: [x: c; y: dot (d * c) d; ]
1: [x: dot c d; y: dot c d; ]
2: [x: dot (c * d) c; y: d; ]
All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
4 possible(s) substitution(s)
0: [x: c; y: dot (d * c * d) b; ]
1: [x: dot c d; y: dot (c * d) b; ]
2: [x: dot (c * d) c; y: dot d b; ]
3: [x: dot (c * d * c) d; y: b; ]
occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b
3 possible(s) substitution(s)
0: [x: c; y: dot (d * c) d; ]
1: [x: dot c d; y: dot c d; ]
2: [x: dot (c * d) c; y: d; ]
All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
1 possible(s) substitution(s)
0: [x: plus (c * d) (c * d); y: b; ]
All solutions:
occurrence 0: transitivity through forall x : X, dot (a * x) a
1 possible(s) substitution(s)
0: [x: 1; ]
All solutions:
occurrence 0: transitivity through forall x y z : X,
plus (x * y + x * z) (a * b)
2 possible(s) substitution(s)
0: [x: a; y: c; z: dot b c; ]
1: [x: a; y: dot b c; z: c; ]
occurrence 1: transitivity through forall x y z : X,
plus (x * y + x * z) (a * c)
2 possible(s) substitution(s)
0: [x: a; y: dot b c; z: b; ]
1: [x: a; y: b; z: dot b c; ]
occurrence 2: transitivity through forall x y z : X,
plus (x * y + x * z) (a * b * c)
2 possible(s) substitution(s)
0: [x: a; y: c; z: b; ]
1: [x: a; y: b; z: c; ]
File "./theories/Tutorial.v", line 227, characters 6-24:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z)
6 possible(s) substitution(s)
0: [x: 1; y: dot a (b * c + c); z: dot a b; ]
1: [x: a; y: plus (b * c) c; z: b; ]
2: [x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ]
3: [x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ]
4: [x: 1; y: dot a b; z: dot a (b * c + c); ]
5: [x: a; y: b; z: plus (b * c) c; ]
occurrence 1: transitivity through forall x y z : X,
plus (x * y + x * z) (a * b)
2 possible(s) substitution(s)
0: [x: 1; y: dot a (b * c + c); z: 0; ]
1: [x: 1; y: 0; z: dot a (b * c + c); ]
occurrence 2: transitivity through forall x y z : X,
plus (a * (x * y + x * z)) (a * b)
4 possible(s) substitution(s)
0: [x: 1; y: dot b c; z: c; ]
1: [x: 1; y: 0; z: plus (b * c) c; ]
2: [x: 1; y: plus (b * c) c; z: 0; ]
3: [x: 1; y: c; z: dot b c; ]
occurrence 3: transitivity through forall x y z : X,
plus (a * (x * y + x * z + c)) (a * b)
2 possible(s) substitution(s)
0: [x: 1; y: dot b c; z: 0; ]
1: [x: 1; y: 0; z: dot b c; ]
occurrence 4: transitivity through forall x y z : X,
plus (x * y + x * z) (a * (b * c + c))
2 possible(s) substitution(s)
0: [x: 1; y: dot a b; z: 0; ]
1: [x: 1; y: 0; z: dot a b; ]
occurrence 5: transitivity through forall x y z : X,
plus (a * (b * (x * y + x * z) + c))
(a * b)
2 possible(s) substitution(s)
0: [x: 1; y: c; z: 0; ]
1: [x: 1; y: 0; z: c; ]
occurrence 6: transitivity through forall x y z : X,
plus (a * ((x * y + x * z) * c + c))
(a * b)
2 possible(s) substitution(s)
0: [x: 1; y: b; z: 0; ]
1: [x: 1; y: 0; z: b; ]
occurrence 7: transitivity through forall x y z : X,
plus (a * (x * y + x * z + b * c))
(a * b)
2 possible(s) substitution(s)
0: [x: 1; y: c; z: 0; ]
1: [x: 1; y: 0; z: c; ]
occurrence 8: transitivity through forall x y z : X,
plus ((x * y + x * z) * (b * c + c))
(a * b)
2 possible(s) substitution(s)
0: [x: 1; y: a; z: 0; ]
1: [x: 1; y: 0; z: a; ]
occurrence 9: transitivity through forall x y z : X,
plus (a * (x * y + x * z))
(a * (b * c + c))
2 possible(s) substitution(s)
0: [x: 1; y: b; z: 0; ]
1: [x: 1; y: 0; z: b; ]
occurrence 10: transitivity through forall x y z : X,
plus ((x * y + x * z) * b)
(a * (b * c + c))
2 possible(s) substitution(s)
0: [x: 1; y: a; z: 0; ]
1: [x: 1; y: 0; z: a; ]
occurrence 11: transitivity through plus (a * (b * c + c) + a * b)
(1 * 0 + 1 * 0)
occurrence 12: transitivity through
plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0)))
occurrence 13: transitivity through
plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b)
occurrence 14: transitivity through
plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0)))
occurrence 15: transitivity through
plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0))))
occurrence 16: transitivity through
plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c))
occurrence 17: transitivity through
plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c))
occurrence 18: transitivity through
plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1)
occurrence 19: transitivity through
plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1)))
occurrence 20: transitivity through
plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b)
occurrence 21: transitivity through
plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1)))
occurrence 22: transitivity through
plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1))))
occurrence 23: transitivity through
plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c))
occurrence 24: transitivity through
plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c))
occurrence 25: transitivity through
plus (a * (b * c + c)) ((1 * 1 + 1 * 0) * (a * b))
occurrence 26: transitivity through
plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0))
occurrence 27: transitivity through
plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b))
occurrence 28: transitivity through
plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c)))
occurrence 29: transitivity through
plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0))
occurrence 30: transitivity through
plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c))
occurrence 31: transitivity through
plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0)))
occurrence 32: transitivity through
plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c)))
occurrence 33: transitivity through
plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0)))
occurrence 34: transitivity through
plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c)))
occurrence 35: transitivity through
plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c)))
occurrence 36: transitivity through
dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0)
occurrence 37: transitivity through
dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b)
occurrence 38: transitivity through
plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b))
occurrence 39: transitivity through
plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1))
occurrence 40: transitivity through
plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b))
occurrence 41: transitivity through
plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c)))
occurrence 42: transitivity through
plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1))
occurrence 43: transitivity through
plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c))
occurrence 44: transitivity through
plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1)))
occurrence 45: transitivity through
plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c)))
occurrence 46: transitivity through
plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1)))
occurrence 47: transitivity through
plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c)))
occurrence 48: transitivity through
plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c)))
occurrence 49: transitivity through
dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1)
occurrence 50: transitivity through
dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b)
occurrence 51: transitivity through
plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0)))
occurrence 52: transitivity through
plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b))
occurrence 53: transitivity through
plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b))
occurrence 54: transitivity through
plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0)))
occurrence 55: transitivity through
plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0))))
occurrence 56: transitivity through
plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c)))
occurrence 57: transitivity through
plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c)))
occurrence 58: transitivity through
plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c)))
occurrence 59: transitivity through
plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c)))
occurrence 60: transitivity through
plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1)))
occurrence 61: transitivity through
plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b))
occurrence 62: transitivity through
plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b))
occurrence 63: transitivity through
plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1)))
occurrence 64: transitivity through
plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1))))
occurrence 65: transitivity through
plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c)))
occurrence 66: transitivity through
plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c)))
occurrence 67: transitivity through
plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c)))
occurrence 68: transitivity through
plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c)))
All solutions:
occurrence 0: transitivity through forall x y z : nat,
Nat.max (x + y) (x + z)
2 possible(s) substitution(s)
0: [x: a; y: c; z: b; ]
1: [x: a; y: b; z: c; ]
All solutions:
occurrence 0: transitivity through forall x y z : nat,
Nat.max (x + y) (x + z)
2 possible(s) substitution(s)
0: [x: a; y: c; z: b; ]
1: [x: a; y: b; z: c; ]
File "./theories/Tutorial.v", line 419, characters 4-36:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z
occurrence 1: transitivity through
(Z.abs a + - (Z.abs b + 0))%Z
occurrence 2: transitivity through
(Z.abs a + - Z.abs (b + 0))%Z
occurrence 3: transitivity through
(- Z.abs b + Z.abs (a + 0))%Z
File "./theories/Tutorial.v", line 420, characters 4-39:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
COQC theories/Caveats.v
All solutions:
occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z
1 possible(s) substitution(s)
0: [x: a; ]
occurrence 1: transitivity through forall x : Z, (x + x + (c + - (a + a)))%Z
1 possible(s) substitution(s)
0: [x: b; ]
All solutions:
occurrence 0: transitivity through dot y 1
occurrence 1: transitivity through
dot 1 y
File "./theories/Caveats.v", line 294, characters 4-32:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 295, characters 4-35:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 315, characters 4-18:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 320, characters 4-23:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
File "./theories/Caveats.v", line 347, characters 4-21:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
occurrence 0: transitivity through (b * c + a + 0)%nat
occurrence 1: transitivity through
(a + c * (b + 0))%nat
occurrence 2: transitivity through
(a + b * (c + 0))%nat
File "./theories/Caveats.v", line 364, characters 4-28:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (a + b + c + 0)%nat
File "./theories/Caveats.v", line 366, characters 4-28:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through ((a + b + c) * 1)%nat
occurrence 1: transitivity through
(a + c + b * 1)%nat
occurrence 2: transitivity through
(c + (a + b) * 1)%nat
occurrence 3: transitivity through
(b + c + a * 1)%nat
occurrence 4: transitivity through
(a + (b + c) * 1)%nat
occurrence 5: transitivity through
(a + b + c * 1)%nat
occurrence 6: transitivity through
(b + (a + c) * 1)%nat
All solutions:
occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat
1 possible(s) substitution(s)
0: [x: a; y: b; ]
File "./theories/Caveats.v", line 384, characters 4-24:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat
1 possible(s) substitution(s)
0: [x: a; y: b; ]
occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat
occurrence 2: transitivity through
(a * b + c + a * a * (1 * 1 + 0 * 1))%nat
occurrence 3: transitivity through
(c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat
occurrence 4: transitivity through
(a * a + c + a * b * (1 * 1 + 0 * 1))%nat
occurrence 5: transitivity through
(a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat
occurrence 6: transitivity through
(a * b + a * a + c * (1 * 1 + 0 * 1))%nat
occurrence 7: transitivity through
(a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat
File "./theories/Caveats.v", line 386, characters 4-22:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat
occurrence 1: transitivity through
(a * b + c + a * a * 1)%nat
occurrence 2: transitivity through
(c + (a * b + a * a) * 1)%nat
occurrence 3: transitivity through
(a * a + c + a * b * 1)%nat
occurrence 4: transitivity through
(a * b + (a * a + c) * 1)%nat
occurrence 5: transitivity through
(a * b + a * a + c * 1)%nat
occurrence 6: transitivity through
(a * a + (a * b + c) * 1)%nat
make[1]: Leaving directory '/home/coq/aac-tactics'
[abhishek@optiplex pgissue]$ docker exec -w /home/coq/aac-tactics coqaac /bin/bash -c "source ~/.profile && make install"
make[1]: Entering directory '/home/coq/aac-tactics'
INSTALL theories/Utils.vo /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Constants.vo /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/AAC.vo /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Instances.vo /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Tutorial.vo /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Caveats.vo /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Utils.v /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Constants.v /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/AAC.v /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Instances.v /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Tutorial.v /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Caveats.v /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Utils.glob /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Constants.glob /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/AAC.glob /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Instances.glob /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Tutorial.glob /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL theories/Caveats.glob /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL src/aac_plugin.cmxs /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
INSTALL src/aac_plugin.cmxs /home/coq/.opam/4.13.1+flambda/lib/coq//user-contrib/AAC_tactics/
ocamlfind: [WARNING] No such file: /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/META
Installed /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmx
Installed /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxa
Installed /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxs
ocamlfind: [WARNING] Overwriting file /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxs
Installed /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxs
Installed /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmi
Installed /home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core//../coq-aac-tactics/META
make[2]: Entering directory '/home/coq/aac-tactics'
make[2]: Leaving directory '/home/coq/aac-tactics'
make[1]: Leaving directory '/home/coq/aac-tactics'
[abhishek@optiplex pgissue]$ docker attach coqaac
coq@99313f5cc7b0:~$ coqtop
Welcome to Coq buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (39157c3fc7c2269e619879c41dd5465613b45192)
Coq < From AAC_tactics Require Import AAC.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-aac-tactics.plugin ... done]
Coq < Lemma foo: forall X:Prop, X->X.
1 goal
============================
forall X : Prop, X -> X
foo < try aac_normalise.
foo < aac_normalize.
Toplevel input, characters 0-13:
> aac_normalize.
> ^^^^^^^^^^^^^
Error: The reference aac_normalize was not found in the current environment.
foo < aac_normalise
foo < try aac_rewrite Z.gcd_mod.
Toplevel input, characters 30-39:
> try aac_rewrite Z.gcd_mod.
> ^^^^^^^^^
Error: The reference Z.gcd_mod was not found in the current environment.
foo < Require Import ZArith.
foo < try aac_rewrite Z.gcd_mod.
foo < aac_rewrite Z.gcd_mod.
Toplevel input, characters 0-21:
> aac_rewrite Z.gcd_mod.
> ^^^^^^^^^^^^^^^^^^^^^
Error: [aac_tactics] The goal is not an applied relation
foo < -
-
Save aa755/a7ae663b196ee60f9ff4c601e76bc976 to your computer and use it in GitHub Desktop.
aac_tactics do not anymore throw despite try
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| coq@99313f5cc7b0:~/aac-tactics$ git log --stat | |
| commit 8ba7a8b2c5ce80859e9645c89ebe39c33948525c (HEAD -> master, origin/master, origin/HEAD) | |
| Author: Karl Palmskog <palmskog@gmail.com> | |
| Date: Fri Jun 21 00:04:44 2024 +0200 | |
| silence warning 67 in Dune build | |
| src/dune | 2 +- | |
| 1 file changed, 1 insertion(+), 1 deletion(-) | |
| commit aa70a2d40b4bf659cccc187b25cff03a08f5a63f | |
| Merge: 22aceb2 0e3c19e | |
| Author: Karl Palmskog <palmskog@gmail.com> | |
| Date: Sat Jun 1 15:03:18 2024 +0200 | |
| Merge pull request #143 from coq-community/canonical-ordering-master | |
| Canonical ordering for aac_normalise tactic in master | |
| commit 0e3c19eaf9cf6835f161fdce0e1857f366c41b7e | |
| Author: Karl Palmskog <palmskog@gmail.com> | |
| Date: Sat Jun 1 15:00:25 2024 +0200 | |
| fix deployment boilerplate | |
| .github/workflows/deploy-docs.yml | 2 +- | |
| 1 file changed, 1 insertion(+), 1 deletion(-) | |
| commit d56ffd3a5cd558cdc963c4b6fb711f39caa37e20 | |
| Author: Karl Palmskog <palmskog@gmail.com> | |
| Date: Sat Jun 1 14:54:33 2024 +0200 | |
| use standard changelog format | |
| CHANGELOG | 7 ------- | |
| CHANGELOG.md | 20 ++++++++++++++++++++ | |
| 2 files changed, 20 insertions(+), 7 deletions(-) | |
| commit 64ccce2380622adc2a00c3261ff23b2da6fc4664 | |
| Author: Karl Palmskog <palmskog@gmail.com> | |
| Date: Sat Jun 1 13:22:33 2024 +0200 | |
| add example by Abhishek Anand using aac_normalise_all tactic | |
| theories/Tutorial.v | 11 ++++++++++- | |
| 1 file changed, 10 insertions(+), 1 deletion(-) | |
| commit 3a1038937f54007c7427b81dfeb9e880beabfe77 | |
| Author: Damien Pous <damien.pous@ens-lyon.fr> | |
| Date: Fri May 31 17:09:07 2024 +0200 | |
| aac_normalise in * | |
| tests/aac_135.v | 4 ++++ | |
| theories/AAC.v | 7 +++++++ | |
| theories/Tutorial.v | 7 ++++++- | |
| 3 files changed, 17 insertions(+), 1 deletion(-) | |
| commit a1dcc0bc0f41c99c999fe3b38990de8ecfa4d7e0 | |
| Author: Damien Pous <damien.pous@ens-lyon.fr> | |
| Date: Fri May 31 17:03:48 2024 +0200 | |
| lcm instances for Nat, N, Z | |
| CHANGELOG | 2 +- | |
| theories/Instances.v | 19 +++++++++++++++++-- | |
| 2 files changed, 18 insertions(+), 3 deletions(-) | |
| commit b9d691bfc3cc22f7077de5a3de45bf98b5b193ad | |
| Author: Damien Pous <damien.pous@ens-lyon.fr> | |
| Date: Fri May 31 16:46:48 2024 +0200 | |
| gcd instances for Nat, N, Z | |
| CHANGELOG | 1 + | |
| theories/Instances.v | 19 +++++++++++++++++-- | |
| 2 files changed, 18 insertions(+), 2 deletions(-) | |
| commit 6efa965cfb3d87c7341a5c770a74a3c470c4d1ad | |
| Author: Damien Pous <damien.pous@ens-lyon.fr> | |
| Date: Fri May 31 16:29:36 2024 +0200 | |
| gitignore | |
| .gitignore | 1 + | |
| 1 file changed, 1 insertion(+) | |
| commit d3bc26760deeec6685ac0f06ef4fd2f2bc1e7bd0 | |
| Author: Damien Pous <damien.pous@ens-lyon.fr> | |
| Date: Fri May 31 16:28:24 2024 +0200 | |
| some tests | |
| tests/aac_135.v | 23 ++++++++++++++++------- | |
| 1 file changed, 16 insertions(+), 7 deletions(-) | |
| commit 9986913304c0e473b463c4be5433600e5d72223b | |
| Author: Damien Pous <damien.pous@ens-lyon.fr> | |
| Date: Fri May 31 16:00:59 2024 +0200 | |
| changelog | |
| CHANGELOG | 6 ++++++ | |
| 1 file changed, 6 insertions(+) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment