twelf Meta-logical framework for deductive systems

1.7.1_4 lang =0 1.7.1Version of this port present on the latest quarterly branch.

IGNORE: is marked as broken on FreeBSD 12.0: invalid target: self

Maintainer: beyert@cs.ucr.edu

Port Added: 2005-11-26 13:27:41

Last Update: 2019-07-26 21:46:57

SVN Revision: 507372

Also Listed In: math

License: BSD2CLAUSE

Description:

The Twelf implementation comprises * the LF logical framework, including type reconstruction; * the Elf constraint logic programming language; * an inductive meta-theorem prover for LF; * and an Emacs interface. Twelf provides a uniform meta-language for specifying, implementing, and proving properties of programming languages and logics. Example suites include Cartesian Closed Categories and lambda-calculus, the Church-Rosser theorem for the untyped lambda-calculus, Mini-ML including type preservation and compilation, cut elimination, theory of logic programming, and Hilbert's deduction theorem. -- the Twelf home page WWW: http://www.cs.cmu.edu/~twelf

SVNWeb : Homepage

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

Expand this list (4 items)

1. bin/twelf-server
2. /usr/local/share/licenses/twelf-1.7.1_4/catalog.mk
3. /usr/local/share/licenses/twelf-1.7.1_4/LICENSE
4. /usr/local/share/licenses/twelf-1.7.1_4/BSD2CLAUSE

Collapse this list.

Dependency lines:

• twelf>0:lang/twelf

To install the port: cd /usr/ports/lang/twelf/ && make install clean

A package is not available for ports marked as: Forbidden / Broken / Ignore / Restricted

PKGNAME: twelf

Flavors: there is no flavor information for this port.

distinfo:

SHA256 (twelf-src-1.7.1.tar.gz) = 91b0d4d8c2e54452a042da0ff642f3b46b25efb36a84497aa8b96598f49a213a SIZE (twelf-src-1.7.1.tar.gz) = 1147610

Dependencies

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

Build dependencies:

1. mlton : lang/mlton
2. texi2html : textproc/texi2html
3. tex.fmt : print/tex-formats
4. dvips : print/tex-dvipsk
5. gmake : devel/gmake
6. makeinfo : print/texinfo

Runtime dependencies:

1. mlton : lang/mlton
2. indexinfo : print/indexinfo

There are no ports dependent upon this port

Configuration Options

===> The following configuration options are available for twelf-1.7.1_4: DOCS=on: Build and/or install documentation ===> Use 'make config' to modify these settings

USES:

gmake makeinfo

Master Sites:

1. http://twelf.plparty.org/releases/
2. http://www-2.cs.cmu.edu/~twelf/dist/
3. http://www.cs.cmu.edu/~twelf/dist/

Bump PORTREVISION for ports depending on the canonical version of GCC
as defined in Mk/bsd.default-versions.mk which has moved from GCC 8.3
to GCC 9.1 under most circumstances now after revision 507371.

This includes ports
 - with USE_GCC=yes or USE_GCC=any,
 - with USES=fortran,
 - using Mk/bsd.octave.mk which in turn features USES=fortran, and
 - with USES=compiler specifying openmp, nestedfct, c11, c++0x, c++11-lang,
   c++11-lib, c++14-lang, c++17-lang, or gcc-c++11-lib
plus, everything INDEX-11 shows with a dependency on lang/gcc9 now.

PR:		238330

Mark BROKEN on FreeBSD 12 and 13

mlton -default-ann 'nonexhaustiveMatch ignore' -output bin/twelf-server
build/${cmfileid}
invalid target: self

Reported by:	pkg-fallout
MFH:		2019Q2

Bump PORTREVISION for ports depending on the canonical version of GCC
defined via Mk/bsd.default-versions.mk which has moved from GCC 7.4 t
GCC 8.2 under most circumstances.

This includes ports
 - with USE_GCC=yes or USE_GCC=any,
 - with USES=fortran,
 - using Mk/bsd.octave.mk which in turn features USES=fortran, and
 - with USES=compiler specifying openmp, nestedfct, c11, c++0x, c++11-lang,
   c++11-lib, c++14-lang, c++17-lang, or gcc-c++11-lib
