./math/coq [proof assistant based on a typed lambda calculus]
[+] Add this package to your ports tracker

[ CVSweb ] [ Homepage ] [ RSS feed ]

Version: 8.10.0, Package name: coq-8.10.0
Maintained by: Yozo Toda
Master sites:
Description
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs.


Filesize: 6074.544 KB
Version History (View Complete History)
  • (2019-10-16) Updated to version: coq-8.10.0
  • (2019-09-20) Updated to version: coq-8.10beta3
  • (2019-09-08) Updated to version: coq-8.10beta2
  • (2019-03-04) Updated to version: coq-8.8.0
  • (2015-06-20) Updated to version: coq-8.4pl6
  • (2014-11-18) Updated to version: coq-8.4pl5
  • (2014-08-27) Updated to version: coq-8.4pl4
  • (2014-03-26) Updated to version: coq-8.4pl3
  • (2013-11-09) Updated to version: coq-8.4pl2
  • (2013-02-07) Updated to version: coq-8.4pl1
[show/hide] View available PLISTS (Can be a lot of data)

CVS Commit History:

   2019-10-16 00:40:03 by Daniel Dickman | Files touched by this commit (2)
Log message:
Update to coq 8.10.0; ok Yoza Toda (MAINTAINER)
   2019-10-08 04:56:29 by Stuart Henderson | Files touched by this commit (1)
Log message:
really bump REVISION
   2019-10-07 00:40:15 by Christopher Zimmermann | Files touched by this commit (4)
Log message:
fix plist for bytecode-only arm64, sparc64
OK jca@
   2019-09-27 03:58:09 by Antoine Jacoutot | Files touched by this commit (1)
Log message:
Missed bump.
-@depend lang/ocaml,-main:ocaml-=4.08.1:ocaml-4.08.1
-@depend x11/lablgtk3:lablgtk3-*:lablgtk3-3.0.beta6p0
+@depend lang/ocaml:ocaml-=4.09.0:ocaml-4.09.0
+@depend x11/lablgtk3:lablgtk3-*:lablgtk3-3.0.beta6p1
   2019-09-19 21:28:34 by Daniel Dickman | Files touched by this commit (5)
Log message:
- Update to beta3 to pickup a few bug fixes.
- Make the regression tests more verbose like we used but lost in one
of the recent updates.
ok Yozo Toda (MAINTAINER)
   2019-09-18 11:49:37 by Christopher Zimmermann | Files touched by this commit (42)
Log message:
Upgrade lang/ocaml to 4.08.1
* net unison needed some patchign to avoid deprecated library functions.
* all ports depending on the exact version of OCaml need revision bumps.
* net/unison needed some help to avoid deprecated library functions.
ok krw@, testing on i386 and ok daniel@
   2019-09-10 08:09:17 by Stuart Henderson | Files touched by this commit (1)
Log message:
BUILD_DEPENDS on bash
   2019-09-06 16:10:18 by Christopher Zimmermann | Files touched by this commit (8)
Log message:
Upgrade to 8.10beta2, which supports OCaml 4.08.
no objections krw@, please commit daniel@
   2019-07-12 14:47:59 by Stuart Henderson | Files touched by this commit (874)
Log message:
replace simple PERMIT_PACKAGE_CDROM=Yes with PERMIT_PACKAGE=Yes
   2019-03-23 04:55:51 by Jeremie Courreges-Anglas | Files touched by this commit (1)
Log message:
Move comment to the right place
   2019-03-23 04:54:59 by Jeremie Courreges-Anglas | Files touched by this commit (2)
Log message:
DPB_PROPERTIES=parallel not needed
Sneaked in the last OCaml update.  Those ports aren't big nor critical
enough to warrant the use of multiple build slots in regular bulk
builds.
   2019-03-04 21:29:47 by Jeremie Courreges-Anglas | Files touched by this commit (68)
Log message:
Those files should have been removed in the ocaml-4.07.1+friends update
Noticed by krw@ and Adam Steen
   2019-03-04 05:51:17 by Christopher Zimmermann | Files touched by this commit (133)
Log message:
Upgrade OCaml and dependent ports
testing and OKs by avsm@, jca@, krw@ Thanks a lot !
   2018-05-20 02:25:36 by Marc Espie | Files touched by this commit (2)
Log message:
this does need the emacs dirs
   2017-02-25 11:58:04 by Daniel Dickman | Files touched by this commit (1)
Log message:
Minor cleanup:
- http -> https
- drop gettext module
ok shadchin@, tb@
   2016-06-24 09:59:13 by Kenneth R Westerback | Files touched by this commit (42)
