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.
===> The following configuration options are available for coq-8.20.1_3,3:
DOCS=on: Build and/or install documentation
IDE=on: Include desktop environment (coqide)
===> Use 'make config' to modify these settings
Reason:
Upstream no longer installs Emacs lisp, so the Emacs flavors have been
removed. In order for a `pkg upgrade` to install new versions of coq,
any installed package for a non-default flavor must be renamed. Do
this by running the commands below under /bin/sh with superuser
privileges:
on=$(pkg query -g %n coq-emacs_*)
nn=$(pkg query -g %n g coq-emacs_* | sed -e 's/-emacs_[a-z_]*//')
pkg set -n "$on":"$nn"
Number of commits found: 107 (showing only 7 on this page) #
- Unbreak on amd64
(Johan van Selst succesfully ran the test-suite
on an amd64 running 6-CURRENT and ocaml-3.08.2)
PR: ports/75334
Submitted by: maintainer
- Add optional CoqIde support (depends on lablgtk2)
- Correct PORTVERSION to match actual source version
- Cosmetics
PR: ports/73634
Submitted by: Rene Ladan <r.c.ladan@student.tue.nl> (maintainer)
Add coq, 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".
PR: ports/72718
Submitted by: Rene Ladan <r.c.ladan@student.tue.nl>
Number of commits found: 107 (showing only 7 on this page)
