[Pkg-ocaml-maint-commits] [alt-ergo] branch experimental/master updated (93ae5f0 -> 5f1b37b)
Ralf Treinen
treinen at moszumanska.debian.org
Tue Dec 30 18:13:00 UTC 2014
This is an automated email from the git hooks/post-receive script.
treinen pushed a change to branch experimental/master
in repository alt-ergo.
from 93ae5f0 upload to experimental
adds 231d305 upload to sid
adds 4cb6613 lib-dev package breaks/replaces alt-ergo in versions before package split
adds 4363a13 debian/watch : new site @ ocamlpro
adds 5dc7ee9 Imported Upstream version 0.95.2
adds 51132e0 Merge tag 'upstream/0.95.2'
adds 99bea10 refresh patch 0001-No-need-to-activate-debug-flag.patch
adds c2476f3 drop patch 0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch
adds fbd9f75 drop patch 0003-Fix-a-typo.patch
adds eeac213 drop patch 0004-Add-rules-and-targets-for-gui.byte.patch
adds 368bca3 drop patch 0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
adds 996dbd0 drop patch 0007-Fix-all-target.patch
adds dca871a drop patch 0009-clean-remove-META.patch
adds ba352a9 + build-dep on libzarith-ocaml-dev
adds ee16ced debian/rules : drop backup of .depends
adds e6907cc debian/rules : additional make targets for build and install
adds f920a24 drop mandir setting in invocation of ./configure
adds 15e39bf debian/rules: drop touching of configure
adds 18bc16a + changelog entry: new upstream release
adds b5daf76 fix filenamemangle in debian/watch
adds 0413dbd update debian/copyright
adds 5dff4ab install examples
adds 8524fde drop overwrite of dh_auto_configure
adds 2ca15d4 standards-version 3.9.5
adds a0fbd4f add todo
adds a257ccf Port to OCamlgraph 1.8.4 (Closes: #743072)
adds 088a28a Release to unstable
adds 7d41a30 Revert "Port to OCamlgraph 1.8.4 (Closes: #743072)"
adds f184ab2 Revert back to match OCamlgraph 1.8.5 API.
adds 5fd8c71 Release to unstable
new f4be06c debian/copyright : Files-Excluded: non-free
new da20a0b Imported Upstream version 0.99.1+dfsg1
new 1816bce Merge tag 'upstream/0.99.1+dfsg1' into experimental/master
new d12791c new upstream 0.99.1
new 476fbac debian/rules clean target : execute ony when config.status exists
new adafe15 update patch 0001-No-need-to-activate-debug-flag
new adf7037 fix Makefile.users for dropping of non-free dirfectory
new 3ae0b13 debian/rules : drop install-pack
new 14ee89e drop libalt-ergo-ocaml-dev binary package
new e61f1c9 bump standards-version
new 5f1b37b debian/watch : mangle +dfsg\d* \version suffix
The 11 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:
.depend | 263 ----
CHANGES | 43 +
COPYING | 12 -
COPYING.md | 28 +
INSTALL | 35 -
INSTALL.md | 74 ++
CeCILL-C => LICENSE | 0
Makefile | 3 +
Makefile.configurable.in | 58 +
Makefile.in | 418 ------
Makefile.users | 334 +++++
README | 36 -
README.md | 22 +
arith.ml | 592 ---------
arith.mli | 26 -
arrays.ml | 439 -------
boxed.ml | 68 -
boxed.mli | 45 -
cc.ml | 719 ----------
cnf.ml | 422 ------
cnf.mli | 29 -
combine.mli | 20 -
common.ml | 257 ----
configure | 318 +++--
configure.in | 74 +-
custom_theory.ml | 485 -------
custom_theory.mli | 34 -
debian/alt-ergo.examples | 1 +
debian/changelog | 78 ++
debian/control | 24 +-
debian/copyright | 19 +-
debian/libalt-ergo-ocaml-dev.install | 1 -
.../0001-No-need-to-activate-debug-flag.patch | 20 +-
...the-test-if-test.mlw-is-absent-and-use-be.patch | 24 -
debian/patches/0002-non-free-dropped | 35 +
debian/patches/0003-Fix-a-typo.patch | 16 -
.../0004-Add-rules-and-targets-for-gui.byte.patch | 72 -
...ma-instead-of-cmxa-for-lablgtksourceview2.patch | 42 -
debian/patches/0007-Fix-all-target.patch | 26 -
...ll-pack-into-two-separate-targets-opt-and.patch | 33 -
debian/patches/0009-clean-remove-META.patch | 17 -
debian/patches/series | 8 +-
debian/rules | 25 +-
debian/todo | 2 +
debian/watch | 3 +-
{util => doc}/gtk-lang/alt-ergo.lang | 0
examples/invalid/arith1.why | 5 +
examples/invalid/arith2.why | 4 +
examples/invalid/arrays.why | 12 +
examples/invalid/bitv.why | 7 +
examples/valid/ac_arith.why | 3 +
examples/valid/arith1.why | 9 +
examples/valid/arith2.why | 10 +
examples/valid/arith3.why | 7 +
examples/valid/arith4.why | 2 +
examples/valid/arrays.why | 12 +
examples/valid/bitv.why | 5 +
examples/valid/congruence.why | 10 +
examples/valid/enum_arrays.why | 11 +
examples/valid/quantifiers.why | 14 +
explanation.ml | 155 ---
fm.ml | 1011 --------------
frontend.ml | 260 ----
frontend.mli | 53 -
gui_replay.mli | 4 -
hashcons.mli | 129 --
incr_match.ml | 393 ------
incr_match.mli | 39 -
instantiation.ml | 470 -------
instantiation.mli | 54 -
literal.ml | 236 ----
matching.ml | 341 -----
matching.mli | 61 -
options.ml | 150 ---
parseoptions.ml | 124 --
preoptions.ml | 116 --
preoptions.mli | 96 --
pretty.ml | 66 -
pretty.mli | 25 -
print_color.ml | 208 ---
print_color.mli | 102 --
pruning.ml | 370 ------
revision.sh | 31 -
sat.ml | 636 ---------
sat.mli | 55 -
sig.mli | 238 ----
smt_to_why.ml | 273 ----
smtlib2_util.ml | 31 -
src/Makefile | 9 +
src/gui/Makefile | 9 +
gui_replay.ml => src/gui/gui_replay.ml | 30 +-
arrays.mli => src/gui/gui_replay.mli | 52 +-
gui_session.ml => src/gui/gui_session.ml | 39 +-
gui_session.mli => src/gui/gui_session.mli | 39 +-
why_annoted.ml => src/gui/why_annoted.ml | 927 +++++++------
why_annoted.mli => src/gui/why_annoted.mli | 53 +-
why_connected.ml => src/gui/why_connected.ml | 750 +++++------
why_connected.mli => src/gui/why_connected.mli | 41 +-
src/instances/Makefile | 9 +
src/instances/matching.ml | 604 +++++++++
src/instances/matching.mli | 51 +
src/main/Makefile | 9 +
src/main/frontend.ml | 237 ++++
src/main/frontend.mli | 54 +
gui.ml => src/main/main_gui.ml | 987 +++++++-------
arrays.mli => src/main/main_gui.mli | 51 +-
src/main/main_text.ml | 77 ++
bitv.mli => src/main/main_text.mli | 50 +-
src/parsing/Makefile | 9 +
src/parsing/errors.ml | 143 ++
common.mli => src/parsing/errors.mli | 63 +-
smt_lex.mll => src/parsing/smt_lex.mll | 39 +-
smt_parser.mly => src/parsing/smt_parser.mly | 39 +-
smtlib2_lex.mll => src/parsing/smtlib2_lex.mll | 44 +-
smtlib2_parse.mly => src/parsing/smtlib2_parse.mly | 39 +-
why_lexer.mll => src/parsing/why_lexer.mll | 65 +-
why_parser.mly => src/parsing/why_parser.mly | 190 ++-
src/preprocess/Makefile | 9 +
src/preprocess/cnf.ml | 258 ++++
main.ml => src/preprocess/cnf.mli | 52 +-
existantial.ml => src/preprocess/existantial.ml | 67 +-
existantial.mli => src/preprocess/existantial.mli | 39 +-
src/preprocess/pruning.ml | 375 ++++++
pruning.mli => src/preprocess/pruning.mli | 39 +-
src/preprocess/smt_to_why.ml | 276 ++++
.../preprocess/smtlib2_to_why.ml | 118 +-
triggers.ml => src/preprocess/triggers.ml | 719 +++++-----
triggers.mli => src/preprocess/triggers.mli | 40 +-
src/preprocess/why_typing.ml | 1380 +++++++++++++++++++
why_typing.mli => src/preprocess/why_typing.mli | 39 +-
src/sat/Makefile | 9 +
src/sat/sat_solvers.ml | 591 +++++++++
src/sat/sat_solvers.mli | 65 +
src/structures/Makefile | 9 +
exception.ml => src/structures/exception.ml | 39 +-
exception.mli => src/structures/exception.mli | 39 +-
src/structures/explanation.ml | 147 +++
explanation.mli => src/structures/explanation.mli | 79 +-
formula.ml => src/structures/formula.ml | 391 +++---
formula.mli => src/structures/formula.mli | 51 +-
src/structures/literal.ml | 335 +++++
literal.mli => src/structures/literal.mli | 73 +-
smt_ast.mli => src/structures/smt_ast.mli | 51 +-
smtlib2_ast.ml => src/structures/smtlib2_ast.ml | 45 +-
src/structures/smtlib2_ast.mli | 131 ++
symbols.ml => src/structures/symbols.ml | 54 +-
symbols.mli => src/structures/symbols.mli | 43 +-
term.ml => src/structures/term.ml | 161 ++-
term.mli => src/structures/term.mli | 56 +-
ty.ml => src/structures/ty.ml | 301 ++---
ty.mli => src/structures/ty.mli | 61 +-
why_ptree.mli => src/structures/why_ptree.ml | 155 ++-
why_ptree.mli => src/structures/why_ptree.mli | 64 +-
src/theories/Makefile | 9 +
ac.ml => src/theories/ac.ml | 190 +--
ac.mli => src/theories/ac.mli | 38 +-
src/theories/arith.ml | 548 ++++++++
src/theories/arith.mli | 41 +
src/theories/arrays.ml | 442 +++++++
arrays.mli => src/theories/arrays.mli | 46 +-
bitv.ml => src/theories/bitv.ml | 563 ++++----
bitv.mli => src/theories/bitv.mli | 47 +-
combine.ml => src/theories/combine.ml | 505 ++++---
src/theories/combine.mli | 29 +
src/theories/fm.ml | 1051 +++++++++++++++
fm.mli => src/theories/fm.mli | 49 +-
intervals.ml => src/theories/intervals.ml | 431 +++---
intervals.mli => src/theories/intervals.mli | 56 +-
polynome.ml => src/theories/polynome.ml | 264 ++--
polynome.mli => src/theories/polynome.mli | 68 +-
records.ml => src/theories/records.ml | 286 ++--
records.mli => src/theories/records.mli | 46 +-
src/theories/sig.mli | 136 ++
src/theories/sum.ml | 392 ++++++
sum.mli => src/theories/sum.mli | 46 +-
src/theories/theory.ml | 793 +++++++++++
cc.mli => src/theories/theory.mli | 49 +-
uf.ml => src/theories/uf.ml | 679 +++++-----
uf.mli => src/theories/uf.mli | 61 +-
src/theories/use.ml | 122 ++
use.mli => src/theories/use.mli | 65 +-
src/util/Makefile | 9 +
hashcons.ml => src/util/hashcons.ml | 68 +-
src/util/hashcons.mli | 109 ++
hstring.ml => src/util/hstring.ml | 53 +-
hstring.mli => src/util/hstring.mli | 44 +-
loc.ml => src/util/loc.ml | 45 +-
arrays.mli => src/util/loc.mli | 51 +-
src/util/numbers.ml | 165 +++
src/util/numbers.mli | 69 +
src/util/options.ml | 356 +++++
options.mli => src/util/options.mli | 229 ++--
timers.ml => src/util/timers.ml | 43 +-
timers.mli => src/util/timers.mli | 39 +-
src/util/version.ml | 3 +
src/util/version.mli | 10 +
subst.ml | 49 -
subst.mli | 37 -
sum.ml | 339 -----
use.ml | 124 --
why_typing.ml | 1390 --------------------
201 files changed, 15520 insertions(+), 16972 deletions(-)
delete mode 100644 .depend
delete mode 100644 COPYING
create mode 100644 COPYING.md
delete mode 100644 INSTALL
create mode 100644 INSTALL.md
rename CeCILL-C => LICENSE (100%)
create mode 100644 Makefile
create mode 100644 Makefile.configurable.in
delete mode 100644 Makefile.in
create mode 100644 Makefile.users
delete mode 100644 README
create mode 100644 README.md
delete mode 100644 arith.ml
delete mode 100644 arith.mli
delete mode 100644 arrays.ml
delete mode 100644 boxed.ml
delete mode 100644 boxed.mli
delete mode 100644 cc.ml
delete mode 100644 cnf.ml
delete mode 100644 cnf.mli
delete mode 100644 combine.mli
delete mode 100644 common.ml
delete mode 100644 custom_theory.ml
delete mode 100644 custom_theory.mli
create mode 100644 debian/alt-ergo.examples
delete mode 100644 debian/libalt-ergo-ocaml-dev.install
delete mode 100644 debian/patches/0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch
create mode 100644 debian/patches/0002-non-free-dropped
delete mode 100644 debian/patches/0003-Fix-a-typo.patch
delete mode 100644 debian/patches/0004-Add-rules-and-targets-for-gui.byte.patch
delete mode 100644 debian/patches/0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
delete mode 100644 debian/patches/0007-Fix-all-target.patch
delete mode 100644 debian/patches/0008-Split-install-pack-into-two-separate-targets-opt-and.patch
delete mode 100644 debian/patches/0009-clean-remove-META.patch
create mode 100644 debian/todo
rename {util => doc}/gtk-lang/alt-ergo.lang (100%)
create mode 100644 examples/invalid/arith1.why
create mode 100644 examples/invalid/arith2.why
create mode 100644 examples/invalid/arrays.why
create mode 100644 examples/invalid/bitv.why
create mode 100644 examples/valid/ac_arith.why
create mode 100644 examples/valid/arith1.why
create mode 100644 examples/valid/arith2.why
create mode 100644 examples/valid/arith3.why
create mode 100644 examples/valid/arith4.why
create mode 100644 examples/valid/arrays.why
create mode 100644 examples/valid/bitv.why
create mode 100644 examples/valid/congruence.why
create mode 100644 examples/valid/enum_arrays.why
create mode 100644 examples/valid/quantifiers.why
delete mode 100644 explanation.ml
delete mode 100644 fm.ml
delete mode 100644 frontend.ml
delete mode 100644 frontend.mli
delete mode 100644 gui_replay.mli
delete mode 100644 hashcons.mli
delete mode 100644 incr_match.ml
delete mode 100644 incr_match.mli
delete mode 100644 instantiation.ml
delete mode 100644 instantiation.mli
delete mode 100644 literal.ml
delete mode 100644 matching.ml
delete mode 100644 matching.mli
delete mode 100644 options.ml
delete mode 100644 parseoptions.ml
delete mode 100644 preoptions.ml
delete mode 100644 preoptions.mli
delete mode 100644 pretty.ml
delete mode 100644 pretty.mli
delete mode 100644 print_color.ml
delete mode 100644 print_color.mli
delete mode 100644 pruning.ml
delete mode 100755 revision.sh
delete mode 100644 sat.ml
delete mode 100644 sat.mli
delete mode 100644 sig.mli
delete mode 100644 smt_to_why.ml
delete mode 100644 smtlib2_util.ml
create mode 100644 src/Makefile
create mode 100644 src/gui/Makefile
rename gui_replay.ml => src/gui/gui_replay.ml (56%)
copy arrays.mli => src/gui/gui_replay.mli (53%)
rename gui_session.ml => src/gui/gui_session.ml (83%)
rename gui_session.mli => src/gui/gui_session.mli (64%)
rename why_annoted.ml => src/gui/why_annoted.ml (66%)
rename why_annoted.mli => src/gui/why_annoted.mli (89%)
rename why_connected.ml => src/gui/why_connected.ml (61%)
rename why_connected.mli => src/gui/why_connected.mli (65%)
create mode 100644 src/instances/Makefile
create mode 100644 src/instances/matching.ml
create mode 100644 src/instances/matching.mli
create mode 100644 src/main/Makefile
create mode 100644 src/main/frontend.ml
create mode 100644 src/main/frontend.mli
rename gui.ml => src/main/main_gui.ml (60%)
copy arrays.mli => src/main/main_gui.mli (54%)
create mode 100644 src/main/main_text.ml
copy bitv.mli => src/main/main_text.mli (54%)
create mode 100644 src/parsing/Makefile
create mode 100644 src/parsing/errors.ml
rename common.mli => src/parsing/errors.mli (62%)
rename smt_lex.mll => src/parsing/smt_lex.mll (85%)
rename smt_parser.mly => src/parsing/smt_parser.mly (90%)
rename smtlib2_lex.mll => src/parsing/smtlib2_lex.mll (77%)
rename smtlib2_parse.mly => src/parsing/smtlib2_parse.mly (92%)
rename why_lexer.mll => src/parsing/why_lexer.mll (66%)
rename why_parser.mly => src/parsing/why_parser.mly (56%)
create mode 100644 src/preprocess/Makefile
create mode 100644 src/preprocess/cnf.ml
rename main.ml => src/preprocess/cnf.mli (53%)
rename existantial.ml => src/preprocess/existantial.ml (73%)
rename existantial.mli => src/preprocess/existantial.mli (56%)
create mode 100644 src/preprocess/pruning.ml
rename pruning.mli => src/preprocess/pruning.mli (58%)
create mode 100644 src/preprocess/smt_to_why.ml
rename smtlib2_to_why.ml => src/preprocess/smtlib2_to_why.ml (88%)
rename triggers.ml => src/preprocess/triggers.ml (50%)
rename triggers.mli => src/preprocess/triggers.mli (61%)
create mode 100644 src/preprocess/why_typing.ml
rename why_typing.mli => src/preprocess/why_typing.mli (63%)
create mode 100644 src/sat/Makefile
create mode 100644 src/sat/sat_solvers.ml
create mode 100644 src/sat/sat_solvers.mli
create mode 100644 src/structures/Makefile
rename exception.ml => src/structures/exception.ml (59%)
rename exception.mli => src/structures/exception.mli (59%)
create mode 100644 src/structures/explanation.ml
rename explanation.mli => src/structures/explanation.mli (56%)
rename formula.ml => src/structures/formula.ml (58%)
rename formula.mli => src/structures/formula.mli (74%)
create mode 100644 src/structures/literal.ml
rename literal.mli => src/structures/literal.mli (54%)
rename smt_ast.mli => src/structures/smt_ast.mli (77%)
rename smtlib2_ast.ml => src/structures/smtlib2_ast.ml (87%)
create mode 100644 src/structures/smtlib2_ast.mli
rename symbols.ml => src/structures/symbols.ml (78%)
rename symbols.mli => src/structures/symbols.mli (69%)
rename term.ml => src/structures/term.ml (64%)
rename term.mli => src/structures/term.mli (64%)
rename ty.ml => src/structures/ty.ml (61%)
rename ty.mli => src/structures/ty.mli (69%)
copy why_ptree.mli => src/structures/why_ptree.ml (59%)
rename why_ptree.mli => src/structures/why_ptree.mli (83%)
create mode 100644 src/theories/Makefile
rename ac.ml => src/theories/ac.ml (61%)
rename ac.mli => src/theories/ac.mli (74%)
create mode 100644 src/theories/arith.ml
create mode 100644 src/theories/arith.mli
create mode 100644 src/theories/arrays.ml
copy arrays.mli => src/theories/arrays.mli (53%)
rename bitv.ml => src/theories/bitv.ml (63%)
rename bitv.mli => src/theories/bitv.mli (53%)
rename combine.ml => src/theories/combine.ml (58%)
create mode 100644 src/theories/combine.mli
create mode 100644 src/theories/fm.ml
rename fm.mli => src/theories/fm.mli (54%)
rename intervals.ml => src/theories/intervals.ml (66%)
rename intervals.mli => src/theories/intervals.mli (54%)
rename polynome.ml => src/theories/polynome.ml (50%)
rename polynome.mli => src/theories/polynome.mli (60%)
rename records.ml => src/theories/records.ml (65%)
rename records.mli => src/theories/records.mli (53%)
create mode 100644 src/theories/sig.mli
create mode 100644 src/theories/sum.ml
rename sum.mli => src/theories/sum.mli (53%)
create mode 100644 src/theories/theory.ml
rename cc.mli => src/theories/theory.mli (57%)
rename uf.ml => src/theories/uf.ml (51%)
rename uf.mli => src/theories/uf.mli (52%)
create mode 100644 src/theories/use.ml
rename use.mli => src/theories/use.mli (51%)
create mode 100644 src/util/Makefile
rename hashcons.ml => src/util/hashcons.ml (57%)
create mode 100644 src/util/hashcons.mli
rename hstring.ml => src/util/hstring.ml (55%)
rename hstring.mli => src/util/hstring.mli (58%)
rename loc.ml => src/util/loc.ml (54%)
rename arrays.mli => src/util/loc.mli (51%)
create mode 100644 src/util/numbers.ml
create mode 100644 src/util/numbers.mli
create mode 100644 src/util/options.ml
rename options.mli => src/util/options.mli (56%)
rename timers.ml => src/util/timers.ml (78%)
rename timers.mli => src/util/timers.mli (63%)
create mode 100644 src/util/version.ml
create mode 100644 src/util/version.mli
delete mode 100644 subst.ml
delete mode 100644 subst.mli
delete mode 100644 sum.ml
delete mode 100644 use.ml
delete mode 100644 why_typing.ml
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/alt-ergo.git
More information about the Pkg-ocaml-maint-commits
mailing list