why3-1.2.0-5.fc31.x86_64.rpm


Advertisement

Description

why3 - Software verification platform

Property Value
Distribution Fedora 31
Repository Fedora x86_64
Package filename why3-1.2.0-5.fc31.x86_64.rpm
Package name why3
Package version 1.2.0
Package release 5.fc31
Package architecture x86_64
Package type rpm
Homepage http://why3.lri.fr/
License LGPLv2 with exceptions
Maintainer -
Download size 35.33 MB
Installed size 141.60 MB
Why3 is the next generation of the Why software verification platform.
Why3 clearly separates the purely logical specification part from
generation of verification conditions for programs.  It features a rich
library of proof task transformations that can be chained to produce a
suitable input for a large set of theorem provers, including SMT
solvers, TPTP provers, as well as interactive proof assistants.

Alternatives

Package Version Architecture Repository
why3-1.2.1-1.fc31.x86_64.rpm 1.2.1 x86_64 Fedora Updates
why3-1.2.0-5.fc31.x86_64.rpm 1.2.0 x86_64 Fedora Updates Testing
why3 - - -

Requires

Name Value
/usr/bin/sh -
gtksourceview2 -
libc.so.6(GLIBC_2.28)(64bit) -
libdl.so.2()(64bit) -
libdl.so.2(GLIBC_2.2.5)(64bit) -
libgdk-x11-2.0.so.0()(64bit) -
libgdk_pixbuf-2.0.so.0()(64bit) -
libglib-2.0.so.0()(64bit) -
libgobject-2.0.so.0()(64bit) -
libgtk-x11-2.0.so.0()(64bit) -
libgtksourceview-2.0.so.0()(64bit) -
libm.so.6()(64bit) -
libm.so.6(GLIBC_2.2.5)(64bit) -
libm.so.6(GLIBC_2.29)(64bit) -
libpango-1.0.so.0()(64bit) -
libz.so.1()(64bit) -
rtld(GNU_HASH) -
texlive-base -
vim-filesystem -

Provides

Name Value
bundled(jquery) -
why3 = 1.2.0-5.fc31
why3(x86-64) = 1.2.0-5.fc31

Download

Type URL
Mirror download-ib01.fedoraproject.org
Binary Package why3-1.2.0-5.fc31.x86_64.rpm
Source Package why3-1.2.0-5.fc31.src.rpm

Install Howto

Install why3 rpm package:

# dnf install why3

Files

