notbugAs an Amazon Associate I earn from qualifying purchases.
Want a good read? Try FreeBSD Mastery: Jails (IT Mastery Book 15)
Want a good monitor light? See my photosAll times are UTC
Ukraine
This referral link gives you 10% off a Fastmail.com account and gives me a discount on my Fastmail account.

Get notified when packages are built

A new feature has been added. FreshPorts already tracks package built by the FreeBSD project. This information is displayed on each port page. You can now get an email when FreshPorts notices a new package is available for something on one of your watch lists. However, you must opt into that. Click on Report Subscriptions on the right, and New Package Notification box, and click on Update.

FInally, under Watch Lists, click on ABI Package Subscriptions to select your ABI (e.g. FreeBSD:14:amd64) & package set (latest/quarterly) combinatio for a given watch list. This is what FreshPorts will look for.

Port details
why3 Deductive program verification platform
0.83_2 math Deleted 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 View this port on Repology. pkg-fallout 0.83_2Version of this port present on the latest quarterly branch.
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: 2014-06-04 19:22:50
Last Update: 2021-02-04 09:58:34
SVN Revision: 564008
License: LGPL21
WWW:
http://why3.lri.fr
Description:
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
Homepage    cgit ¦ GitHub ¦ GitHub ¦ GitLab ¦ SVNWeb

Manual pages:
FreshPorts has no man page information for this port.
pkg-plist: as obtained via: make generate-plist
Expand this list (191 items)
Collapse this list.
  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
Collapse this list.
Dependency lines:
  • why3>0:math/why3
Conflicts:
CONFLICTS_INSTALL:
  • why3-gpl-*
Conflicts Matches:
There are no Conflicts Matches for this port. This is usually an error.
No installation instructions:
This port has been deleted.
PKGNAME: why3
Flavors: there is no flavor information for this port.
distinfo:
SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9 SIZE (why3-0.83.tar.gz) = 5347628

No package information for this port in our database
Sometimes this happens. Not all ports have packages.
Dependencies
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
Options name:
N/A
USES:
gmake
FreshPorts was unable to extract/find any pkg message
Master Sites:
Expand this list (2 items)
Collapse this list.
  1. http://gforge.inria.fr/frs/download.php/33490/
  2. http://pkgs.fedoraproject.org/repo/pkgs/why3/why3-0.83.tar.gz/35f99e5f64939e50ea57f641ba2073ec/
Collapse this list.
Port Moves
  • port deleted on 2021-02-04
    REASON: Depends on deprecated gnome2 library, very outdated and unmaintained

Number of commits found: 13

Commit History - (may be incomplete: for full details, see links to repositories near top of page)
CommitCreditsLog message
0.83_2
04 Feb 2021 09:58:34
Revision:564008Original commit files touched by this commit
bapt search for other commits by this committer
Remove math/why3

This port depends on deprecated gnome2 only libraries, the port is unmaintained
for
a while and very outdated.
0.83_2
29 Jan 2017 23:39:24
Revision:432811Original commit files touched by this commit
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.
0.83_2
01 Apr 2016 14:16:20
Revision:412348Original commit files touched by this commit
mat search for other commits by this committer
Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p.

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

Approved by:	portmgr blanket
0.83_2
20 Nov 2015 09:17:20
Revision:402062Original commit files touched by this commit
sunpoet search for other commits by this committer
- Add LICENSE_FILE
- Strip object files
- Bump PORTREVISION for package change
0.83_1
28 Aug 2015 13:39:57
Revision:395483Original commit files touched by this commit
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
0.83_1
29 Jul 2015 17:49:13
Revision:393189Original commit files touched by this commit
amdmi3 search for other commits by this committer
- Strip binaries
0.83_1
28 Jun 2015 07:11:24
Revision:390740Original commit files touched by this commit
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.
0.83_1
01 Mar 2015 21:14:57
Revision:380227Original commit files touched by this commit
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.
0.83_1
14 Nov 2014 09:39:21
Revision:372555Original commit files touched by this commit
antoine search for other commits by this committer
Cleanup plist
0.83_1
03 Sep 2014 15:03:05
Revision:367210Original commit files touched by this commit
antoine search for other commits by this committer
Fix packaging
0.83_1
05 Jul 2014 12:19:33
Revision:360738Original commit files touched by this commit
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)
0.83
04 Jun 2014 19:22:34
Revision:356538Original commit files touched by this commit
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: 13