Log message:
Upgrade Ocaml to 4.3.0 and tweak ports the minimal amount to keep
them all compiling.
Tweaks include updating
ocaml-batteries 2.3.1 -> 2.5.0
ocaml-lwt 2.4.8 -> 2.5.2
ocaml-ppx-tools 0.99.2 -> 4.03.0
ocaml-camlp4 4.02+6 -> 4.03+1
utop 1.15 -> 1.19.2
and fixes to coccinelle and wyrd to let them build on bytecode archs.
Other necessary tweaks from the various homes of the projects.
Everything still builds on amd64 (native and bytecode) and sparc64 (bytecode).
ok anil@ sthen@ so final 4.3.0 tweaks can be done in-tree.
   2016-03-29 05:27:01 by Christian Weisgerber | Files touched by this commit (50)
Log message:
g/c PFRAG.shared from OCaml ports; ok chrisz@
   2015-08-30 10:34:41 by Anil Madhavapeddy | Files touched by this commit (1)
Log message:
bump coq REVISION due to OCaml 4.02.3 update
ok jca@, tested by krw@ daniel@ jsg@
   2015-06-19 15:25:32 by Daniel Dickman | Files touched by this commit (5)
Log message:
Update to coq 8.4pl6; ok Yozo (MAINTAINER), sthen@
   2015-01-22 14:17:47 by Christian Weisgerber | Files touched by this commit (23)
Log message:
Drop USE_GROFF: trivial page footer differences only.
   2014-11-17 19:00:52 by Daniel Dickman | Files touched by this commit (4)
Log message:
coq update from chrisz@ and nigel@ by way of Yozo Toda (MAINTAINER).
using dpb, sthen@ discovered that having latex around at config time
but not at build time will cause the coq build to fail because
latex is not listed as a BDEP. Fix this as well.
   2010-11-19 00:23:15 by Marc Espie | Files touched by this commit (332)
Log message:
new depends
   2010-10-18 14:52:10 by Marc Espie | Files touched by this commit (151)
Log message:
USE_GROFF=Yes
   2010-07-18 04:30:41 by Steven Mestdagh | Files touched by this commit (23)
Log message:
REVISION
   2008-01-04 10:48:38 by Marc Espie | Files touched by this commit (187)
Log message:
tweak FAKE_FLAGS semantics to saner defaults.
   2007-09-15 12:44:37 by Steven Mestdagh | Files touched by this commit (60)
Log message:
remove quotes from COMMENT/PERMIT*/BROKEN
   2007-04-05 10:20:19 by Marc Espie | Files touched by this commit (912)
Log message:
base64 checksums.


   2005-08-09 16:50:15 by Alexandre Anriot | Files touched by this commit (1)
Log message:
this version doesn't work with ocaml 3.08, mark it as broken.
ok naddy@


   2005-01-05 10:05:07 by Christian Weisgerber | Files touched by this commit (124)
Log message:
SIZE


   2004-12-27 00:16:44 by Aleksander Piotrowski | Files touched by this commit (16)
Log message:
Add WANTLIB markers


   2004-09-15 03:12:00 by Marc Espie | Files touched by this commit (42)
Log message:
new style PLISTs


   2004-08-10 14:41:47 by Xavier Santolaria | Files touched by this commit (9)
Log message:
more new-style MODULES.


   2004-07-11 06:18:45 by Marc Espie | Files touched by this commit (2)
Log message:
fed up with changing checksums: provide a local mirror and kill
IGNOREFILES.


   2003-12-31 10:07:26 by Nikolay Sturm | Files touched by this commit (2)
Log message:
compile with ocaml 3.07


   2003-12-15 14:42:44 by Christian Weisgerber | Files touched by this commit (507)
Log message:
remove WWW lines


   2002-12-18 02:41:07 by Nikolay Sturm | Files touched by this commit (1)
Log message:
make coq use the ocaml module
requested by and OK naddy@


   2002-12-18 02:40:07 by Nikolay Sturm | Files touched by this commit (2)
Log message:
make coq use the ocaml module
requested by and OK naddy@


   2002-11-04 14:10:44 by Christian Weisgerber | Files touched by this commit (4)
Log message:
Update to 7.3.1 and unbreak.
From: Yozo Toda <yozo@v007.vaio.ne.jp>


   2002-09-07 17:43:09 by Christian Weisgerber | Files touched by this commit (1)
Log message:
remove obsolete camlp4 dependency