twelf Meta-logical framework for deductive systems
1.7.1_3 lang =0

Maintainer: beyert@cs.ucr.edu
Port Added: 2005-11-26 13:27:41
Last Update: 2019-04-22 17:01:13
SVN Revision: 499655
Also Listed In: math
License: BSD2CLAUSE

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

Pseudo-pkg-plist information, but much better, from make generate-plist
Expand this list (4 items)

1. bin/twelf-server
2. /usr/local/share/licenses/twelf-1.7.1_3/catalog.mk
3. /usr/local/share/licenses/twelf-1.7.1_3/LICENSE
4. /usr/local/share/licenses/twelf-1.7.1_3/BSD2CLAUSE
Collapse this list.

Dependency lines:

• twelf>0:lang/twelf

---

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

PKGNAME: twelf

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

---

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_3:
     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/

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>

8 vulnerabilities affecting 48 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities

Last updated:
2019-05-18 02:24:37