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.
===> The following configuration options are available for alt-ergo-2.5.4_2:
DOCS=on: Build and/or install documentation
MANPAGES=off: Build and/or install manual pages
===> Use 'make config' to modify these settings
Mk/**ocaml.mk: Convert remaining bsd.ocaml.mk to Uses/ocaml.mk
- Instead of USE_OCAML=yes use USES=ocaml. If empty USES=ocaml implies
build and run
- Instead of USE_OCAMLFIND_PLIST use USES=ocaml:findplist which also
implies USES=ocaml:findlib
- Instead of USE_OCAML_CAMLP4 use USES=ocaml:camlp4
- Instead of USE_OCAML_FINDLIB use USES=ocaml:findlib
- Instead of USE_OCAML_LDCONFIG use USES=ocaml:ldconfig
- Instead of USE_OCAML_WASH use USES=ocaml:wash
- Instead of NO_OCAML_BUILDDEPENDS use USES=ocaml:run
- Instead of NO_OCAML_RUNDDEPENDS use USES=ocaml:build
- Instead of USE_OCAML_TK use USES=ocaml:tk which actually implies
USES=ocaml:tkbuild and USES=ocaml:tkrun
- Instead of NO_OCAMLTK_BUILDDEPENDS use USES=ocaml:tkrun
- Instead of NO_OCAMLTK_RUNDEPENDS use USES=ocaml:tkbuild
- USES=ocaml:dune remains unchanged
- Prepare to add/remove keywords easily
Approved by: mat (portmgr)
Reviewed by: freebsd@dev.thsi.be
Differential Revision: https://reviews.freebsd.org/D48227
devel/ocaml-seq: Mark DEPRECATED and set EXPIRATION_DATE to 2024-12-10
Seq the ocaml module is part of lang/ocaml since 4.07. This package is a
compatibility shims that is needed for people using 4.06 and earlier.
PR: 280761
Approved by: submitter is maintainer
math/alt-ergo: Update to 2.5.4, many new ports
Replace GNU configure to dune builds system.
Add do-test target.
Submitter takes maintainership.
Update WWW.
Switch to DISTVERSION.
The last update of alt-ergo in ports tree was about 10 years ago, the newest
version requires many new libraries in ports tree.
New ports:
devel/ocaml-dolmen
devel/ocaml-gen
devel/ocaml-hmap
devel/ocaml-linol
(Only the first 15 lines of the commit message are shown above )
ocaml: Updates to ocaml compiler and several ocaml ports
- Update devel/ocaml to 4.14.2 [1]
- Specify runtime dependency on GNU AS as full path, this fixes
build on armv6 - armv7 [1] [2]
- converters/ocaml-base64: Update to 3.5.1, add LICENSE, other
improvements
- converters/ocaml-jsonm: Strip shared objects [3]
- databases/ocaml-dbm: Update to 1.3, move to gitlub, other
improvements
- devel/menhir: Update to 20231231
- devel/ocaml-base: Unbreak non-x86 [2]
- devel/ocaml-camlp-streams: Silence patch and strip commands
- devel/ocaml-ipaddr: Update to 5.5.0
- devel/ocaml-lwt: Update to 5.7.0 [4]
(Only the first 15 lines of the commit message are shown above )
lang/ocaml: Update to 4.08.1
This update allows (and for some requires) to also update dependencies
to newer versions. Where possible I updated to the latest version.
The ocaml port now is MAKE_JOBS safe.
Changes to dependent ports included in this commit:
- devel/ocaml-sexplib: Rename to devel/ocaml-sexplib0 adapting to
upstream. Update to 0.16.0
- devel/coccinelle: Update to 1.1.1, moved to github
- devel/ocaml-camlp4: Update to 4.08+1
- devel/ocaml-camomile: Use dune for build, adapt port
- devel/ocaml-cppo: Fix lib files installation [1]
(Only the first 15 lines of the commit message are shown above )
Remove WWW entries moved into port Makefiles
Commit b7f05445c00f has added WWW entries to port Makefiles based on
WWW: lines in pkg-descr files.
This commit removes the WWW: lines of moved-over URLs from these
pkg-descr files.
Approved by: portmgr (tcberner)
Add WWW entries to port Makefiles
It has been common practice to have one or more URLs at the end of the
ports' pkg-descr files, one per line and prefixed with "WWW:". These
URLs should point at a project website or other relevant resources.
Access to these URLs required processing of the pkg-descr files, and
they have often become stale over time. If more than one such URL was
present in a pkg-descr file, only the first one was tarnsfered into
the port INDEX, but for many ports only the last line did contain the
port specific URL to further information.
There have been several proposals to make a project URL available as
a macro in the ports' Makefiles, over time.
(Only the first 15 lines of the commit message are shown above )
math: remove 'Created by' lines
A big Thank You to the original contributors of these ports:
* Aaron Dalton <aaron@FreeBSD.org>
* Aaron Dalton <aaron@daltons.ca>
* Alessando Sagratini <ale_sagra@hotmail.com>
* Alex Dupre <ale@FreeBSD.org>
* Alexey Dokuchaev <danfe@FreeBSD.org>
* Amarendra Godbole <amarendra.godbole@gmail.com>
* Anders Nordby <anders@FreeBSD.org>
* Andreas Fehlner (fehlner@gmx.de)
* Andrew L. Neporada <andrew@chg.ru>
* Andrey <gugu@zoo.rambler.ru>
* Andrey Zakhvatov
(Only the first 15 lines of the commit message are shown above )
OCaml: transient update of the stack to version 4.07.1
This is the first step in modernizing our OCaml ports infrastructure,
as we had accumulated substantial technical debt over the years when
many of its consumer ports had not received proper care and updates.
It is currently considered as the lowest supported version (baseline)
in majority of open-source OCaml projects, which would help to pull
up other ports, e.g. `devel/ocaml-dune' in smaller, manageable pieces.
For conservative hackers among us and for compatibility with RHEL 8
which is also on it, having 4.07 in the tree would allow users stick
to that package (pkg lock it) if needed.
PR: 250408, 262781
Exp-run by: antoine
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)
- 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)
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
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)
