Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
Name: alt-ergo | Distribution: Fedora Project |
Version: 2.3.3 | Vendor: Fedora Project |
Release: 22.fc41 | Build date: Mon Aug 5 18:37:40 2024 |
Group: Unspecified | Build host: buildhw-x86-08.iad2.fedoraproject.org |
Size: 16383306 | Source RPM: alt-ergo-2.3.3-22.fc41.src.rpm |
Packager: Fedora Project | |
Url: https://alt-ergo.ocamlpro.com/ | |
Summary: Automated theorem prover including linear arithmetic |
Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on CC(X) - a congruence closure algorithm parameterized by an equational theory X. This algorithm is reminiscent of the Shostak algorithm. Currently CC(X) is instantiated by the theory of linear arithmetics. Alt-Ergo also contains a home made SAT-solver and an instantiation mechanism by which it fully supports quantifiers.
Apache-2.0 AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception
* Mon Aug 05 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-22 - Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12 * Wed Jul 17 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-21 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild * Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-20 - Rebuild for ocaml-zarith 1.14 * Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-19 - OCaml 5.2.0 ppc64le fix * Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-18 - OCaml 5.2.0 for Fedora 41 * Thu May 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-17 - Add patch to fix misplaced inline attributes * Fri Feb 02 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-17 - Rebuild for changed ocamlx(Dynlink) hash * Mon Jan 22 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-16 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild * Fri Jan 19 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-15 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild * Tue Jan 02 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-14 - Rebuild for ocaml-num and ocaml-menhir 20231231 * Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-13 - OCaml 5.1.1 + s390x code gen fix for Fedora 40 * Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-12 - OCaml 5.1.1 rebuild for Fedora 40 * Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-11 - OCaml 5.1 rebuild for Fedora 40 * Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-10 - Rebuild for ocaml-zarith 1.13 * Wed Jul 19 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-9 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild * Tue Jul 18 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-8 - Validate appdata with appstream-util * Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-8 - OCaml 5.0 rebuild for Fedora 39 * Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-7 - OCaml 5.0.0 rebuild * Fri Mar 24 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-6 - Dune 3.7.0 changed the install location of mli files * Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-5 - Rebuild OCaml packages for F38 * Wed Jan 18 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-4 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild * Thu Aug 11 2022 Jerry James <loganjerry@gmail.com> - 2.3.3-3 - Convert License tag to SPDX - Note that the AB plugin has a different license
/usr/bin/alt-ergo /usr/lib/.build-id /usr/lib/.build-id/ed /usr/lib/.build-id/ed/34a05b5a9df0496c405536be3bb16a2d1a1c99 /usr/lib64/ocaml/alt-ergo /usr/lib64/ocaml/alt-ergo-free /usr/lib64/ocaml/alt-ergo-free/META /usr/lib64/ocaml/alt-ergo-free/dune-package /usr/lib64/ocaml/alt-ergo-free/opam /usr/lib64/ocaml/alt-ergo/META /usr/lib64/ocaml/alt-ergo/dune-package /usr/lib64/ocaml/alt-ergo/opam /usr/lib64/ocaml/alt-ergo/plugins /usr/lib64/ocaml/alt-ergo/plugins/AB-Why3-plugin.cma /usr/lib64/ocaml/alt-ergo/plugins/AB-Why3-plugin.cmxs /usr/lib64/ocaml/alt-ergo/plugins/fm-simplex-plugin.cma /usr/lib64/ocaml/alt-ergo/plugins/fm-simplex-plugin.cmxs /usr/lib64/ocaml/alt-ergo/preludes /usr/lib64/ocaml/alt-ergo/preludes/b-set-theory-prelude-2018-09-28.ae /usr/lib64/ocaml/alt-ergo/preludes/fpa-theory-2017-01-04-16h00.why /usr/share/doc/alt-ergo /usr/share/doc/alt-ergo/Alt-Ergo--Atelier-B--RSSR-2016.pdf /usr/share/doc/alt-ergo/Alt-Ergo-2.2--SMT-Workshop-2018.pdf /usr/share/doc/alt-ergo/CHANGES /usr/share/doc/alt-ergo/README.md /usr/share/doc/alt-ergo/examples /usr/share/doc/alt-ergo/examples/AB-Why3-plugin /usr/share/doc/alt-ergo/examples/AB-Why3-plugin/p4_34.why /usr/share/doc/alt-ergo/examples/invalid /usr/share/doc/alt-ergo/examples/invalid/arith1.why /usr/share/doc/alt-ergo/examples/invalid/arith2.why /usr/share/doc/alt-ergo/examples/invalid/arrays.why /usr/share/doc/alt-ergo/examples/invalid/bitv.why /usr/share/doc/alt-ergo/examples/lib_usage.ml /usr/share/doc/alt-ergo/examples/valid /usr/share/doc/alt-ergo/examples/valid/ac_arith.why /usr/share/doc/alt-ergo/examples/valid/arith1.why /usr/share/doc/alt-ergo/examples/valid/arith2.why /usr/share/doc/alt-ergo/examples/valid/arith3.why /usr/share/doc/alt-ergo/examples/valid/arith4.why /usr/share/doc/alt-ergo/examples/valid/arrays.why /usr/share/doc/alt-ergo/examples/valid/bitv.why /usr/share/doc/alt-ergo/examples/valid/congruence.why /usr/share/doc/alt-ergo/examples/valid/enum_arrays.why /usr/share/doc/alt-ergo/examples/valid/quantifiers.why /usr/share/man/man1/alt-ergo.1.gz
Generated by rpm2html 1.8.1
Fabrice Bellet, Sat Nov 16 01:56:07 2024