math/coq 8.20.1_3,3 FreeBSD

Theorem prover based on lambda-C

System: FreeBSD
Repository: FreeBSD ports
Maintainer: [email protected]
License: LGPL21
Categories: math
Package size: 200490.3 KiB, 695323.2 KiB installed

Description

Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine.

In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification "kernel".

Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.

CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.

In the other systems

System

Port

Version

FreeBSD

math/coq

8.20.1_3,3

NetBSD

lang/coq

8.20.1nb10

Install

Binary package:

pkg install coq

From the ports tree:

cd /usr/ports/math/coq/ && make install clean

To depend on this port in another port's Makefile:

RUN_DEPENDS=	coq>0:math/coq

Packages

The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.

Repository

aarch64

amd64

armv6

armv7

i386

FreeBSD:14:latest

8.20.1_3,3

FreeBSD:14:quarterly

8.20.1_3,3

n/a

8.20.1_3,3

FreeBSD:15:latest

8.20.1_3,3

n/a

8.20.1_2,3

FreeBSD:15:quarterly

8.20.1_3,3

n/a

FreeBSD:16:latest

8.20.1_3,3

n/a

FreeBSD:16:quarterly

n/a

Dependencies

As this port's Makefile names them.

Build 4

${LOCALBASE}/${OCAML_SITELIBDIR}/num/META : math/ocaml-num
${LOCALBASE}/${OCAML_SITELIBDIR}/zarith/META : math/ocaml-zarith
bash : shells/bash
camlp5 : devel/ocaml-camlp5

Library 4

libfontconfig.so : x11-fonts/fontconfig
libfreetype.so : print/freetype2
libgmp.so : math/gmp
libharfbuzz.so : print/harfbuzz

Runtime 2

${LOCALBASE}/${OCAML_SITELIBDIR}/num/META : math/ocaml-num
${LOCALBASE}/${OCAML_SITELIBDIR}/zarith/META : math/ocaml-zarith

The full lists below include those, and their dependencies in turn.

Build dependencies 119

The first 100 are listed.

Run dependencies 110

The first 100 are listed.

No port depends on this one.

Configuration

Options name: math_coq

Option

Default

Description

DOCS

off

Build and/or install documentation

IDE

Include desktop environment (coqide)

USES: gettext-runtime gmake gnome ocaml:camlp4,dune,ldconfig python:env shebangfix tex
Service scripts: none
Conflicts with: coq-emacs_*

Message after installing

===>   NOTICE:

The coq port currently does not have a maintainer. As a result, it is
more likely to have unresolved issues, not be up-to-date, or even be removed in
the future. To volunteer to maintain this port, please create an issue at:

https://bugs.freebsd.org/bugzilla

More information about port maintainership is available at:

https://docs.freebsd.org/en/articles/contributing/#ports-contributing

Files

Manual pages 11

coq-tex(1)
coq_makefile(1)
coqc(1)
coqchk(1)
coqdep(1)
coqdoc(1)
coqide(1)
coqnative(1)
coqtop(1)
coqtop.byte(1)
coqwc(1)

pkg-plist 7057

bin/coq-tex
bin/coq_makefile
bin/coqc
bin/coqc.byte
bin/coqchk
bin/coqdep
bin/coqide
bin/coqidetop.byte
bin/coqidetop.opt
bin/coqdoc
bin/coqnative
bin/coqpp
bin/coqtimelog2html
bin/coqtop
bin/coqtop.byte
bin/coqwc
bin/coqworkmgr
bin/coqworker.opt
bin/csdpcert
bin/ocamllibdep
bin/votour
@dir etc/xdg/coq
share/coq/coq-ssreflect.lang
share/coq/coq.lang
share/coq/coq.png
share/coq/coq_style.xml
share/coq/default.bindings
share/doc/ocaml/coq-core/LICENSE
share/doc/ocaml/coq-core/README.md
share/doc/ocaml/coq-stdlib/LICENSE
share/doc/ocaml/coq-stdlib/README.md
share/doc/ocaml/coq/LICENSE
share/doc/ocaml/coq/README.md
share/doc/ocaml/coq/odoc-pages/index.mld
share/doc/ocaml/coqide-server/LICENSE
share/doc/ocaml/coqide-server/README.md
share/doc/ocaml/coqide/FAQ
share/doc/ocaml/coqide/LICENSE
share/doc/ocaml/coqide/README.md
share/doc/ocaml/coqide/odoc-pages/index.mld
share/man/man1/coq-tex.1.gz
share/man/man1/coq_makefile.1.gz
share/man/man1/coqc.1.gz
share/man/man1/coqchk.1.gz
share/man/man1/coqdep.1.gz
share/man/man1/coqdoc.1.gz
share/man/man1/coqide.1.gz
share/man/man1/coqnative.1.gz
share/man/man1/coqtop.byte.1.gz
share/man/man1/coqtop.1.gz
share/man/man1/coqwc.1.gz
%%TEXMFDIR%%/tex/latex/misc/coqdoc.sty
%%OCAML_SITELIBDIR%%/coq-core/META
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.a
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cma
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cmi
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cmt
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cmx
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cmxa
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cmxs
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.ml
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Env.cmi
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Env.cmt
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Env.cmti
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Env.cmx
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Path.cmi
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Path.cmt
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Path.cmti
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Path.cmx
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Usage.cmi
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Usage.cmt
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Usage.cmti
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Usage.cmx
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Util.cmi
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Util.cmt
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Util.cmti
%%OCAML_SITELIBDIR%%/coq-core/boot/boot__Util.cmx
%%OCAML_SITELIBDIR%%/coq-core/boot/env.ml
%%OCAML_SITELIBDIR%%/coq-core/boot/env.mli
%%OCAML_SITELIBDIR%%/coq-core/boot/path.ml
%%OCAML_SITELIBDIR%%/coq-core/boot/path.mli
%%OCAML_SITELIBDIR%%/coq-core/boot/usage.ml
%%OCAML_SITELIBDIR%%/coq-core/boot/usage.mli
%%OCAML_SITELIBDIR%%/coq-core/boot/util.ml
%%OCAML_SITELIBDIR%%/coq-core/boot/util.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/analyze.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/analyze.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/check.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/check.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/checkFlags.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/checkFlags.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/checkInductive.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/checkInductive.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/checkTypes.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/checkTypes.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/check_stat.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/check_stat.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/checker.ml
%%OCAML_SITELIBDIR%%/coq-core/checklib/checker.mli
%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.a

The first 100 are listed.

distinfo 1

File

Size

SHA256

coq-coq-V8.20.1_GH0.tar.gz

7.842928e+06

09ad238cc7930d59564b032be2a8a1fd10d6ef845364d739072d04090a6d3cc2

Commit history 0

No commits in the history this site was built from.