plus, as a double check, everything INDEX-11 showed depending on lang/gcc7.

PR:		231590

Install texinfo files (GNU info) into ${PREFIX}/share/info

After a discussion on the mailing list on moving manpages to
${PREFIX}/share/man for consistency with base where it is
installed in usr/share/man, it appeared the same should happen
to GNU info files which were installed under share in base and
not in ports.

Now texinfo is not in base on any of the supported version of FreeBSD
it is possible to proceed to this move and it is easier to do than
the manpage change.

Other benefit than consistency are less patching: all build tools but
cmake are expecting info files to be under share/info and cmake (patched here)
was having an exception for BSD so the patch makes FreeBSD case less
specific for them

Bump revision of all impacted ports

PR:		232907
exp-run by:	antoine
Differential Revision:	https://reviews.freebsd.org/D17816

Install info page properly

Bump PORTREVISIONs of all users of math/mpc that we just updated to
version 1.1.0 (via revision 464079).

- USe DISTVERSIONPREFIX instead of DISTNAME
- Add missing OPTIONS_DEFINE=DOCS
- Use USES=makeinfo instead of hard-coded BUILD_DEPENDS
- Convert to options helper
- Convert to options target helper
- While I'm here, fix indent

Approved by:	portmgr (blanket)

Remove ${PORTSDIR}/ from dependencies, categories h, i, j, k, and l.

With hat:	portmgr
Sponsored by:	Absolight

Do not hardcode dvips dependency

Fix build with texlive

- Update to latest upstream release 1.7.1
- Assign maintainership to Timothy Beyer <beyert@cs.ucr.edu>
  (previously ports@)
- General cleanup
- Add LICENSE
- Remove twelf from LEGAL (port is now BSD2CLAUSE licensed)

PR:		191758
Submitted by:	Timothy Beyer <beyert@cs.ucr.edu>
Approved by:	mentors (implicit)

Remove indefinite articles and trailing periods from COMMENT, plus minor
COMMENT typos and surrounding whitespace fixes. A few Makefiles where not
included as they contain Latin-1 characters that break the Phabricator
workflow. Categories J-L.

CR:		D305
Approved by:	portmgr (swills)

Maintainer no longer wishes to maintain those ports

With hat:	portmgr

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

Rectify USE_TEX to support both of teTeX and TeXLive.

TEX_DEFAULT:
	A knob to choose teTeX or TeXLive.  One can specify in /etc/make.conf.

USE_TEX:
	A knob for port developers.  Valid keywords are listed in
	bsd.tex.mk.

Remove *_DEPENDS from ports which depend on teTeX and add USE_TEX=tetex
instead to make migration to TeXLive easier.

- update png to 1.5.10

The vast majority of pkg-descr files had the following format when they
had both lines:

Author: ...
WWW: ....

So standardize on that, and move them to the end of the file when necessary.

Also fix some more whitespace, and remove more "signature tags" of varying
forms, like -- name, etc.

s/AUTHOR/Author/

A few other various formatting issues

- remove MD5

Bump PORTREVISION after open-mofit update

- update to 1.4.1
Reviewed by:    exp8 run on pointyhat
Supported by:   miwi

- update to jpeg-8

- bump all port that indirectly depends on libjpeg and have not yet been bumped
or updated
Requested by:   edwin

- Update to 1.5R1

PR:             ports/131631
Submitted by:   Andrew Bernard <andrewb@cs.cmu.edu> (maintainer)

Remove USE_REINPLACE from the categories starting with L

New port: lang/twelf A meta-logical framework for deductive systems

        The Twelf implementation comprises
         * the LF logical framework, including type reconstruction;
         * the Elf constraint logic programming language;
         * an inductive meta-theorem prover for LF;
         * and an Emacs interface.

PR:             ports/84625
Submitted by:   "Andrew Bernard" <andrew@hobnob.com>

18 vulnerabilities affecting 97 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities

Last updated:
2019-08-23 22:19:20