Path
/usr/bin/why3
/usr/lib/.build-id/
/usr/lib/.build-id/05/1d2ea85e84f94c5a7fde934927167d170199ae
/usr/lib/.build-id/15/3471b02bb7d15fb815e016726d9390365b5f89
/usr/lib/.build-id/3e/2e9da168008f5b1a0a3788eaa556a0a1dbba02
/usr/lib/.build-id/4a/04f3e3c5f087a898ae08604f07e8cf279c9283
/usr/lib/.build-id/4e/8d701560b36f3dfd3635d93032eff6c16114f8
/usr/lib/.build-id/50/d475aef45b57f69229015729a0edaaf8c98a44
/usr/lib/.build-id/69/e50fca9a230aa02163ace46572b02b415452a5
/usr/lib/.build-id/69/e50fca9a230aa02163ace46572b02b415452a5.1
/usr/lib/.build-id/69/e50fca9a230aa02163ace46572b02b415452a5.2
/usr/lib/.build-id/82/649ee151c01be0ec6c453542e4bc1282dde5f1
/usr/lib/.build-id/82/a5d3d6cacbf3c31071404f8d4ebc6a1f3cf956
/usr/lib/.build-id/84/8591eed5bf2705c0331720a6db2a211c3ffa8a
/usr/lib/.build-id/89/b8c058b5dd94667990a76c90fe23876ee90690
/usr/lib/.build-id/8c/0b3bea4eeefc0cf5b4d90a4d138cb25dd4041a
/usr/lib/.build-id/9a/c406f243aa8b499e423757a6dc7dae39e50062
/usr/lib/.build-id/a0/32db24c1acaba500b88f36889a95ffafbe64b2
/usr/lib/.build-id/b0/6b57eb3f40da3079b6b119727fc52a87d687ae
/usr/lib/.build-id/d9/07038cc533849c4908bb76d63484a7b428ca25
/usr/lib/.build-id/ec/9bab0dbc40168835dca6bf5d601c0b2cb53a26
/usr/lib/.build-id/ef/51fbea1d78cd62112f9307540559104fa75d17
/usr/lib64/why3/why3-call-pvs
/usr/lib64/why3/why3cpulimit
/usr/lib64/why3/why3server
/usr/lib64/why3/commands/why3config
/usr/lib64/why3/commands/why3doc
/usr/lib64/why3/commands/why3execute
/usr/lib64/why3/commands/why3extract
/usr/lib64/why3/commands/why3ide
/usr/lib64/why3/commands/why3prove
/usr/lib64/why3/commands/why3realize
/usr/lib64/why3/commands/why3replay
/usr/lib64/why3/commands/why3session
/usr/lib64/why3/commands/why3shell
/usr/lib64/why3/commands/why3wc
/usr/lib64/why3/commands/why3webserver
/usr/lib64/why3/coq/BuiltIn.vo
/usr/lib64/why3/coq/HighOrd.vo
/usr/lib64/why3/coq/version
/usr/lib64/why3/coq/bool/Bool.vo
/usr/lib64/why3/coq/bv/BV_Gen.vo
/usr/lib64/why3/coq/bv/Pow2int.vo
/usr/lib64/why3/coq/floating_point/Double.vo
/usr/lib64/why3/coq/floating_point/DoubleFormat.vo
/usr/lib64/why3/coq/floating_point/GenFloat.vo
/usr/lib64/why3/coq/floating_point/Rounding.vo
/usr/lib64/why3/coq/floating_point/Single.vo
/usr/lib64/why3/coq/floating_point/SingleFormat.vo
/usr/lib64/why3/coq/for_drivers/ComputerOfEuclideanDivision.vo
/usr/lib64/why3/coq/ieee_float/Float32.vo
/usr/lib64/why3/coq/ieee_float/Float64.vo
/usr/lib64/why3/coq/ieee_float/GenericFloat.vo
/usr/lib64/why3/coq/ieee_float/RoundingMode.vo
/usr/lib64/why3/coq/int/Abs.vo
/usr/lib64/why3/coq/int/ComputerDivision.vo
/usr/lib64/why3/coq/int/Div2.vo
/usr/lib64/why3/coq/int/EuclideanDivision.vo
/usr/lib64/why3/coq/int/Exponentiation.vo
/usr/lib64/why3/coq/int/Int.vo
/usr/lib64/why3/coq/int/MinMax.vo
/usr/lib64/why3/coq/int/NumOf.vo
/usr/lib64/why3/coq/int/Power.vo
/usr/lib64/why3/coq/list/Append.vo
/usr/lib64/why3/coq/list/Combine.vo
/usr/lib64/why3/coq/list/Distinct.vo
/usr/lib64/why3/coq/list/HdTl.vo
/usr/lib64/why3/coq/list/HdTlNoOpt.vo
/usr/lib64/why3/coq/list/Length.vo
/usr/lib64/why3/coq/list/List.vo
/usr/lib64/why3/coq/list/Mem.vo
/usr/lib64/why3/coq/list/Nth.vo
/usr/lib64/why3/coq/list/NthHdTl.vo
/usr/lib64/why3/coq/list/NthLength.vo
/usr/lib64/why3/coq/list/NthLengthAppend.vo
/usr/lib64/why3/coq/list/NthNoOpt.vo
/usr/lib64/why3/coq/list/NumOcc.vo
/usr/lib64/why3/coq/list/Permut.vo
/usr/lib64/why3/coq/list/RevAppend.vo
/usr/lib64/why3/coq/list/Reverse.vo
/usr/lib64/why3/coq/map/Const.vo
/usr/lib64/why3/coq/map/Map.vo
/usr/lib64/why3/coq/map/MapInjection.vo
/usr/lib64/why3/coq/map/MapPermut.vo
/usr/lib64/why3/coq/map/Occ.vo
/usr/lib64/why3/coq/number/Coprime.vo
/usr/lib64/why3/coq/number/Divisibility.vo
/usr/lib64/why3/coq/number/Gcd.vo
/usr/lib64/why3/coq/number/Parity.vo
/usr/lib64/why3/coq/number/Prime.vo
/usr/lib64/why3/coq/option/Option.vo
/usr/lib64/why3/coq/real/Abs.vo
/usr/lib64/why3/coq/real/ExpLog.vo
/usr/lib64/why3/coq/real/FromInt.vo
/usr/lib64/why3/coq/real/MinMax.vo
/usr/lib64/why3/coq/real/PowerInt.vo
/usr/lib64/why3/coq/real/PowerReal.vo
/usr/lib64/why3/coq/real/Real.vo
/usr/lib64/why3/coq/real/RealInfix.vo
/usr/lib64/why3/coq/real/Square.vo
/usr/lib64/why3/coq/real/Trigonometry.vo
/usr/lib64/why3/coq/real/Truncate.vo
/usr/lib64/why3/coq/set/Set.vo
/usr/lib64/why3/plugins/dimacs.cmxs
/usr/lib64/why3/plugins/genequlin.cmxs
/usr/lib64/why3/plugins/hypothesis_selection.cmxs
/usr/lib64/why3/plugins/python.cmxs
/usr/lib64/why3/plugins/tptp.cmxs
/usr/share/bash-completion/
/usr/share/bash-completion/completions/why3
/usr/share/doc/why3/AUTHORS
/usr/share/doc/why3/CHANGES.md
/usr/share/doc/why3/README.md
/usr/share/doc/why3/manual.pdf
/usr/share/gtksourceview-2.0/language-specs/why3.lang
/usr/share/licenses/why3/LICENSE
/usr/share/man/man1/why3-cpulimit.1.gz
/usr/share/man/man1/why3.1.gz
/usr/share/man/man1/why3bench.1.gz
/usr/share/man/man1/why3config.1.gz
/usr/share/man/man1/why3doc.1.gz
/usr/share/man/man1/why3ide.1.gz
/usr/share/man/man1/why3ml.1.gz
/usr/share/man/man1/why3realize.1.gz
/usr/share/man/man1/why3replayer.1.gz
/usr/share/texlive/texmf-local/tex/latex/why3/why3lang.sty
/usr/share/vim/vimfiles/ftdetect/why3.vim
/usr/share/vim/vimfiles/syntax/why3.vim
/usr/share/why3/LICENSE
/usr/share/why3/Makefile.config
/usr/share/why3/provers-detection-data.conf
/usr/share/why3/why3session.dtd
/usr/share/why3/drivers/alt_ergo.drv
/usr/share/why3/drivers/alt_ergo_common.drv
/usr/share/why3/drivers/alt_ergo_fp.drv
/usr/share/why3/drivers/alt_ergo_model.drv
/usr/share/why3/drivers/alt_ergo_smt2.drv
/usr/share/why3/drivers/beagle.drv
/usr/share/why3/drivers/c.drv
/usr/share/why3/drivers/cakeml.drv
/usr/share/why3/drivers/coq-common.gen
/usr/share/why3/drivers/coq-realizations.aux
/usr/share/why3/drivers/coq-realize.drv
/usr/share/why3/drivers/coq-ssreflect.drv
/usr/share/why3/drivers/coq.drv
/usr/share/why3/drivers/cvc3.drv
/usr/share/why3/drivers/cvc4-realize.drv
/usr/share/why3/drivers/cvc4.drv
/usr/share/why3/drivers/cvc4_14.drv
/usr/share/why3/drivers/cvc4_15.drv
/usr/share/why3/drivers/cvc4_15_counterexample.drv
/usr/share/why3/drivers/cvc4_16.drv
/usr/share/why3/drivers/cvc4_16_counterexample.drv
/usr/share/why3/drivers/cvc4_bv.gen
/usr/share/why3/drivers/discrimination.gen
/usr/share/why3/drivers/eprover.drv
/usr/share/why3/drivers/gappa.drv
/usr/share/why3/drivers/iprover.drv
/usr/share/why3/drivers/isabelle-2017.gen
/usr/share/why3/drivers/isabelle-2018.gen
/usr/share/why3/drivers/isabelle-common.gen
/usr/share/why3/drivers/isabelle-realizations.aux
/usr/share/why3/drivers/isabelle2017-realize.drv
/usr/share/why3/drivers/isabelle2017.drv
/usr/share/why3/drivers/isabelle2018-realize.drv
/usr/share/why3/drivers/isabelle2018.drv
/usr/share/why3/drivers/mathematica.drv
/usr/share/why3/drivers/mathsat.drv
/usr/share/why3/drivers/metis.drv
/usr/share/why3/drivers/metitarski.drv
/usr/share/why3/drivers/no-bv.gen
/usr/share/why3/drivers/ocaml-unsafe-int.drv
/usr/share/why3/drivers/ocaml64.drv
/usr/share/why3/drivers/polypaver.drv
/usr/share/why3/drivers/princess.drv
/usr/share/why3/drivers/psyche.drv
/usr/share/why3/drivers/pvs-common.gen
/usr/share/why3/drivers/pvs-realizations.aux
/usr/share/why3/drivers/pvs-realize.drv
/usr/share/why3/drivers/pvs.drv
/usr/share/why3/drivers/safeprover.drv
/usr/share/why3/drivers/simplify.drv
/usr/share/why3/drivers/smt-libv2-bv-realization.gen
/usr/share/why3/drivers/smt-libv2-bv.gen
/usr/share/why3/drivers/smt-libv2-floats-gnatprove.gen
/usr/share/why3/drivers/smt-libv2-floats-int_via_bv.gen
/usr/share/why3/drivers/smt-libv2-floats-int_via_real.gen
/usr/share/why3/drivers/smt-libv2-floats.gen
/usr/share/why3/drivers/smt-libv2-gnatprove.gen
/usr/share/why3/drivers/smt-libv2.drv
/usr/share/why3/drivers/smt-libv2.gen
/usr/share/why3/drivers/spass.drv
/usr/share/why3/drivers/spass_types.drv
/usr/share/why3/drivers/tptp-tff0.drv
/usr/share/why3/drivers/tptp-tff1.drv
/usr/share/why3/drivers/tptp.gen
/usr/share/why3/drivers/vampire.drv
/usr/share/why3/drivers/verit.drv
/usr/share/why3/drivers/why3.drv
/usr/share/why3/drivers/why3_smt.drv
/usr/share/why3/drivers/why3_tptp.drv
/usr/share/why3/drivers/yices-smt2.drv
/usr/share/why3/drivers/yices.drv
/usr/share/why3/drivers/z3.drv
/usr/share/why3/drivers/z3_432.drv
/usr/share/why3/drivers/z3_440.drv
/usr/share/why3/drivers/z3_440_counterexample.drv
/usr/share/why3/drivers/z3_bv.gen
/usr/share/why3/drivers/z3_smtv1.drv
/usr/share/why3/drivers/zenon.drv
/usr/share/why3/drivers/zenon_modulo.drv
/usr/share/why3/images/fatcow.rc
/usr/share/why3/images/logo-why.png
/usr/share/why3/images/fatcow/accept.png
/usr/share/why3/images/fatcow/bin.png
/usr/share/why3/images/fatcow/bomb.png
/usr/share/why3/images/fatcow/brick_delete.png
/usr/share/why3/images/fatcow/bullet_black.png
/usr/share/why3/images/fatcow/bullet_blue.png
/usr/share/why3/images/fatcow/bullet_green.png
/usr/share/why3/images/fatcow/bullet_red.png
/usr/share/why3/images/fatcow/bullet_white.png
/usr/share/why3/images/fatcow/cancel.png
/usr/share/why3/images/fatcow/control_pause_blue.png
/usr/share/why3/images/fatcow/control_play_blue.png
/usr/share/why3/images/fatcow/database_delete.png
/usr/share/why3/images/fatcow/ddr_memory.png
/usr/share/why3/images/fatcow/delete.png
/usr/share/why3/images/fatcow/exclamation.png
/usr/share/why3/images/fatcow/folder.png
/usr/share/why3/images/fatcow/help.png
/usr/share/why3/images/fatcow/magic_wand_2.png
/usr/share/why3/images/fatcow/multitool.png
/usr/share/why3/images/fatcow/package.png
/usr/share/why3/images/fatcow/pencil.png
/usr/share/why3/images/fatcow/readme-fatcow.txt
/usr/share/why3/images/fatcow/script.png
/usr/share/why3/images/fatcow/time_delete.png
/usr/share/why3/images/fatcow/timeline.png
/usr/share/why3/images/fatcow/update.png
/usr/share/why3/stdlib/algebra.mlw
/usr/share/why3/stdlib/appmap.mlw
/usr/share/why3/stdlib/appset.mlw
/usr/share/why3/stdlib/array.mlw
/usr/share/why3/stdlib/bag.mlw
/usr/share/why3/stdlib/bintree.mlw
/usr/share/why3/stdlib/bool.mlw
/usr/share/why3/stdlib/bv.mlw
/usr/share/why3/stdlib/cursor.mlw
/usr/share/why3/stdlib/debug.mlw
/usr/share/why3/stdlib/exn.mlw
/usr/share/why3/stdlib/floating_point.mlw
/usr/share/why3/stdlib/for_drivers.mlw
/usr/share/why3/stdlib/function.mlw
/usr/share/why3/stdlib/graph.mlw
/usr/share/why3/stdlib/hashtbl.mlw
/usr/share/why3/stdlib/ieee_float.mlw
/usr/share/why3/stdlib/impmap.mlw
/usr/share/why3/stdlib/impset.mlw
/usr/share/why3/stdlib/int.mlw
/usr/share/why3/stdlib/io.mlw
/usr/share/why3/stdlib/list.mlw
/usr/share/why3/stdlib/map.mlw
/usr/share/why3/stdlib/matrix.mlw
/usr/share/why3/stdlib/null.mlw
/usr/share/why3/stdlib/number.mlw
/usr/share/why3/stdlib/ocaml.mlw
/usr/share/why3/stdlib/option.mlw
/usr/share/why3/stdlib/pigeon.mlw
/usr/share/why3/stdlib/pqueue.mlw
/usr/share/why3/stdlib/python.mlw
/usr/share/why3/stdlib/queue.mlw
/usr/share/why3/stdlib/random.mlw
/usr/share/why3/stdlib/real.mlw
/usr/share/why3/stdlib/ref.mlw
/usr/share/why3/stdlib/regexp.mlw
/usr/share/why3/stdlib/relations.mlw
/usr/share/why3/stdlib/seq.mlw
/usr/share/why3/stdlib/set.mlw
/usr/share/why3/stdlib/stack.mlw
/usr/share/why3/stdlib/string.mlw
/usr/share/why3/stdlib/sum.mlw
/usr/share/why3/stdlib/tptp.mlw
/usr/share/why3/stdlib/tree.mlw
/usr/share/why3/stdlib/witness.mlw
/usr/share/why3/stdlib/mach/array.mlw
/usr/share/why3/stdlib/mach/bv.mlw
/usr/share/why3/stdlib/mach/c.mlw
/usr/share/why3/stdlib/mach/float.mlw
/usr/share/why3/stdlib/mach/int.mlw
/usr/share/why3/stdlib/mach/matrix.mlw
/usr/share/why3/stdlib/mach/onetime.mlw
/usr/share/why3/stdlib/mach/peano.mlw
/usr/share/why3/vim/
/usr/share/zsh/
/usr/share/zsh/site-functions/_why3

