Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
54c75717
Commit
54c75717
authored
Nov 06, 2017
by
Guillaume Melquiond
Browse files
Convert README, INSTALL, and CHANGES to markdown.
parent
dd12e66e
Changes
4
Expand all
Hide whitespace changes
Inline
Side-by-side
CHANGES
deleted
100644 → 0
View file @
dd12e66e
This diff is collapsed.
Click to expand it.
CHANGES.md
0 → 100644
View file @
54c75717
This diff is collapsed.
Click to expand it.
INSTALL
→
INSTALL
.md
View file @
54c75717
Installation instructions
Installation instructions
=========================
Installation from a source distribution (tarball)
...
...
@@ -7,14 +7,14 @@ Installation from a source distribution (tarball)
After unpacking, installation is done by
./configure
make
make install (as root)
./configure
make
make install (as root)
To install also the Ocaml library do
To install also the Ocaml library
,
do
make byte
make install-lib (as root)
make byte
make install-lib (as root)
Installation from the git repository
...
...
@@ -22,15 +22,16 @@ Installation from the git repository
First run
autoconf
automake --add-missing
autoconf
automake --add-missing
to build the ./configure file and install the helper scripts, then follow
instructions from the section above.
to build the
`
./configure
`
file and install the helper scripts, then follow
the
instructions from the section above.
Detailed instructions
---------------------
For detailed instructions and required dependencies, please see
the manual (doc/manual.pdf), Chapter 5 "Compilation, Installation".
the manual
[
doc/manual.pdf
](
http://why3.lri.fr/manual.pdf
)
, Chapter 5
[
Compilation, Installation
](
http://why3.lri.fr/doc/install.html
)
.
README
→
README
.md
View file @
54c75717
WHY 3
=====
Why3 is a platform for deductive program verification. It provides
a rich language for specification and programming, called WhyML, and
...
...
@@ -11,42 +13,43 @@ automated extraction mechanism. WhyML is also used as an intermediate
language for the verification of C, Java, or Ada programs.
PROJECT HOME
============
------------
http://why3.lri.fr
http://why3.lri.fr
/
https://g
forge
.inria.fr/
projects
/why3
https://g
itlab
.inria.fr/
why3
/why3
DOCUMENTATION
=============
-------------
The documentation (a tutorial and a reference manual) is in
the file doc/manual.pdf.
The documentation (a tutorial and a reference manual) is in the file
[
doc/manual.pdf
](
http://why3.lri.fr/manual.pdf
)
or online at
http://why3.lri.fr/doc/.
Various examples can be found in the subdirectories theories/
and examples/.
Various examples can be found in the subdirectories
[
theories/
](
theories
)
and
[
examples/
](
examples
)
.
Mailing list (Why3 Club):
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
Bug Tracking System:
https://g
forge
.inria.fr/
tracker/?atid=10293&group_id=2990&func=browse
https://g
itlab
.inria.fr/
why3/why3/issues
COPYRIGHT
=========
---------
This program is distributed under the GNU LGPL 2.1. See the enclosed
file LICENSE.
file
[
LICENSE
](
LICENSE
)
.
The files src/util/extmap.ml{i} are derived from the
sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file OCAML-LICENSE).
The files
[
src/util/extmap.ml{i}
](
src/util/extmap.mli
)
are derived from the
sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file
[
OCAML-LICENSE
](
OCAML-LICENSE
)
).
Icon sets for the graphical interface of Why3 are subject to specific
licenses, some of them may forbid commercial usage. These specific
licenses are detailed in files share/images/*/*.txt
licenses are detailed in files
[
share/images/
\
*/
\
*.txt
](
share/images
)
.
INSTALLATION
============
------------
See the file INSTALL.
See the file
[
INSTALL.
md
](
INSTALL.md
)
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment