[Pkg-ocaml-maint-commits] [coq] 02/05: Merge tag 'upstream/8.4pl3dfsg'
This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch master in repository coq. commit 58545b00a1c1825d9e51b16c2986976dd45dd3b2 Merge: bdb99a4 d2c5c5e Author: Stephane Glondu st...@glondu.net Date: Sun Jan 19 15:09:26 2014 +0100 Merge tag 'upstream/8.4pl3dfsg' Upstream version 8.4pl3dfsg CHANGES | 31 ++ README | 2 +- _tags | 4 +- configure | 38 +- ide/command_windows.ml | 10 +- ide/coq.ml | 12 +- ide/coq.mli | 2 +- ide/coqide.ml | 11 +- interp/topconstr.ml | 2 +- kernel/cbytecodes.mli | 2 +- kernel/csymtable.mli| 2 +- kernel/indtypes.ml | 7 +- kernel/indtypes.mli | 2 +- kernel/univ.ml | 2 +- lib/pp.ml4 | 1 + lib/pp.mli | 1 + library/library.ml | 2 +- myocamlbuild.ml | 8 +- parsing/lexer.ml4 | 2 +- parsing/printer.ml | 4 +- plugins/nsatz/Nsatz.v | 4 +- plugins/setoid_ring/Field_tac.v | 6 +- plugins/setoid_ring/Field_theory.v | 16 +- plugins/subtac/subtac_obligations.ml| 10 +- plugins/xml/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 26 +- pretyping/arguments_renaming.ml | 14 +- pretyping/detyping.ml | 4 +- pretyping/evarconv.ml | 63 ++- pretyping/matching.ml | 7 +- pretyping/retyping.ml | 20 +- pretyping/unification.ml| 18 +- proofs/redexpr.ml | 6 +- scripts/coqc.ml | 2 +- tactics/class_tactics.ml4 | 8 +- tactics/equality.ml | 28 +- tactics/tacinterp.ml| 4 +- test-suite/Makefile | 1 + test-suite/bugs/closed/3003.v | 12 + test-suite/bugs/closed/3023.v | 31 ++ test-suite/bugs/closed/shouldsucceed/2230.v | 6 + test-suite/bugs/closed/shouldsucceed/2837.v | 15 + test-suite/output/Arguments_renaming.out| 5 + test-suite/output/Arguments_renaming.v | 2 +- test-suite/success/Case19.v | 11 + theories/Logic/ConstructiveEpsilon.v| 2 +- tools/coqdep.ml | 13 +- tools/coqdep_boot.ml| 2 +- tools/coqdep_common.ml | 16 +- tools/coqdep_common.mli | 3 +- tools/fake_ide.ml | 16 +- toplevel/class.ml | 2 +- toplevel/coqinit.ml | 2 +- toplevel/himsg.ml | 6 +- toplevel/ide_intf.ml| 610 +--- toplevel/ide_intf.mli | 99 ++--- toplevel/ide_slave.ml | 32 +- toplevel/indschemes.ml | 2 +- toplevel/interface.mli | 125 +- toplevel/metasyntax.ml | 4 +- toplevel/mltop.ml4 | 2 +- toplevel/vernacentries.ml | 16 +- 62 files changed, 910 insertions(+), 508 deletions(-) -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] 05/05: Update README.Debian (Closes: #680248)
This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch master in repository coq. commit e3ef7f22f8ca1549633371e1f6fa14ae2e27546d Author: Stephane Glondu st...@glondu.net Date: Sun Jan 19 15:12:15 2014 +0100 Update README.Debian (Closes: #680248) --- debian/README.Debian | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/debian/README.Debian b/debian/README.Debian index 7e9997a..55825cf 100644 --- a/debian/README.Debian +++ b/debian/README.Debian @@ -14,7 +14,9 @@ Coq frontends For interactive use of coqtop, we suggest - a readline editor, such as ledit or rlwrap (or anything that provides the readline-editor virtual packages); - - or the Proof-General (x)emacs mode, available in the proofgeneral-coq + - or the Proof-General (x)emacs mode, available in the proofgeneral package. However, we recommend you to use the CoqIde GTK+ interface provided in coqide. + + -- Stéphane Glondu glo...@debian.org, Sun, 19 Jan 2014 15:11:59 +0100 -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] branch upstream updated (db38bb4 - d2c5c5e)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to branch upstream in repository coq. from db38bb4 Merge branch 'experimental/upstream' into upstream new d2c5c5e Imported Upstream version 8.4pl3dfsg The 1 revisions listed above as new are entirely new to this repository and will be described in separate emails. The revisions listed as adds were already present in the repository and have only been added to this reference. Summary of changes: CHANGES | 31 ++ README | 2 +- _tags | 4 +- configure | 38 +- ide/command_windows.ml | 10 +- ide/coq.ml | 12 +- ide/coq.mli | 2 +- ide/coqide.ml | 11 +- interp/topconstr.ml | 2 +- kernel/cbytecodes.mli | 2 +- kernel/csymtable.mli| 2 +- kernel/indtypes.ml | 7 +- kernel/indtypes.mli | 2 +- kernel/univ.ml | 2 +- lib/pp.ml4 | 1 + lib/pp.mli | 1 + library/library.ml | 2 +- myocamlbuild.ml | 8 +- parsing/lexer.ml4 | 2 +- parsing/printer.ml | 4 +- plugins/nsatz/Nsatz.v | 4 +- plugins/setoid_ring/Field_tac.v | 6 +- plugins/setoid_ring/Field_theory.v | 16 +- plugins/subtac/subtac_obligations.ml| 10 +- plugins/xml/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 26 +- pretyping/arguments_renaming.ml | 14 +- pretyping/detyping.ml | 4 +- pretyping/evarconv.ml | 63 ++- pretyping/matching.ml | 7 +- pretyping/retyping.ml | 20 +- pretyping/unification.ml| 18 +- proofs/redexpr.ml | 6 +- scripts/coqc.ml | 2 +- tactics/class_tactics.ml4 | 8 +- tactics/equality.ml | 28 +- tactics/tacinterp.ml| 4 +- test-suite/Makefile | 1 + test-suite/bugs/closed/3003.v | 12 + test-suite/bugs/closed/3023.v | 31 ++ test-suite/bugs/closed/shouldsucceed/2230.v | 6 + test-suite/bugs/closed/shouldsucceed/2837.v | 15 + test-suite/output/Arguments_renaming.out| 5 + test-suite/output/Arguments_renaming.v | 2 +- test-suite/success/Case19.v | 11 + theories/Logic/ConstructiveEpsilon.v| 2 +- tools/coqdep.ml | 13 +- tools/coqdep_boot.ml| 2 +- tools/coqdep_common.ml | 16 +- tools/coqdep_common.mli | 3 +- tools/fake_ide.ml | 16 +- toplevel/class.ml | 2 +- toplevel/coqinit.ml | 2 +- toplevel/himsg.ml | 6 +- toplevel/ide_intf.ml| 610 +--- toplevel/ide_intf.mli | 99 ++--- toplevel/ide_slave.ml | 32 +- toplevel/indschemes.ml | 2 +- toplevel/interface.mli | 125 +- toplevel/metasyntax.ml | 4 +- toplevel/mltop.ml4 | 2 +- toplevel/vernacentries.ml | 16 +- 62 files changed, 910 insertions(+), 508 deletions(-) create mode 100644 test-suite/bugs/closed/3003.v create mode 100644 test-suite/bugs/closed/3023.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2230.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2837.v -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] annotated tag upstream/8.4pl3dfsg created (now 6980791)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to annotated tag upstream/8.4pl3dfsg in repository coq. at 6980791 (tag) tagging d2c5c5e616a6e118291fe1ce9965c731adac03a8 (commit) replaces upstream/8.4pl2dfsg tagged by Stephane Glondu on Sun Jan 19 15:09:26 2014 +0100 - Log - Upstream version 8.4pl3dfsg Stephane Glondu (4): Imported Upstream version 8.3.pl4 Remove non-DFSG contents Merge branch 'experimental/upstream' into upstream Imported Upstream version 8.4pl3dfsg --- No new revisions were added by this update. -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] branch master updated (bdb99a4 - e3ef7f2)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to branch master in repository coq. from bdb99a4 Prepare upload to unstable new d2c5c5e Imported Upstream version 8.4pl3dfsg new 58545b0 Merge tag 'upstream/8.4pl3dfsg' new 4d459d5 New upstream release new fc0c747 Update ABI new e3ef7f2 Update README.Debian (Closes: #680248) The 5 revisions listed above as new are entirely new to this repository and will be described in separate emails. The revisions listed as adds were already present in the repository and have only been added to this reference. Summary of changes: CHANGES | 31 ++ README | 2 +- _tags | 4 +- configure | 38 +- debian/README.Debian| 4 +- debian/changelog| 6 + debian/rules| 2 +- ide/command_windows.ml | 10 +- ide/coq.ml | 12 +- ide/coq.mli | 2 +- ide/coqide.ml | 11 +- interp/topconstr.ml | 2 +- kernel/cbytecodes.mli | 2 +- kernel/csymtable.mli| 2 +- kernel/indtypes.ml | 7 +- kernel/indtypes.mli | 2 +- kernel/univ.ml | 2 +- lib/pp.ml4 | 1 + lib/pp.mli | 1 + library/library.ml | 2 +- myocamlbuild.ml | 8 +- parsing/lexer.ml4 | 2 +- parsing/printer.ml | 4 +- plugins/nsatz/Nsatz.v | 4 +- plugins/setoid_ring/Field_tac.v | 6 +- plugins/setoid_ring/Field_theory.v | 16 +- plugins/subtac/subtac_obligations.ml| 10 +- plugins/xml/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 26 +- pretyping/arguments_renaming.ml | 14 +- pretyping/detyping.ml | 4 +- pretyping/evarconv.ml | 63 ++- pretyping/matching.ml | 7 +- pretyping/retyping.ml | 20 +- pretyping/unification.ml| 18 +- proofs/redexpr.ml | 6 +- scripts/coqc.ml | 2 +- tactics/class_tactics.ml4 | 8 +- tactics/equality.ml | 28 +- tactics/tacinterp.ml| 4 +- test-suite/Makefile | 1 + test-suite/bugs/closed/3003.v | 12 + test-suite/bugs/closed/3023.v | 31 ++ test-suite/bugs/closed/shouldsucceed/2230.v | 6 + test-suite/bugs/closed/shouldsucceed/2837.v | 15 + test-suite/output/Arguments_renaming.out| 5 + test-suite/output/Arguments_renaming.v | 2 +- test-suite/success/Case19.v | 11 + theories/Logic/ConstructiveEpsilon.v| 2 +- tools/coqdep.ml | 13 +- tools/coqdep_boot.ml| 2 +- tools/coqdep_common.ml | 16 +- tools/coqdep_common.mli | 3 +- tools/fake_ide.ml | 16 +- toplevel/class.ml | 2 +- toplevel/coqinit.ml | 2 +- toplevel/himsg.ml | 6 +- toplevel/ide_intf.ml| 610 +--- toplevel/ide_intf.mli | 99 ++--- toplevel/ide_slave.ml | 32 +- toplevel/indschemes.ml | 2 +- toplevel/interface.mli | 125 +- toplevel/metasyntax.ml | 4 +- toplevel/mltop.ml4 | 2 +- toplevel/vernacentries.ml | 16 +- 65 files changed, 920 insertions(+), 510 deletions(-) create mode 100644 test-suite/bugs/closed/3003.v create mode 100644 test-suite/bugs/closed/3023.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2230.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2837.v -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] 01/01: pristine-tar data for coq_8.4pl3dfsg.orig.tar.gz
This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch pristine-tar in repository coq. commit bf00afb369c7e411c853a58a4ce315591f0f Author: Stephane Glondu st...@glondu.net Date: Sun Jan 19 15:09:25 2014 +0100 pristine-tar data for coq_8.4pl3dfsg.orig.tar.gz --- coq_8.4pl3dfsg.orig.tar.gz.delta | Bin 0 - 60701 bytes coq_8.4pl3dfsg.orig.tar.gz.id| 1 + 2 files changed, 1 insertion(+) diff --git a/coq_8.4pl3dfsg.orig.tar.gz.delta b/coq_8.4pl3dfsg.orig.tar.gz.delta new file mode 100644 index 000..994fca5 Binary files /dev/null and b/coq_8.4pl3dfsg.orig.tar.gz.delta differ diff --git a/coq_8.4pl3dfsg.orig.tar.gz.id b/coq_8.4pl3dfsg.orig.tar.gz.id new file mode 100644 index 000..b20e6d3 --- /dev/null +++ b/coq_8.4pl3dfsg.orig.tar.gz.id @@ -0,0 +1 @@ +7b000ad50dcc45ff1c63768a983cded1e23a07ca -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] branch pristine-tar updated (14c75b1 - bf00ccc)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to branch pristine-tar in repository coq. from 14c75b1 pristine-tar data for coq_8.4pl2dfsg.orig.tar.gz new bf00ccc pristine-tar data for coq_8.4pl3dfsg.orig.tar.gz The 1 revisions listed above as new are entirely new to this repository and will be described in separate emails. The revisions listed as adds were already present in the repository and have only been added to this reference. Summary of changes: coq_8.4pl3dfsg.orig.tar.gz.delta | Bin 0 - 60701 bytes coq_8.4pl3dfsg.orig.tar.gz.id| 1 + 2 files changed, 1 insertion(+) create mode 100644 coq_8.4pl3dfsg.orig.tar.gz.delta create mode 100644 coq_8.4pl3dfsg.orig.tar.gz.id -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] branch master updated (e3ef7f2 - 100dfc2)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to branch master in repository coq. from e3ef7f2 Update README.Debian (Closes: #680248) new 100dfc2 Update changelog and prepare upload to unstable The 1 revisions listed above as new are entirely new to this repository and will be described in separate emails. The revisions listed as adds were already present in the repository and have only been added to this reference. Summary of changes: debian/changelog | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] 01/01: Update changelog and prepare upload to unstable
This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch master in repository coq. commit 100dfc287ad57a3245eea312f7aa95c49f8e2a34 Author: Stephane Glondu st...@glondu.net Date: Sun Jan 19 15:12:59 2014 +0100 Update changelog and prepare upload to unstable --- debian/changelog | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/debian/changelog b/debian/changelog index e7ca1a7..31e1770 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,8 +1,9 @@ -coq (8.4pl3dfsg-1) UNRELEASED; urgency=medium +coq (8.4pl3dfsg-1) unstable; urgency=medium * New upstream release + * Update README.Debian (Closes: #680248) - -- Stéphane Glondu glo...@debian.org Sun, 19 Jan 2014 15:09:31 +0100 + -- Stéphane Glondu glo...@debian.org Sun, 19 Jan 2014 16:16:36 +0100 coq (8.4pl2dfsg-4) unstable; urgency=low -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [coq] annotated tag debian/8.4pl3dfsg-1 created (now 2b3c523)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to annotated tag debian/8.4pl3dfsg-1 in repository coq. at 2b3c523 (tag) tagging 100dfc287ad57a3245eea312f7aa95c49f8e2a34 (commit) replaces debian/8.4pl2dfsg-4 tagged by Stephane Glondu on Sun Jan 19 17:31:46 2014 +0100 - Log - coq Debian release 8.4pl3dfsg-1 -BEGIN PGP SIGNATURE- Version: GnuPG v1 iQIcBAABCgAGBQJS2/3yAAoJEHhT2k1JiBrTAU8P/0sHdn3TUERtU/Z7Hl9ABIZj ZT0Z3sMNVfTuGuu9meH2O6X0ecGoAVvc+OKPyvuyEYlNazKwsdw14gEjfv9LFFlA bLAPJUxrVvCQ+BDLwTYwXtbOMHfjZEf7Br1wGUqFcgfeacrXysrp8QFInA996yMH qLqUGPSKh3wPeR/HOnlNpdIU4vzErViHht6nVz75juO2lr/hy5SIjCLQXC1Z9LZP dVoQaY8rpslQH57xhIWFx+rBt59j3cQrMUW7q24oqtVCzYJApTbB3sfpnYLZKDC5 EIjdwVfblPJj97TSy94lL6ZHk8Zf3F9Lbkbr4eeMiWrsBYnFokFQuRSf1n/Ypnrf UjjdFxQyhdsthOk93AectIw7grSDSqHCX5GGAkli+deirlJlXfmnjeRSP0ybC8nU 6N+3P5OVTfEPeQT15N03eVmAhTXn++QNgHnQEJaM9Aean/6oALRAoIucoawUaBYA xGeyUyNDlf4kxJJ1XrraqU19tFmjE3DqGlH3BVfqozJHKwpmCf4eww+byUbjw4Og R2AeApZlAV5QpPgtG2SUIMvjUFwzvO1xumUb+N413XnESUDuhQ0e2mD8I2/8rd6u BvORph/Rs5sE9b9+gmWTTr3Z7qeaKLbbuiN+zlth+n4L4pJ2P9TbKCEdgWkAOGpN Pho4wSvdXIDsCn2U0yGe =sOtW -END PGP SIGNATURE- Stephane Glondu (6): Imported Upstream version 8.4pl3dfsg Merge tag 'upstream/8.4pl3dfsg' New upstream release Update ABI Update README.Debian (Closes: #680248) Update changelog and prepare upload to unstable --- No new revisions were added by this update. -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [why] 03/03: package tests with alt-ergo, cvc3
This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch master
in repository why.
commit b50d5aa0a0f77abce9798be7d801634719de392b
Author: Ralf Treinen trei...@free.fr
Date: Sun Jan 19 20:08:10 2014 +0100
package tests with alt-ergo, cvc3
---
debian/changelog | 3 ++-
debian/control | 1 +
debian/tests/control | 7 +++
debian/tests/why+alt-ergo| 21 +
debian/tests/why+cvc3| 20
debian/tests/why/gauss.why | 18 ++
debian/tests/why/minimum.why | 4
debian/tests/why/racine.why | 20
8 files changed, 93 insertions(+), 1 deletion(-)
diff --git a/debian/changelog b/debian/changelog
index ad2c0a2..d6e0b46 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -17,8 +17,9 @@ why (2.33-1) unstable; urgency=low
alt-ergo, coq
* Add myself to uploaders.
* Standards-Version 3.9.5 (no change)
+ * Add DEP8-style package tests for why with alt-ergo, and why with cvc3.
- -- Ralf Treinen trei...@debian.org Fri, 17 Jan 2014 20:36:07 +0100
+ -- Ralf Treinen trei...@debian.org Sun, 19 Jan 2014 20:07:21 +0100
why (2.30+dfsg-5) unstable; urgency=low
diff --git a/debian/control b/debian/control
index 125751d..b95eba3 100644
--- a/debian/control
+++ b/debian/control
@@ -24,6 +24,7 @@ Standards-Version: 3.9.5
Homepage: http://why.lri.fr/
Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/why.git
Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/why.git
+XS-Testsuite: autopkgtest
Package: why
Architecture: any
diff --git a/debian/tests/control b/debian/tests/control
new file mode 100644
index 000..f09e8f9
--- /dev/null
+++ b/debian/tests/control
@@ -0,0 +1,7 @@
+Tests: why+alt-ergo
+Depends: @, alt-ergo
+Restrictions: allow-stderr
+
+Tests: why+cvc3
+Depends: @, cvc3
+Restrictions: allow-stderr
diff --git a/debian/tests/why+alt-ergo b/debian/tests/why+alt-ergo
new file mode 100755
index 000..fb99ab9
--- /dev/null
+++ b/debian/tests/why+alt-ergo
@@ -0,0 +1,21 @@
+#!/bin/sh
+
+set -e
+
+indir=debian/tests/why
+outdir=${TMPDIR-/tmp}
+
+# alt-ergo cannot prove the VC of racine :-(
+for infile in $indir/minimum.why $indir/gauss.why
+do
+base=$(basename $infile)
+echo Testing why + alt-ergo on $base 2
+whyoutfile=$outdir/${base%.why}_why.why
+altoutfile=$outdir/${base%.why}.ae
+why --alt-ergo --output $whyoutfile $infile
+alt-ergo $whyoutfile $altoutfile
+if $(grep -qv Valid $altoutfile); then
+ cat $altoutfile
+ exit 1
+fi
+done
\ No newline at end of file
diff --git a/debian/tests/why+cvc3 b/debian/tests/why+cvc3
new file mode 100755
index 000..6df7332
--- /dev/null
+++ b/debian/tests/why+cvc3
@@ -0,0 +1,20 @@
+#!/bin/sh
+
+set -e
+
+indir=debian/tests/why
+outdir=${TMPDIR-/tmp}
+
+for infile in $indir/*.why
+do
+base=$(basename $infile)
+echo Testing why + cvc3 on $base 2
+whyoutfile=$outdir/${base%.why}_why.cvc
+cvcoutfile=$outdir/${base%.why}.cvcout
+why --cvcl --output $whyoutfile $infile
+cvc3 $whyoutfile $cvcoutfile
+if $(grep -qv Valid $cvcoutfile); then
+ cat $cvcoutfile
+ exit 1
+fi
+done
\ No newline at end of file
diff --git a/debian/tests/why/gauss.why b/debian/tests/why/gauss.why
new file mode 100644
index 000..d6c1517
--- /dev/null
+++ b/debian/tests/why/gauss.why
@@ -0,0 +1,18 @@
+let gauss (y: int) =
+
+{y 0}
+ let x = ref 0 in
+ let z = ref 0 in
+
+ while ( !z y) do
+
+ {invariant z = y and 2*x = z*(z+1)}
+
+ z := !z + 1;
+ x := !x + !z
+
+ done;
+
+ !x
+
+{2*result = y*(y+1)}
diff --git a/debian/tests/why/minimum.why b/debian/tests/why/minimum.why
new file mode 100644
index 000..602e478
--- /dev/null
+++ b/debian/tests/why/minimum.why
@@ -0,0 +1,4 @@
+logic min: int, int - int
+axiom min_ax: forall x,y:int. min(x,y) = x
+parameter r: int ref
+let f (n:int) = r := min !r n { r = r@ }
diff --git a/debian/tests/why/racine.why b/debian/tests/why/racine.why
new file mode 100644
index 000..1d5f525
--- /dev/null
+++ b/debian/tests/why/racine.why
@@ -0,0 +1,20 @@
+let racine (x: int) =
+{x = 0}
+
+ let y1 = ref 0 in
+ let y2 = ref 1 in
+ let y3 = ref 1 in
+
+ while ( !y3 = x) do
+
+ {invariant y2 = 2*y1+1 and y3 = (y1+1)*(y1+1) and y1*y1 = x}
+
+ y1 := !y1 + 1;
+ y2 := !y2 + 2;
+ y3 := !y3 + !y2
+
+ done;
+
+ !y1
+
+{result*result=x and (result+1)*(result+1)x}
--
Alioth's /usr/local/bin/git-commit-notice on
/srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git
___
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [why] 01/03: accept coq 8.4pl3
This is an automated email from the git hooks/post-receive script. treinen pushed a commit to branch master in repository why. commit 38c7821b307fe832b02f699dbbd99acaa9e7173d Author: Ralf Treinen trei...@free.fr Date: Sun Jan 19 18:10:58 2014 +0100 accept coq 8.4pl3 --- debian/patches/atp-versions | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/debian/patches/atp-versions b/debian/patches/atp-versions index a9990b9..2862e35 100644 --- a/debian/patches/atp-versions +++ b/debian/patches/atp-versions @@ -19,7 +19,7 @@ Index: why/tools/dpConfig.ml versions_ok = [8.0; 8.1;8.2;8.2pl1; 8.3pl1; 8.3pl2;8.3pl3; 8.3pl4; - 8.4]; -+ 8.4; 8.4pl2]; ++ 8.4; 8.4pl2; 8.4pl3]; versions_old = [7.4]; command = coqc; command_switches = ; -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [why] 02/03: close bug #707585 (FTBFS)
This is an automated email from the git hooks/post-receive script. treinen pushed a commit to branch master in repository why. commit 8698f7bc248e270f99d6755ae51e93117f7bdd41 Author: Ralf Treinen trei...@free.fr Date: Sun Jan 19 18:23:41 2014 +0100 close bug #707585 (FTBFS) --- debian/changelog | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/debian/changelog b/debian/changelog index ae76300..ad2c0a2 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,6 +1,7 @@ why (2.33-1) unstable; urgency=low - * New upstream release. + * New upstream release. This fixes an issue with compilation under +ocaml-4.01 (closes: #707585). Drop patches adopted or otherwise fixed by upstream: - 0001-Why-2.29-do-support-Coq-8.3.patch - 0002-Mark-alt-ergo-0.93-as-compatible.patch -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [why] branch master updated (740a5af - b50d5aa)
This is an automated email from the git hooks/post-receive script. treinen pushed a change to branch master in repository why. from 740a5af accept alt-ergo 0.95.2, coq 8.4pl2 new 38c7821 accept coq 8.4pl3 new 8698f7b close bug #707585 (FTBFS) new b50d5aa package tests with alt-ergo, cvc3 The 3 revisions listed above as new are entirely new to this repository and will be described in separate emails. The revisions listed as adds were already present in the repository and have only been added to this reference. Summary of changes: debian/changelog | 6 -- debian/control | 1 + debian/patches/atp-versions | 2 +- debian/tests/control | 7 +++ debian/tests/why+alt-ergo| 21 + debian/tests/why+cvc3| 20 debian/tests/why/gauss.why | 18 ++ debian/tests/why/minimum.why | 4 debian/tests/why/racine.why | 20 9 files changed, 96 insertions(+), 3 deletions(-) create mode 100644 debian/tests/control create mode 100755 debian/tests/why+alt-ergo create mode 100755 debian/tests/why+cvc3 create mode 100644 debian/tests/why/gauss.why create mode 100644 debian/tests/why/minimum.why create mode 100644 debian/tests/why/racine.why -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [aac-tactics] annotated tag debian/0.4-2 created (now 541008d)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to annotated tag debian/0.4-2 in repository aac-tactics. at 541008d (tag) tagging 09c08cc6fe8bd98780f64d4931305dc670d454fd (commit) replaces debian/0.4-1 tagged by Stephane Glondu on Mon Jan 20 08:29:02 2014 +0100 - Log - aac-tactics Debian release 0.4-2 -BEGIN PGP SIGNATURE- Version: GnuPG v1 iQIcBAABCgAGBQJS3NA+AAoJEHhT2k1JiBrTg7IQAKb+eV9MhkjYTjfomikn4i2d JbnsthjTpYlmMjFXRy8pXFfZSO1pqkg+mnNNv6ivPaglsNlR5XgxrSSDrZjlKaaR jcC+gYfk+gaGQDcziB+Yo5zdUA16AAPsu3xFzCa3yrWfFF/HVDX+1uZlpNbdAj02 b0L4kTxq/Y27QIje3J6aiRI6CHGnii62TMonzQTy9JHOChdBBz1j1s1Si2WoQ8ZW E8cmmC+W+uaVaEcHYmhUZaMbJJM2QmSTKbmzrqD7wycU+Ls66SuZDyzRpVQ+G7Aj dZxd5kiQfpoxapvRxR9tLElLSv1kG4hi963Sb6GhxOaXJbFL3GPLoGugYD+PK9oF Hn9ZUtuAbe76P38rA7nXGruQQHK9kYga9pej2oye4Dcu7cY5X+/MoRq2F8jihaZn 6OHOJ3gLC0u/VwVH/FqflnWlT8cQx4f+SB8ygLYwVz18eL7SuwB+14qq9+7hAWAD 30eQad6T4kqiT7bxuMK0AZGuB+PdA8lcacmGU9Kr+zXPvoqf/m6cOeMr+3z80HSQ l0ydesEzpPapvkUgIUI5Xk10/f804J4DsSeqCyTMiOpJ17AA8Uxld4ug8HiZ+dW0 xh3X7RtSw4lVZ5/apUXcX5bgBtrczlJsyzMaP8NLaTiHBCLB1x9SVAkqAm9SJyHk iOTtpda1KO7e3n1Ehzr4 =CRsN -END PGP SIGNATURE- Stephane Glondu (3): Bump Standards-Version to 3.9.5 (no changes) Update Vcs-* Update changelog and prepare upload to unstable --- No new revisions were added by this update. -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [aac-tactics] branch master updated (b150377 - 09c08cc)
This is an automated email from the git hooks/post-receive script. glondu pushed a change to branch master in repository aac-tactics. from b150377 Prepare upload to unstable new 912dbce Bump Standards-Version to 3.9.5 (no changes) new 50c6d2f Update Vcs-* new 09c08cc Update changelog and prepare upload to unstable The 3 revisions listed above as new are entirely new to this repository and will be described in separate emails. The revisions listed as adds were already present in the repository and have only been added to this reference. Summary of changes: debian/changelog | 8 debian/control | 6 +++--- 2 files changed, 11 insertions(+), 3 deletions(-) -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [aac-tactics] 01/03: Bump Standards-Version to 3.9.5 (no changes)
This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch master in repository aac-tactics. commit 912dbce4c453004cbc22bc1c319077fd39a0756a Author: Stephane Glondu st...@glondu.net Date: Mon Jan 20 07:38:26 2014 +0100 Bump Standards-Version to 3.9.5 (no changes) --- debian/control | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/debian/control b/debian/control index 291727b..91638d2 100644 --- a/debian/control +++ b/debian/control @@ -9,7 +9,7 @@ Build-Depends: ocaml-nox (= 3.11.1-3~), coq (= 8.4dfsg-2~), libcoq-ocaml-dev -Standards-Version: 3.9.4 +Standards-Version: 3.9.5 Homepage: http://sardes.inrialpes.fr/~braibant/aac_tactics/ Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/aac-tactics.git Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [aac-tactics] 03/03: Update changelog and prepare upload to unstable
This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch master in repository aac-tactics. commit 09c08cc6fe8bd98780f64d4931305dc670d454fd Author: Stephane Glondu st...@glondu.net Date: Mon Jan 20 07:38:40 2014 +0100 Update changelog and prepare upload to unstable --- debian/changelog | 8 1 file changed, 8 insertions(+) diff --git a/debian/changelog b/debian/changelog index a35e1d9..755c979 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,11 @@ +aac-tactics (0.4-2) unstable; urgency=medium + + * Recompile with coq 8.4pl3 + * Bump Standards-Version to 3.9.5 (no changes) + * Update Vcs-* + + -- Stéphane Glondu glo...@debian.org Mon, 20 Jan 2014 08:22:59 +0100 + aac-tactics (0.4-1) unstable; urgency=low * New upstream release -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