Changelog

2019-09-06 - Jerry James <loganjerry@gmail.com> - 1.2.0-5
- Rebuild for ocaml-zarith 1.9
2019-08-01 - Jerry James <loganjerry@gmail.com> - 1.2.0-4
- Also install the library, for consumption by frama-c
2019-08-01 - Jerry James <loganjerry@gmail.com> - 1.2.0-3
- Rebuild for flocq 3.2.0
2019-07-27 - Fedora Release Engineering <releng@fedoraproject.org> - 1.2.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
2019-06-05 - Jerry James <loganjerry@gmail.com> - 1.2.0-1
- New upstream release
2019-02-03 - Fedora Release Engineering <releng@fedoraproject.org> - 1.1.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
2019-01-26 - Jerry James <loganjerry@gmail.com> - 1.1.1-1
- New upstream release
2018-07-14 - Fedora Release Engineering <releng@fedoraproject.org> - 0.88.3-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
2018-07-12 - Richard W.M. Jones <rjones@redhat.com> - 0.88.3-4
- OCaml 4.07.0 (final) rebuild.
2018-06-20 - Richard W.M. Jones <rjones@redhat.com> - 0.88.3-3
- Bump release and rebuild.

See Also

Package Description
why3-all-1.2.0-5.fc31.x86_64.rpm Complete Why3 software verification platform suite
why3-emacs-1.2.0-5.fc31.noarch.rpm Emacs support file for why3 files
why3-examples-1.2.0-5.fc31.noarch.rpm Example inputs
why3-xemacs-1.2.0-5.fc31.noarch.rpm XEmacs support file for why3 files
whysynth-dssi-20120903-9.fc31.x86_64.rpm DSSI software synthesizer plugin
wicd-kde-0.3.1-16.fc31.x86_64.rpm A Wicd client built on the KDE Development Platform
wide-dhcpv6-20080615-13.1.fc31.9.x86_64.rpm DHCP Client and Server for IPv6
widelands-0-0.72.build20.fc31.x86_64.rpm Open source realtime-strategy game
wifi-radar-2.0.s10-11.fc31.noarch.rpm A utility for managing WiFi profiles
wiggle-1.1-4.fc31.x86_64.rpm A tool for applying patches with conflicts
wiiuse-0.15.4-3.fc31.i686.rpm The wiiuse library is used to access and control multiple Nintendo Wiimotes
wiiuse-0.15.4-3.fc31.x86_64.rpm The wiiuse library is used to access and control multiple Nintendo Wiimotes
wiiuse-devel-0.15.4-3.fc31.i686.rpm Developer tools for the wiiuse library
wiiuse-devel-0.15.4-3.fc31.x86_64.rpm Developer tools for the wiiuse library
wiiuse-examples-0.15.4-3.fc31.x86_64.rpm Example programs for the wiiuse library
Advertisement
Advertisement