Merge branch 'topic/fsf_merge_269/20250903' into 'fsf'

Synchronize with GNAT

Issue: eng/spark/spark2014#269

See merge request eng/spark/why3!96

Author: marc-adacore

.gitattributes

@@ -18,18 +18,13 @@ src/config.sh.in binary
 /.gitlab-ci.yml export-ignore
 /.mailmap export-ignore
 /check.sh export-ignore
-/DEVELOPER.readme export-ignore
-/ROADMAP export-ignore
-/TODO export-ignore
 
 /bench/encoding/ export-ignore
 /examples_in_progress/ export-ignore
 /misc/ export-ignore
 /opam/ export-ignore
 /tests/ export-ignore
 
-/src/trywhy3/Makefile export-ignore
-
 why3session.xml merge=ours
 why3shapes.gz merge=ours
 *.png diff=image

.github/workflows/workflow.yml

@@ -1,9 +1,9 @@
 name: Main workflow
 
-
 on:
   pull_request:
   push:
+  workflow_dispatch:
   schedule:
     # Prime the caches every Monday
     - cron: 0 1 * * MON
@@ -16,25 +16,27 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - macos-latest
-          - ubuntu-latest
-          - windows-latest
+          - macos-13
+          - macos-14
+          - ubuntu-22.04
+          - windows-2019
+          - ubuntu-22.04-arm
         ocaml-compiler:
-          - "4.11.2"
+          - "4.13.1"
 
     runs-on: ${{ matrix.os }}
 
     steps:
       - name: Checkout tree
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
-      - name: Set up Python 3.10
+      - name: Set up Python 3.12
         uses: actions/setup-python@v4
         with:
-          python-version: "3.10"
+          python-version: "3.12"
 
       - name: Set-up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
@@ -43,7 +45,7 @@ jobs:
           opam exec -- bash ./fsf_build.sh staging
 
       - name: Upload package
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: why3pack-${{matrix.os}}
           path: staging

.gitignore

@@ -47,12 +47,12 @@ why3.conf
 /src/jessie/.merlin
 /_build
 /public
-/bench/z3_nombqi/sessions
-/bench/alt_ergo_smt/sessions
 
 # /bench/
 /bench/extraction/test/test.*
 /bench/extraction/test/main.opt
+/bench/extraction/interface1/interface1.*
+/bench/extraction/interface1/main.opt
 /bench/programs/good/booleans/
 /bench/programs/good/exceptions/
 /bench/programs/good/for/
