FreshPorts -- The Place For Ports If you buy from Amazon USA, please support us by using this link.
Follow us
Blog
Twitter

We also have a status page: https://freshports.wordpress.com/

Port details
why3 Deductive program verification platform
0.83_2 math on this many watch lists=0 search for ports that depend on this port Find issues related to this port Report an issue related to this port

There is no maintainer for this port.
Any concerns regarding this port should be directed to the FreeBSD Ports mailing list via ports@FreeBSD.org search for ports maintained by this maintainer
Port Added: 04 Jun 2014 19:22:50
License: LGPL21
Why3 is a platform for deductive program verification. It provides a rich
language for specification and programming, called WhyML, and relies on
external theorem provers, both automated and interactive, to discharge
verification conditions. Why3 comes with a standard library of logical
theories (integer and real arithmetic, Boolean operations, sets and maps,
etc.) and basic programming data structures (arrays, queues, hash tables,
etc.). A user can write WhyML programs directly and get correct-by-
construction OCaml programs through an automated extraction mechanism.
WhyML is also used as an intermediate language for the verification of C,
Java, or Ada programs.

Why3 is a complete reimplementation of the former Why platform. Among the
new features are: numerous extensions to the input language, a new
architecture for calling external provers, and a well-designed API,
allowing to use Why3 as a software library. An important emphasis is put
on modularity and genericity, giving the end user a possibility to easily
reuse Why3 formalizations or to add support for a new external prover if
wanted.

