alt-ergo Automatic solver of mathematical formulas for program verification

0.95.2_2 math =0 0.95.2_2Version of this port present on the latest quarterly branch.

There is no maintainer for this port.

Any concerns regarding this port should be directed to the FreeBSD Ports mailing list via ports@FreeBSD.org

Port Added: 2011-12-21 02:58:38

Last Update: 2020-05-18 01:58:50

SVN Revision: 535698

License: CeCILL-C

Description:

Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X), a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism. Alt-Ergo is compact, safe, and modular. Each component is described by a small set of inference rules and is implemented as an Ocaml functor. WWW: http://alt-ergo.lri.fr

SVNWeb : Homepage

pkg-plist: as obtained via: make generate-plist

Expand this list (12 items)

Collapse this list.

1. /usr/local/share/licenses/alt-ergo-0.95.2_2/catalog.mk
2. /usr/local/share/licenses/alt-ergo-0.95.2_2/LICENSE
3. /usr/local/share/licenses/alt-ergo-0.95.2_2/CeCILL-C
4. bin/alt-ergo
5. bin/altgr-ergo
6. lib/ocaml/alt-ergo/META
7. lib/ocaml/alt-ergo/altErgo.cmi
8. lib/ocaml/alt-ergo/altErgo.cmo
9. lib/ocaml/alt-ergo/altErgo.cmx
10. lib/ocaml/alt-ergo/altErgo.o
11. man/man1/alt-ergo.1.gz
12. share/gtksourceview-2.0/language-specs/alt-ergo.lang

Collapse this list.

Dependency lines:

• alt-ergo>0:math/alt-ergo

To install the port: cd /usr/ports/math/alt-ergo/ && make install clean

To add the package: pkg install alt-ergo

PKGNAME: alt-ergo

Flavors: there is no flavor information for this port.

distinfo:

SHA256 (alt-ergo-0.95.2.tar.gz) = 5a6cd4349c144653be19a1ba4c254bbf626bdfd97c54d1c13ba63e396006eeac SIZE (alt-ergo-0.95.2.tar.gz) = 233778

Dependencies

NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.

Build dependencies:

1. ocaml-zarith>1.2 : math/ocaml-zarith
2. ocaml-ocamlgraph>1.8 : math/ocaml-ocamlgraph
3. lablgtk2 : x11-toolkits/ocaml-lablgtk2
4. ocamlc : lang/ocaml
5. gmake>=4.3 : devel/gmake

Runtime dependencies:

1. ocaml-ocamlgraph>1.8 : math/ocaml-ocamlgraph
2. lablgtk2 : x11-toolkits/ocaml-lablgtk2
3. ocamlc : lang/ocaml

Patch dependencies:

1. ocamlc : lang/ocaml

Extract dependencies:

1. ocamlc : lang/ocaml

This port is required by:

for Run

Deleted ports which required this port:

Expand this list of 1 deleted port
1. lang/spark^*
2. Collapse this list of deleted ports.

* - deleted ports are only shown under the This port is required by section. It was harder to do for the Required section. Perhaps later...

Configuration Options

===> The following configuration options are available for alt-ergo-0.95.2_2: GUI=on: GUI (Graphical User Interface) support ===> Use 'make config' to modify these settings

USES:

gmake

Master Sites:

Expand this list (1 items)

Collapse this list.
1. http://alt-ergo.ocamlpro.com/http/alt-ergo-0.95.2/
Collapse this list.

Mark as BROKEN on powerpc64:

  /tmp/camlasm2822e8.s: Assembler messages:
  /tmp/camlasm2822e8.s:10348: Error: operand out of range (0x000000000000804c is
not between 0xffffffffffff8000 and 0x0000000000007ffc)
  /tmp/camlasm2822e8.s:32988: Error: operand out of range (0x000000000000805c is
not between 0xffffffffffff8000 and 0x0000000000007ffc)

Reset ports maintained by bf@ until he has time again to work on them.

PR:		210474
Submitted by:	jbeich
With hat:	portmgr-secretary

Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p.

With hat:	portmgr
Sponsored by:	Absolight

- Add USE_OCAML_CAMLP4 and USE_OCAML_TK to bsd.ocaml.mk which add
  depends on the camlp4 language and labltk ocaml modules, which are
  now in separate ports.
- Update x11-toolkits/ocaml-lablgtk2 to 2.18.3
- Update graphics/ocaml-lablgl to 1.05
- Make unison ports use USE_OCAML
- Convert ports to the new flags where needed
- Bump PORTREVISION on ports depending on ocaml-lablgtk2, those need to be
rebuilt

PR:			199845
Submitted by:		jbeich@
Differential Revision:	https://reviews.freebsd.org/D2434
Approved by:		portmgr (mat)

Canonicalize a few licenses

Cleanup plist

Update the default version of GCC in the Ports Collection from GCC 4.7.4
to GCC 4.8.3.

Part II, Bump PORTREVISIONs.

PR:		192025
Tested by:	antoine (-exp runs)
Approved by:	portmgr (implicit)

Convert GMAKE to MAKE_CMD
Please note that lots of invocation of MAKE_CMD here are wrong as they do not
properly respect MAKE_ENV and friends

With hat:	portmgr

math/alt-ergo: Update version 0.94 => 0.95.2 and support stage

- Convert gmake,bzip2 to USES

Approved by:	portmgr

Add NO_STAGE all over the place in preparation for the staging support (cat:
math)

update master sites; trim headers; reposition LICENSE, WWW

switch to the new options format

update x11-toolkits/ocaml-lablgtk2 to 2.16.0+bugfixes, and adjust
dependent ports

PR:		144982, 149958
Reviewed by:	johans (earlier version of the patch)

- update png to 1.5.10

Add alt-ergo 0.94, an automatic theorem prover dedicated to program
verification.

12 vulnerabilities affecting 81 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities

Last updated:
2021-01-23 18:22:23