@@ -68,12 +68,21 @@ why3.conf
 /bench/check-ce/petiot2018/*.out
 /bench/check-ce/petiot2018/experiments/
 /bench/parsing/bad/*.out
+#/bench/alt_ergo_smt/sessions
+/bench/alt_ergo_smt2/sessions
+/bench_z3_computerdiv
+/bench/z3_nombqi/bench_z3_nombqi/sessions
+
+
 /examples/tests/*.out
+/bench/java/Makefile
+/bench/java/generated
 
 # /bin/
 /bin/why3.byte
 /bin/why3.opt
 /bin/why3
+/bin/why3.exe
 /bin/isabelle_client.opt
 /bin/isabelle_client.byte
 /bin/isabelle_client
@@ -92,6 +101,7 @@ why3.conf
 /doc/stdlibdoc/
 /doc/_build
 /doc/.doctrees/
+/doc/javaexamples/Makefile
 
 /public/
 
@@ -177,6 +187,7 @@ pvsbin/
 /src/util/mlmpfr_wrapper.ml
 /src/util/mysexplib.ml
 /src/util/ppx_debug_optim
+/src/util/ppx_debug_optim.exe
 
 # /src/session
 /src/session/xml.ml
@@ -217,6 +228,12 @@ pvsbin/
 /plugins/ada_terms/ada_lexer.ml
 /plugins/ada_terms/ada_parser.ml
 /plugins/ada_terms/ada_parser.mli
+/plugins/ada_terms/ada_parser.conflicts
+# /plugins/coma/
+/plugins/coma/coma_lexer.ml
+/plugins/coma/coma_parser.ml
+/plugins/coma/coma_parser.mli
+/plugins/coma/coma_parser.conflicts
 
 # /plugins/cfg/
 /plugins/cfg/cfg_lexer.ml
@@ -270,6 +287,7 @@ pvsbin/
 /examples/*/*/*.tex
 /examples/*/*/*/*.tex
 /examples/split_string/split_string.ml
+/examples/residual/residual.ml
 /examples/vstte10_max_sum/vstte10_max_sum.ml
 /examples/euler001/euler001.ml
 /examples/sudoku/sudoku.ml

.gitlab-ci.yml

@@ -6,7 +6,7 @@ stages:
   - deploy
 
 variables:
-  BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2023-11-13"
+  BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2025-05-20"
   SPHINX_IMAGE: "$CI_REGISTRY_IMAGE:ci-sphinx"
   GIT_CLEAN_FLAGS: "-ffdxq"
 
@@ -15,13 +15,13 @@ build-image:
   image: docker
   script:
     - docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
-    - if docker pull "$BUILD_IMAGE"; then echo "Image already exists!"; exit 1; fi
+    - if docker manifest inspect "$BUILD_IMAGE"; then echo "Image already exists!"; exit 0; fi
     - docker build --force-rm -t "$BUILD_IMAGE" - < misc/Dockerfile.build
     - docker push "$BUILD_IMAGE"
     - docker rmi "$BUILD_IMAGE"
-  only:
-    variables:
-      - $NEW_BUILD_IMAGE
+  rules:
+    - changes:
+        - misc/Dockerfile.build
   tags:
     - large
 

.mailmap

@@ -11,6 +11,7 @@ Paul Bonnot <[email protected]> <[email protected]>
 Paul Bonnot <[email protected]> <[email protected]>
 Martin Clochard <[email protected]> <martin@pc-stagiaire.(none)>
 Martin Clochard <[email protected]> <clochard@MC-MacBook.(none)>
+Loïc Correnson <[email protected]>
 Sylvain Dailler <[email protected]>
 Sylvain Dailler <[email protected]> <sdailler@[email protected]>
 Sylvain Dailler <[email protected]> <[email protected]>
@@ -19,12 +20,13 @@ Sylvain Dailler <[email protected]> <[email protected]>
 Xavier Denis <[email protected]> <[email protected]>
 Kate Deplaix <[email protected]> <[email protected]>
 Diego Diverio <[email protected]>
-Jean-Christophe Filliâtre <[email protected]> <[email protected]>
-Jean-Christophe Filliâtre <[email protected]> <[email protected]>
-Jean-Christophe Filliâtre <[email protected]> <jc@evariste.(none)>
-Jean-Christophe Filliâtre <[email protected]> <jc@gemini.(none)>
-Jean-Christophe Filliâtre <[email protected]> <filliatr@balrog.(none)>
-Jean-Christophe Filliâtre <[email protected]> <[email protected]>
+Jean-Christophe Filliâtre <[email protected]> <[email protected]>
+Jean-Christophe Filliâtre <[email protected]> <[email protected]>
+Jean-Christophe Filliâtre <[email protected]> <[email protected]>
+Jean-Christophe Filliâtre <[email protected]> <jc@evariste.(none)>
+Jean-Christophe Filliâtre <[email protected]> <jc@gemini.(none)>
+Jean-Christophe Filliâtre <[email protected]> <filliatr@balrog.(none)>
+Jean-Christophe Filliâtre <[email protected]> <[email protected]>
 Clément Fumex <[email protected]> <[email protected]>
 Quentin Garchery <[email protected]> <[email protected]>
 Léon Gondelman <[email protected]>
@@ -53,7 +55,10 @@ Thi-Minh-Tuyen Nguyen <[email protected]> <nguyenthiminhtuyen@minht
 Thi-Minh-Tuyen Nguyen <[email protected]> <[email protected]>
 Andrei Paskevich <[email protected]> <[email protected]>
 Andrei Paskevich <[email protected]> <[email protected]>
-Paul Patault <[email protected]>
+Paul Patault <[email protected]>
+Paul Patault <[email protected]> <[email protected]>
+Paul Patault <[email protected]> <[email protected]>
+Paul Patault <[email protected]> <[email protected]>
 Mário Pereira <[email protected]> <[email protected]>
 Mário Pereira <[email protected]> <[email protected]>
 Mário Pereira <[email protected]> <[email protected]>

.merlin.in

@@ -22,6 +22,7 @@ S plugins/transform
 S plugins/tptp
 S plugins/python
 S plugins/gnat_json
+S plugins/coma
 
 B src/util
 B src/core
@@ -47,6 +48,7 @@ B plugins/transform
 B plugins/tptp
 B plugins/python
 B plugins/gnat_json
+B plugins/coma
 B lib/why3
 
-PKG @RELIB@ unix num dynlink yojson @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@ @JSOFOCAMLPKG@ @MLMPFR@ @INFERPKG@ @SEXPLIB@
+PKG @RELIB@ unix zarith dynlink @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@ @JSOFOCAMLPKG@ @MLMPFR@ @INFERPKG@ @SEXPLIB@

CHANGES.md

@@ -1,15 +1,67 @@
 :x: marks a potential source of incompatibility
 
+Version 1.8.0, December 11, 2024
+--------------------------------
+
 Standard library
   * new library `ufloat`: unbounded floating-point numbers
+  * new library `coma`: standard library of the plugin Coma
+  * additional operators in library `fmap`
+  * added 16-bit integers in `mach/int`
+  * added a program equality in `bool`
+  * added meta annotations for "unused dependencies", which usually
+    improve proof automation but very rarely may lose some proofs :x:
+  * made most `(==)` operators trigger the `extensionality` transformation :x:
 
 Core
-  * extended notion of strategies: goal-oriented strategies
+  * records and range types now have some predefined symbol `foo'eq`
+    and some axiom `foo'inj` to express injectivity. See manual
+    Section "The WhyML Language Reference/Record Types".
+
+Transformations
+  * new transformation `extensionality` to help with equality proofs
 
 Plugins
-  * new goal-oriented strategy `forward_propagation` to automatically
-    propagate rounding errors in formulas involving unbounded
-    floats. See examples in `examples/numeric`
+  * new task-oriented strategy `forward_propagation` to automatically
+    propagate rounding errors
+  * new frontend plugin "Coma"
+
+Provers
+  * Alt-Ergo FPA requires Alt-Ergo >= 2.5.4
+  * drop support for versions of Coq < 8.16
+  * support for Coq 8.19 (released Jan 24, 2024)
+  * support for Z3 4.13 (released Mar 7, 2024)
+  * support for CVC5 1.2 (released Aug 8, 2024)
+  * support for Coq 8.20 (released Sep 11, 2024)
+  * support for Alt-Ergo 2.6 (released Sep 24, 2024)
+
+Tools
+  * `why3 prove`: dropped option `--json-model-values` :x:
+  * `why3 execute`: added option `--rac-memlimit`;
+    the `--rac-prover` option no longer supports specifying a time limit
+    and memory limit :x:
+  * `why3 pp`: the LaTeX output now shows algebraic types and logic definitions
+  * `why3 pp`: dropped option `--kind` :x:
+
+Extraction
+  * added support for Java, see Manual, Section "Executing WhyML Programs"
+  * improved extraction to C: floating-point numbers, global variables
+
+API
+  * changed how resource limits are specified :x
+  * renamed type `effect` to `effekt` for compatibility with OCaml 5.3 :x
+
+Miscellaneous
+  * dependency on OCaml library `num` was replaced by `zarith`
+
+Version 1.7.2, April 18, 2024
+-----------------------------
+
+Bug fixes
+  * restored the legacy shortcut for Alt-Ergo 2.5
+  * fixed various bugs in the lexer of `why3 doc`
+  * made prover detection more reliable when paths need escaping
+
 
 Version 1.7.1, January 20, 2024
 -------------------------------

CONTRIBUTING.md

@@ -16,22 +16,21 @@ Contributing to Why3
 
 Welcome, contributor, to the Why3 verification platform!
 
-If you wish to contribute, open an issue or otherwise interact with our [Gitlab](https://gitlab.inria.fr/why3/why3), you will need to have an INRIA account.
-External users can file bug reports using our [mailing list](mailto:why3-club@lists.gforge.inria.fr). We're sorry for the inconvenience.
+If you wish to contribute, open an issue or otherwise interact with our [Gitlab](https://gitlab.inria.fr/why3/why3), you will need to have an Inria account.
+External users can file bug reports using our [mailing list](mailto:why3-club@groupes.renater.fr). We are sorry for the inconvenience.
 
 # Building
 
-To build Why3 locally you will need a functional installation of OCaml (at least 4.08), `menhir`, `num` and `autoconf`. You can set up your developer build using the following commands:
+To build Why3 locally you will need a functional installation of OCaml (at
+least 4.09), `menhir`, `zarith`, and `autoconf`. You can set up your developer
+build using the following commands:
 
 ```
 autoconf
 ./configure --enable-local # stores the built binaries under ./bin
 make
 ```
 
-Note: there can be issues around Num, recall and document those.
-
-
 ## Building Documentation
 
 Building the Why3 documentation requires an installation of Sphinx, as well as the `sphinxcontrib-bibtex` package. If your package manager does not have up to date versions of these packages, or they otherwise fail to install, you can install them using `pip3` as follows:
@@ -52,12 +51,13 @@ To execute the Why3 tests run:
 
 ## Running specific tests
 
-You may run specific classes of tests through the `-only` flag, the full listing of classes can be obtained from `-help`.
+You may run specific classes of tests by specifying them on the command line.
+The full listing of classes can be obtained from `-help`.
 
-For example to run the 'good file' tests, use:
+For example to run the 'good file' and 'bad file' tests, use:
 
 ```
-./bench/bench -only goodfiles
+./bench/bench goodfiles badfiles
 ```
 
 ## Gitlab CI
@@ -91,6 +91,7 @@ While code review is not strictly enforced it is *highly* encouraged.
 ## Commits
 
 Every commit should:
+
 - Compile, and pass CI.
 - Be stripped of trailing whitespace.
 - Use appropriate indentation.
@@ -118,6 +119,7 @@ So, as mentioned above, an example of a `raw_model_parser`, for SMTv2
 solvers, is `Smtv2_model_parser.parse`, which makes use of another
 data type `Smtv2_model_defs.function_def`.  This specific
 `Smtv2_model_parser.parse` function proceeds in 2 main phases:
+
 - first transforms the textual output into an S-expression,
 - then the latter S-expression is transformed into a
   `Model_parser.model_element list`.
@@ -130,7 +132,7 @@ function that recovers the original Why3 name from the
 type `Printer.printer_args`.  The field `printing_info` is supposed to
 be modified in place by printers.
 
-# profiling
+# Profiling
 
 Profiling execution of Why3 can be performed out-of-the-box using
 under Linux using `perf`. A typical usage is
@@ -139,12 +141,18 @@ under Linux using `perf`. A typical usage is
 perf record --call-graph=dwarf -- why3 command <options> <arguments>
 perf report
 ```
-Note that perf may complain you don't have enough priviledges. A typical configuration change required is, for the session only, execute
+
+Note that `perf` may complain you don't have enough privileges. To change
+your configuration for the current session only, execute
+
 ```
 sysctl kernel.perf_event_paranoid=2
 ```
+
 or, to make this setting permanent, add the line
+
 ```
 kernel.perf_event_paranoid = 2
 ```
-to `sys/sysctl.conf`.
+
+to `/etc/sysctl.conf`.