WWW: http://why3.lri.fr
SVNWeb : Homepage : PortsMon
    Pseudo-pkg-plist information, but much better, from make generate-plist
    Expand this list (191 items)
  1. /usr/local/share/licenses/why3-0.83_2/catalog.mk
  2. /usr/local/share/licenses/why3-0.83_2/LICENSE
  3. /usr/local/share/licenses/why3-0.83_2/LGPL21
  4. bin/why3
  5. bin/why3bench
  6. bin/why3config
  7. bin/why3doc
  8. bin/why3ide
  9. bin/why3replayer
  10. bin/why3session
  11. lib/ocaml/site-lib/why3/META
  12. lib/ocaml/site-lib/why3/why3.a
  13. lib/ocaml/site-lib/why3/why3.cma
  14. lib/ocaml/site-lib/why3/why3.cmi
  15. lib/ocaml/site-lib/why3/why3.cmo
  16. lib/ocaml/site-lib/why3/why3.cmx
  17. lib/ocaml/site-lib/why3/why3.cmxa
  18. lib/ocaml/site-lib/why3/why3.o
  19. lib/ocaml/site-lib/why3/why3extract.a
  20. lib/ocaml/site-lib/why3/why3extract.cma
  21. lib/ocaml/site-lib/why3/why3extract.cmi
  22. lib/ocaml/site-lib/why3/why3extract.cmo
  23. lib/ocaml/site-lib/why3/why3extract.cmx
  24. lib/ocaml/site-lib/why3/why3extract.cmxa
  25. lib/ocaml/site-lib/why3/why3extract.o
  26. lib/why3/plugins/dimacs.cmo
  27. lib/why3/plugins/dimacs.cmxs
  28. lib/why3/plugins/genequlin.cmo
  29. lib/why3/plugins/genequlin.cmxs
  30. lib/why3/plugins/hypothesis_selection.cmo
  31. lib/why3/plugins/hypothesis_selection.cmxs
  32. lib/why3/plugins/tptp.cmo
  33. lib/why3/plugins/tptp.cmxs
  34. lib/why3/why3-call-pvs
  35. lib/why3/why3-cpulimit
  36. share/doc/why3/manual.pdf
  37. share/why3/drivers/alt_ergo.drv
  38. share/why3/drivers/alt_ergo_0.92.drv
  39. share/why3/drivers/alt_ergo_0.93.drv
  40. share/why3/drivers/alt_ergo_0.94.drv
  41. share/why3/drivers/alt_ergo_bare.drv
  42. share/why3/drivers/alt_ergo_model.drv
  43. share/why3/drivers/alt_ergo_smt2.drv
  44. share/why3/drivers/beagle.drv
  45. share/why3/drivers/coq-common.gen
  46. share/why3/drivers/coq-realizations.aux
  47. share/why3/drivers/coq-realize.drv
  48. share/why3/drivers/coq.drv
  49. share/why3/drivers/cvc3.drv
  50. share/why3/drivers/cvc3_bare.drv
  51. share/why3/drivers/cvc4.drv
  52. share/why3/drivers/cvc4_bare.drv
  53. share/why3/drivers/discrimination.gen
  54. share/why3/drivers/eprover.drv
  55. share/why3/drivers/gappa.drv
  56. share/why3/drivers/iprover.drv
  57. share/why3/drivers/isabelle-common.gen
  58. share/why3/drivers/isabelle-realizations.aux
  59. share/why3/drivers/isabelle-realize.drv
  60. share/why3/drivers/isabelle.drv
  61. share/why3/drivers/mathematica.drv
  62. share/why3/drivers/mathsat.drv
  63. share/why3/drivers/metis.drv
  64. share/why3/drivers/metitarski.drv
  65. share/why3/drivers/ocaml-gen.drv
  66. share/why3/drivers/ocaml32.drv
  67. share/why3/drivers/ocaml64.drv
  68. share/why3/drivers/princess.drv
  69. share/why3/drivers/pvs-common.gen
  70. share/why3/drivers/pvs-realizations.aux
  71. share/why3/drivers/pvs-realize.drv
  72. share/why3/drivers/pvs.drv
  73. share/why3/drivers/simplify.drv
  74. share/why3/drivers/spass.drv
  75. share/why3/drivers/spass_types.drv
  76. share/why3/drivers/tptp-tff0.drv
  77. share/why3/drivers/tptp-tff1.drv
  78. share/why3/drivers/tptp.gen
  79. share/why3/drivers/vampire.drv
  80. share/why3/drivers/verit.drv
  81. share/why3/drivers/why3.drv
  82. share/why3/drivers/why3_smt.drv
  83. share/why3/drivers/why3_tptp.drv
  84. share/why3/drivers/yices.drv
  85. share/why3/drivers/yices_bare.drv
  86. share/why3/drivers/z3.drv
  87. share/why3/drivers/z3_bare.drv
  88. share/why3/drivers/z3_smtv1.drv
  89. share/why3/drivers/zenon.drv
  90. share/why3/emacs/why3.el
  91. share/why3/images/boomy/accept32.png
  92. share/why3/images/boomy/bug32.png
  93. share/why3/images/boomy/clock32.png
  94. share/why3/images/boomy/configure16.png
  95. share/why3/images/boomy/configure32.png
  96. share/why3/images/boomy/cut32.png
  97. share/why3/images/boomy/cutb32.png
  98. share/why3/images/boomy/delete32.png
  99. share/why3/images/boomy/deletefile32.png
  100. share/why3/images/boomy/edit32.png
  101. share/why3/images/boomy/file16.png
  102. share/why3/images/boomy/file32.png
  103. share/why3/images/boomy/folder16.png
  104. share/why3/images/boomy/folder32.png
  105. share/why3/images/boomy/help32.png
  106. share/why3/images/boomy/movefile32.png
  107. share/why3/images/boomy/obsaccept32.png
  108. share/why3/images/boomy/obsbug32.png
  109. share/why3/images/boomy/obsclock32.png
  110. share/why3/images/boomy/obsdelete32.png
  111. share/why3/images/boomy/obsdeletefile32.png
  112. share/why3/images/boomy/obshelp32.png
  113. share/why3/images/boomy/pause32.png
  114. share/why3/images/boomy/pausehalf32.png
  115. share/why3/images/boomy/play32.png
  116. share/why3/images/boomy/refresh32.png
  117. share/why3/images/boomy/stop32.png
  118. share/why3/images/boomy/transformation32.png
  119. share/why3/images/boomy/trashb32.png
  120. share/why3/images/boomy/undone32.png
  121. share/why3/images/boomy/wizard16.png
  122. share/why3/images/boomy/wizard32.png
  123. share/why3/images/fatcow/accept.png
  124. share/why3/images/fatcow/bin.png
  125. share/why3/images/fatcow/bomb.png
  126. share/why3/images/fatcow/bullet_black.png
  127. share/why3/images/fatcow/bullet_blue.png
  128. share/why3/images/fatcow/bullet_green.png
  129. share/why3/images/fatcow/bullet_red.png
  130. share/why3/images/fatcow/bullet_white.png
  131. share/why3/images/fatcow/cancel.png
  132. share/why3/images/fatcow/control_pause_blue.png
  133. share/why3/images/fatcow/control_play_blue.png
  134. share/why3/images/fatcow/ddr_memory.png
  135. share/why3/images/fatcow/delete.png
  136. share/why3/images/fatcow/exclamation.png
  137. share/why3/images/fatcow/folder.png
  138. share/why3/images/fatcow/help.png
  139. share/why3/images/fatcow/magic_wand_2.png
  140. share/why3/images/fatcow/multitool.png
  141. share/why3/images/fatcow/package.png
  142. share/why3/images/fatcow/pencil.png
  143. share/why3/images/fatcow/script.png
  144. share/why3/images/fatcow/timeline.png
  145. share/why3/images/fatcow/update.png
  146. share/why3/images/icons.rc
  147. share/why3/images/logo-why.png
  148. share/why3/javascript/jquery.js
  149. share/why3/javascript/jquery.jstree.js
  150. share/why3/javascript/session.css
  151. share/why3/javascript/session.js
  152. share/why3/javascript/themes/default/d.gif
  153. share/why3/javascript/themes/default/d.png
  154. share/why3/javascript/themes/default/style.css
  155. share/why3/javascript/themes/default/throbber.gif
  156. share/why3/lang/why3.lang
  157. share/why3/modules/array.mlw
  158. share/why3/modules/hashtbl.mlw
  159. share/why3/modules/impset.mlw
  160. share/why3/modules/mach/array.mlw
  161. share/why3/modules/mach/int.mlw
  162. share/why3/modules/matrix.mlw
  163. share/why3/modules/pqueue.mlw
  164. share/why3/modules/queue.mlw
  165. share/why3/modules/random.mlw
  166. share/why3/modules/ref.mlw
  167. share/why3/modules/stack.mlw
  168. share/why3/modules/string.mlw
  169. share/why3/provers-detection-data.conf
  170. share/why3/theories/algebra.why
  171. share/why3/theories/bag.why
  172. share/why3/theories/bintree.why
  173. share/why3/theories/bool.why
  174. share/why3/theories/comparison.why
  175. share/why3/theories/floating_point.why
  176. share/why3/theories/function.why
  177. share/why3/theories/graph.why
  178. share/why3/theories/int.why
  179. share/why3/theories/list.why
  180. share/why3/theories/map.why
  181. share/why3/theories/number.why
  182. share/why3/theories/option.why
  183. share/why3/theories/pigeon.why
  184. share/why3/theories/real.why
  185. share/why3/theories/regexp.why
  186. share/why3/theories/relations.why
  187. share/why3/theories/set.why
  188. share/why3/theories/sum.why
  189. share/why3/theories/tptp.why
  190. share/why3/vim/why3.vim
  191. share/why3/why3session.dtd
  192. Collapse this list.

