From 2448efa66ed232b3d38aa501fc2d4e545fd1ff8d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 18 Jan 2024 14:06:28 +0100 Subject: [PATCH] Update URL to the website. --- INSTALL.md | 4 ++-- Makefile.in | 2 +- README.md | 13 +++---------- doc/api.rst | 8 ++++---- doc/conf.py | 2 -- doc/foreword.rst | 2 +- doc/input_formats.rst | 4 ---- doc/install.rst | 2 +- doc/syntaxref.rst | 10 +++++----- opam/why3-coq.opam | 4 ++-- opam/why3-ide.opam | 4 ++-- opam/why3.opam | 4 ++-- src/ide/gconfig.ml | 4 ++-- src/ide/why3.html | 4 ++-- src/session/session_itp.ml | 2 +- src/trywhy3/help_micro-C.html | 2 +- src/trywhy3/help_python.html | 2 +- src/trywhy3/help_whyml.html | 2 +- src/trywhy3/trywhy3.html | 2 +- 19 files changed, 32 insertions(+), 45 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 5a40d89a0..2e5c5f856 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -32,5 +32,5 @@ Detailed instructions --------------------- For detailed instructions and required dependencies, please see -the manual [doc/latex/manual.pdf](http://why3.lri.fr/manual.pdf), Chapter 5 -[Compilation, Installation](http://why3.lri.fr/doc/install.html). +the manual: +[Compilation, Installation](https://www.why3.org/doc/install.html). diff --git a/Makefile.in b/Makefile.in index a85f2660e..997a2cc36 100644 --- a/Makefile.in +++ b/Makefile.in @@ -800,7 +800,7 @@ gallery-subs: echo "exporting examples/$$d"; \ mkdir -p $(GALLERYDIR)/$$d; \ cd examples/$$d; \ - WHY3CONFIG="" ../../bin/why3.@OCAMLBEST@ doc --no-stdlib --no-load-default-plugins -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ --warn-off=unused_variable *.mlw -o $(GALLERYDIR)/$$d; \ + WHY3CONFIG="" ../../bin/why3.@OCAMLBEST@ doc --no-stdlib --no-load-default-plugins -L ../../stdlib -L . --stdlib-url https://www.why3.org/stdlib/ --warn-off=unused_variable *.mlw -o $(GALLERYDIR)/$$d; \ cd ..; \ rm -f $(GALLERYDIR)/$$d/$$d.zip; \ git archive --format=zip -o $(GALLERYDIR)/$$d/$$d.zip HEAD $$d; \ diff --git a/README.md b/README.md index 22a083bc2..e888e7599 100644 --- a/README.md +++ b/README.md @@ -15,26 +15,19 @@ language for the verification of C, Java, or Ada programs. PROJECT HOME ------------ -http://why3.lri.fr/ +https://www.why3.org/ https://gitlab.inria.fr/why3/why3 DOCUMENTATION ------------- -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/. +The documentation (a tutorial and a reference manual) is +available [online](https://www.why3.org/doc/). Various examples can be found in the subdirectories [stdlib/](stdlib) and [examples/](examples). -Mailing list (Why3 Club): - http://lists.gforge.inria.fr/mailman/listinfo/why3-club - -Bug Tracking System: - https://gitlab.inria.fr/why3/why3/issues - COPYRIGHT --------- diff --git a/doc/api.rst b/doc/api.rst index d42ff509b..496baf60c 100644 --- a/doc/api.rst +++ b/doc/api.rst @@ -7,7 +7,7 @@ This chapter is a tutorial for the users who want to link their own OCaml code with the Why3 library. We progressively introduce the way one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on tasks. The -complete documentation for API calls is given at URL |apiurl|. +complete documentation for API calls is given at URL https://www.why3.org/api/. We assume the reader has a fair knowledge of the OCaml language. Notice that the Why3 library must be installed, see :numref:`sec.installlib`. @@ -519,8 +519,8 @@ trees, and finally the OCaml module ``Ptree_helpers`` which contains helpers for building those trees and a more concise and friendly manner than the low-level constructors. The latter two OCaml modules are documented in the online API documentation, respectively for -`Ptree `_ and -`Ptree_helpers `_. +`Ptree `_ and +`Ptree_helpers `_. .. literalinclude:: ../examples/use_api/mlw_tree.ml :language: ocaml @@ -893,7 +893,7 @@ The structure of JSON output is described in :numref:`sec.jsonce`. In the code above, the variable ``m`` has type ``Model_parser.model``. This type is described in -`Model_parser `_. +`Model_parser `_. Checking counterexamples diff --git a/doc/conf.py b/doc/conf.py index 7b0f84e94..07ec0bcfb 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -174,6 +174,4 @@ numfig = True rst_prolog = ''' .. |whypath| replace:: ``why3-{v}`` - -.. |apiurl| replace:: http://why3.lri.fr/api-{v}/ '''.format(v=version) diff --git a/doc/foreword.rst b/doc/foreword.rst index bb4b32265..edba2bab8 100644 --- a/doc/foreword.rst +++ b/doc/foreword.rst @@ -23,7 +23,7 @@ formalizations or to add support for a new external prover if wanted. Availability ~~~~~~~~~~~~ -Why3 project page is http://why3.lri.fr/. The last distribution is +Why3 project page is https://www.why3.org/. The latest release is available there, in source format, together with this documentation and several examples. diff --git a/doc/input_formats.rst b/doc/input_formats.rst index ee2da9484..975d50ac5 100644 --- a/doc/input_formats.rst +++ b/doc/input_formats.rst @@ -16,10 +16,6 @@ Any Why3 tool (:why3:tool:`why3 prove`, :why3:tool:`why3 ide`, etc.) can be passed a file with a suffix :file:`.c`, :file:`.py` or :file:`.mlcfg`, which triggers the corresponding input format. -The input formats for C and Python can also be used in on-line -versions of Why3, at http://why3.lri.fr/micro-C/ and -http://why3.lri.fr/python/, respectively. - .. index:: micro-C .. _format.micro-C: diff --git a/doc/install.rst b/doc/install.rst index 59259c84f..c82a94eed 100644 --- a/doc/install.rst +++ b/doc/install.rst @@ -216,7 +216,7 @@ installed separately, and then Why3 needs to be configured to use them. There is no need to install automatic provers, e.g., SMT solvers, before compiling and installing Why3. For installation of external provers, please refer to the specific section about provers from -http://why3.lri.fr/. (If you have installed Why3 via Opam, note that you can +https://www.why3.org/. (If you have installed Why3 via Opam, note that you can install the SMT solver Alt-Ergo via Opam as well.) Once you have installed a prover, or a new version of a prover, you have diff --git a/doc/syntaxref.rst b/doc/syntaxref.rst index cacbc93a0..cb58f8ff8 100644 --- a/doc/syntaxref.rst +++ b/doc/syntaxref.rst @@ -1240,7 +1240,7 @@ argument of type ``int`` and thus can be used to build values such as type option 'a = None | Some 'a (This type is already part of Why3 standard library, in module -`option.Option `_.) +`option.Option `_.) A data type can be recursive. The archetypal example is the type of polymorphic lists: @@ -1250,7 +1250,7 @@ polymorphic lists: type list 'a = Nil | Cons 'a (list 'a) (This type is already part of Why3 standard library, in module -`list.List `_.) +`list.List `_.) Mutually recursive type definitions are supported. @@ -1774,7 +1774,7 @@ The Why3 Standard Library The Why3 standard library provides general-purpose modules, to be used in logic and/or programs. It can be browsed on-line at -http://why3.lri.fr/stdlib/. Each file contains one or several modules. +https://www.why3.org/stdlib/. Each file contains one or several modules. To ``use`` or ``clone`` a module ``M`` from file :file:`file.mlw`, use the syntax ``file.M``, since :file:`file.mlw` is available in Why3’s default load path. For instance, the module of integers and the module of arrays @@ -1823,7 +1823,7 @@ proper pre-conditions, and with the usual infix syntax ``x / y`` and ``x % y``. The detailed documentation of the library is available on-line at -http://why3.lri.fr/stdlib/int.html +https://www.why3.org/stdlib/int.html. Library ``array``: array data structure @@ -1844,4 +1844,4 @@ where ``l`` is the desired length and ``v`` is the initial value of each cell. The detailed documentation of the library is available on-line at -http://why3.lri.fr/stdlib/array.html +https://www.why3.org/stdlib/array.html. diff --git a/opam/why3-coq.opam b/opam/why3-coq.opam index 7a624826f..9e9cd556e 100644 --- a/opam/why3-coq.opam +++ b/opam/why3-coq.opam @@ -8,9 +8,9 @@ authors: [ "Andrei Paskevich" ] -homepage: "http://why3.lri.fr/" +homepage: "https://www.why3.org/" license: "LGPL-2.1-only" -doc: "http://why3.lri.fr/doc/" +doc: "https://www.why3.org/doc/" bug-reports: "https://gitlab.inria.fr/why3/why3/issues" dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" diff --git a/opam/why3-ide.opam b/opam/why3-ide.opam index 9d91ab9b4..49290c0c8 100644 --- a/opam/why3-ide.opam +++ b/opam/why3-ide.opam @@ -8,9 +8,9 @@ authors: [ "Andrei Paskevich" ] -homepage: "http://why3.lri.fr/" +homepage: "https://www.why3.org/" license: "LGPL-2.1-only" -doc: "http://why3.lri.fr/doc/" +doc: "https://www.why3.org/doc/" bug-reports: "https://gitlab.inria.fr/why3/why3/issues" dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" diff --git a/opam/why3.opam b/opam/why3.opam index 6979435c7..ee8f01ebd 100644 --- a/opam/why3.opam +++ b/opam/why3.opam @@ -8,9 +8,9 @@ authors: [ "Andrei Paskevich" ] -homepage: "http://why3.lri.fr/" +homepage: "https://www.why3.org/" license: "LGPL-2.1-only" -doc: "http://why3.lri.fr/doc/" +doc: "https://www.why3.org/doc/" bug-reports: "https://gitlab.inria.fr/why3/why3/issues" dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 8025440e1..0f5998eb4 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -684,8 +684,8 @@ let show_about_window ~parent () = ] ~copyright:"Copyright 2010-2023 Inria, CNRS, Paris-Saclay University" ~license:("See file " ^ Filename.concat Config.datadir "LICENSE") - ~website:"http://why3.lri.fr/" - ~website_label:"http://why3.lri.fr/" + ~website:"https://www.why3.org/" + ~website_label:"https://www.why3.org/" ~version:Config.version ~icon:!why_icon ~logo:!why_icon diff --git a/src/ide/why3.html b/src/ide/why3.html index 14fcd70ec..bc8de5998 100644 --- a/src/ide/why3.html +++ b/src/ide/why3.html @@ -211,8 +211,8 @@
About TryWhy3 -

TryWhy3 is a Javascript based version of - the Why3 +

TryWhy3 is a Javascript-based version of + the Why3 Verification Platform

© 2010-2017, Inria - CNRS - Paris-Sud University
This software is distributed under the terms of the GNU Lesser diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index 542d14d7a..54c2be55f 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -2161,7 +2161,7 @@ let save fname shfname session = let chsh = Compress.Compress_z.open_out shfname in let fmt = formatter_of_out_channel ch in fprintf fmt "@\n"; - fprintf fmt "@\n"; + fprintf fmt "@\n"; fprintf fmt "@[" Termcode.pp_sum_shape_version session.shapes.shape_version; let prover_ids = session.session_prover_ids in diff --git a/src/trywhy3/help_micro-C.html b/src/trywhy3/help_micro-C.html index 8469a893f..971ec3f08 100644 --- a/src/trywhy3/help_micro-C.html +++ b/src/trywhy3/help_micro-C.html @@ -11,7 +11,7 @@ This version of Why3 is intended for teaching purposes. Its input format is a tiny subset of C, called "micro-C", - and described here. + and described here.

diff --git a/src/trywhy3/help_python.html b/src/trywhy3/help_python.html index 8667cbf8a..dee54f05b 100644 --- a/src/trywhy3/help_python.html +++ b/src/trywhy3/help_python.html @@ -11,7 +11,7 @@ This version of Why3 is intended for teaching purposes. Its input format is a tiny subset of Python, called "micro-Python" - and described here. + and described here.

diff --git a/src/trywhy3/help_whyml.html b/src/trywhy3/help_whyml.html index e4c66ed51..d61ee076a 100644 --- a/src/trywhy3/help_whyml.html +++ b/src/trywhy3/help_whyml.html @@ -13,7 +13,7 @@

The WhyML language is - described in the Why3 + described in the Why3 manual.

Verifying a program

diff --git a/src/trywhy3/trywhy3.html b/src/trywhy3/trywhy3.html index 9b0395aff..51aac0506 100644 --- a/src/trywhy3/trywhy3.html +++ b/src/trywhy3/trywhy3.html @@ -190,7 +190,7 @@
About TryWhy3

TryWhy3 is a Javascript based version of - the Why3 + the Why3 Verification Platform

© 2010-2023, Inria - CNRS - Paris-Saclay University
This software is distributed under the terms of the GNU Lesser