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

[ CVSweb ] [ Homepage ] [ RSS feed ]

Version: 8.4pl6, Package name: coq-8.4pl6
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: 4003.726 KB
Version History (View Complete History)
  • (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
  • (2013-01-06) Updated to version: coq-8.4
  • (2006-07-21) Package added to openports.se, version coq-7.3.1p0 (created)
[show/hide] View available PLISTS (Can be a lot of data)

CVS Commit History:

   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@
   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@
   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-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-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-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-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.
   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.
   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.
   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.


   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-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-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-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-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-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