To install the port: cd /usr/ports/math/why3/ && make install clean
To add the package: pkg install why3

PKGNAME: why3

distinfo:

SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9
SIZE (why3-0.83.tar.gz) = 5347628


NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.

Build dependencies:
  1. ocaml-zarith>1.2 : math/ocaml-zarith
  2. lablgtk2 : x11-toolkits/ocaml-lablgtk2
  3. ocaml-sqlite3>2 : databases/ocaml-sqlite3
  4. ocaml-ocamlgraph>1.8 : math/ocaml-ocamlgraph
  5. camlp5o : devel/ocaml-camlp5
  6. ocamlc : lang/ocaml
  7. ocamlfind : devel/ocaml-findlib
  8. gmake : devel/gmake
Runtime dependencies:
  1. ocamlc : lang/ocaml
  2. ocamlfind : devel/ocaml-findlib
Patch dependencies:
  1. ocamlc : lang/ocaml
Extract dependencies:
  1. ocamlc : lang/ocaml
There are no ports dependent upon this port

Configuration Options
===> The following configuration options are available for why3-0.83_2:
     DOCS=on: Build and/or install documentation
===> Use 'make config' to modify these settings

USES:
gmake

Master Sites:
  1. http://gforge.inria.fr/frs/download.php/33490/
  2. http://pkgs.fedoraproject.org/repo/pkgs/why3/why3-0.83.tar.gz/35f99e5f64939e50ea57f641ba2073ec/

Number of commits found: 12

Commit History - (may be incomplete: see SVNWeb link above for full details)
DateByDescription
29 Jan 2017 23:39:24
Original commit files touched by this commit  0.83_2
Revision:432811
marino search for other commits by this committer
math/why3: Unbreak after ocaml-findlib change

Use the same technique madpilot used on x11-toolkits/ocaml-lablgtk2
to restore the build after the (unexpected) changed to the output
of ocamlfindlib during its update to 1.7.1

While here, document previously unknown ocamlfind requirement.
01 Apr 2016 14:16:20
Original commit files touched by this commit  0.83_2
Revision:412348
mat search for other commits by this committer
Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p.

With hat:	portmgr
Sponsored by:	Absolight
10 Feb 2016 16:14:35
Original commit files touched by this commit  0.83_2
Revision:408636
ak search for other commits by this committer
- Fix various typos in CONFLICTS_INSTALL knob

Approved by:	portmgr blanket
20 Nov 2015 09:17:20
Original commit files touched by this commit  0.83_2
Revision:402062
sunpoet search for other commits by this committer
- Add LICENSE_FILE
- Strip object files
- Bump PORTREVISION for package change
28 Aug 2015 13:39:57
Original commit files touched by this commit  0.83_1
Revision:395483
amdmi3 search for other commits by this committer
- Switch to options helpers
- While here, add some NO_ARCHes and couple missing PORT_OPTIONS=DOCS

Approved by:	portmgr blanket
29 Jul 2015 17:49:13
Original commit files touched by this commit  0.83_1
Revision:393189
amdmi3 search for other commits by this committer
- Strip binaries
28 Jun 2015 07:11:24
Original commit files touched by this commit  0.83_1
Revision:390740
marino search for other commits by this committer
math/why3: Release port

I only care about math/why3-gpl, which has been decoupled from why3 and
has already diverged.  Before resetting MAINTAINER, I reintegrated the
Makefile.common file (only used by this port) into the main Makefile. In
the process, some options placeholders were lost but in all probability
these options can't be built without serious work on external ports.
01 Mar 2015 21:14:57
Original commit files touched by this commit  0.83_1
Revision:380227
marino search for other commits by this committer
math/why: remove hidden references to math/isabelle

There was a placeholder to support isabelle, but the port is being
removed so let's just remove the placeholder.
14 Nov 2014 09:39:21
Original commit files touched by this commit  0.83_1
Revision:372555
antoine search for other commits by this committer
Cleanup plist
03 Sep 2014 15:03:05
Original commit files touched by this commit  0.83_1
Revision:367210
antoine search for other commits by this committer
Fix packaging
05 Jul 2014 12:19:33
Original commit files touched by this commit  0.83_1
Revision:360738
tijl search for other commits by this committer
Bump more ports that depend on libsqlite3.so:
- ports that set USE_SQLITE with the *_USE option helper
- ports that depend on libsqlite3 indirectly as reported by pkg rquery

Approved by:	portmgr (implicit)
04 Jun 2014 19:22:34
Original commit files touched by this commit  0.83
Revision:356538
marino search for other commits by this committer
Add two new math ports: why3 and why3-gpl

The primary motivation for adding why3 is to support the upcoming SPARK
2014 port.  However, SPARK 2014 requires a custom version.  In time the
customizations should make it upstream, but currently the stock version
cannot be used to build SPARK.  They are also licensed differently (LGPL2
for stock, GPLv3 for SPARK version).

Rather than force people that find why3 useful on their own to accept a
custom version, both are offered although they currently conflict.

Why3 has optional dependencies on coq, isabelle, and frama-c, and all
three have issus:
  * coq rebuilds its libraries in $LOCALBASE, could be issue with coq
  * isabella currently has a broken dependency (sjsml) and only for i386
(Only the first 15 lines of the commit message are shown above View all of this commit message)

Number of commits found: 12

Login
User Login
Create account

Servers and bandwidth provided by
New York Internet, SuperNews, and RootBSD

This site
What is FreshPorts?
About the authors
Issues
FAQ
How big is it?
The latest upgrade!
Privacy
Forums
Blog
Contact

Search
Enter Keywords:
 
more...

Latest Vulnerabilities
opensslNov 02
openssl-develNov 02
wordpressNov 01
php56Oct 30
php70Oct 30
php71Oct 30
wiresharkOct 30
chromiumOct 28
wgetOct 27
wgetOct 27
openoffice-4*Oct 26
openoffice-devel*Oct 26
gitlabOct 25
nodeOct 25
node4Oct 25

No vulnerabilities have been reported in the past 14 days

* - modified, not new

All vulnerabilities


Ports
Home
Categories
Deleted ports
Sanity Test Failures
Newsfeeds

Statistics
Graphs
NEW Graphs (Javascript)
Traffic

Calculated hourly:
Port count 31887
Broken 126
Deprecated 46
Ignore 362
Forbidden 0
Restricted 173
No CDROM 78
Vulnerable 48
Expired 11
Set to expire 38
Interactive 0
new 24 hours 14
new 48 hours91
new 7 days3239
new fortnight3281
new month3474

Servers and bandwidth provided by
New York Internet, SuperNews, and RootBSD
Valid HTML, CSS, and RSS.
Copyright © 2000-2017 Dan Langille. All rights reserved.