diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7d588a88fab1b3438acac477772223afe4ef27c8..d1504f8db17f344ff75d62fc73c613db0719c6d9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,5 +1,6 @@
variables:
- CAISAR_VERSION: "0.2.0"
+ CAISAR_VERSION: "1.0.0"
+ TAG: "1.0"
default:
interruptible: true
@@ -76,7 +77,7 @@ make_public:
script:
- echo "$CAISAR_PUBLIC_SSH_PRIVATE_KEY" | base64 -d > ci/caisar-public/id_ed25519
- chmod 400 ci/caisar-public/id_ed25519
- - GIT_SSH=$PWD/ci/caisar-public/ssh.sh git push git@git.frama-c.com:pub/caisar.git origin/master:refs/heads/master
+ - GIT_SSH=$PWD/ci/caisar-public/ssh.sh git push --atomic git@git.frama-c.com:pub/caisar.git origin/master:refs/heads/master $TAG
tags:
- docker
rules:
@@ -95,7 +96,7 @@ make_public_confianceai:
script:
- echo "$CAISAR_PUBLIC_SSH_PRIVATE_KEY" | base64 -d > ci/caisar-public/id_ed25519
- chmod 400 ci/caisar-public/id_ed25519
- - GIT_SSH=$PWD/ci/caisar-public/ssh.sh git push git@git.irt-systemx.fr:confianceai/ec_1/fa09_caisar.git origin/master:refs/heads/master
+ - GIT_SSH=$PWD/ci/caisar-public/ssh.sh git push --atomic git@git.irt-systemx.fr:confianceai/ec_1/fa09_caisar.git origin/master:refs/heads/master $TAG
tags:
- docker
rules:
diff --git a/CHANGES.md b/CHANGES.md
index a480eaf144f66dcd1d3d83706978a6427a519bd8..a96840ea3b060fa3d937882675c867af83cd12c1 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,13 +1,27 @@
- ## Unreleased
+# 1.0 (08-12-2023)
-- Add command line option --goal (or, -g) to verify only the provided list of
- goals, either from all theories or from the specified ones.
+- [language] Extended WhyML for AI systems. It is now possible to model with
+ CAISAR computations on vectors, datasets and the application of machine
+ learning programs. Added an interpretation engine that allow direct evaluation
+ on some predicates and functions related to those extensions.
-- Add command line option --theory (or, -T) to verify only the provided list of
- theories (ie, all their goals).
+- [doc] Update the documentation to cover the new interpretation language. Add
+ contribution guide.
-- Add command line option --define (or -D) to define the value of a declared
- constant in any specification file to verify.
+- [cmdline] Add command line option `--goal` (or, `-g`) to verify only the
+ provided list of goals, either from all theories or from the specified ones.
+
+- [cmdline] Add command line option `--theory` (or, `-T`) to verify only the
+ provided list of theories (ie, all their goals).
+
+- [cmdline] Add command line option `--define` (or `-D`) to define the value of
+ a declared constant in any specification file to verify.
+
+- [build] Make CAISAR available as a Nix Flake.
+
+- [prover] Better integration of the AIMOS metamorphic testing prover.
+
+- [docker] Add the $\alpha-\beta-$CROWN prover to the docker image.
# 0.2.1 (19-09-2023)
@@ -22,7 +36,9 @@
- [prover] Integration of the
[$\alpha-\beta-$CROWN](https://github.com/stanleybak/nnenum) prover.
-- [prover] Integration of the AIMOS metamorphic testing prover.
+- [prover] Integration of the
+ [AIMOS](https://dx.doi.org/10.1007/978-3-031-40953-0_27) metamorphic testing
+ prover.
- [prover] Add printer for VNN-LIB format for property specification as
supported by nnenum and $\alpha-\beta-$CROWN provers.
diff --git a/bin/abcrown.sh b/bin/abcrown.sh
index 93a95c6dd38a65ea07daa5ad150c3beaa2d8e14c..b9a3024cf4dae50e8d8f0f099b529424c7e48d0b 100755
--- a/bin/abcrown.sh
+++ b/bin/abcrown.sh
@@ -3,7 +3,7 @@
# #
# This file is part of CAISAR. #
# #
-# Copyright (C) 2022 #
+# Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/bin/dummyversion.py b/bin/dummyversion.py
index 55ff02356c894789ca8e200c139da542da3a2a91..1358d11d6a5bfa7f79b2e5eaa44bf5557029bc94 100755
--- a/bin/dummyversion.py
+++ b/bin/dummyversion.py
@@ -3,7 +3,7 @@
# #
# This file is part of CAISAR. #
# #
-# Copyright (C) 2022 #
+# Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/bin/nnenum.sh b/bin/nnenum.sh
index 907dfda8b2d87f17eb8494bbe09f96889bfccd94..fc41079d54d7aa3dba8acdabc89a759699b26d56 100755
--- a/bin/nnenum.sh
+++ b/bin/nnenum.sh
@@ -3,7 +3,7 @@
# #
# This file is part of CAISAR. #
# #
-# Copyright (C) 2022 #
+# Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/caisar.opam b/caisar.opam
index 98018a4e6b8c8c79e256f3123d057dfef5179cb9..9a8115d8bf1b763f900a28deb4f32ff17eb427e0 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -1,6 +1,6 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
-version: "0.2"
+version: "1.0"
synopsis:
"A platform for characterizing the safety and robustness of artificial intelligence based software"
maintainer: [
@@ -19,7 +19,7 @@ depends: [
"piqilib" {>= "0.6.14"}
"zarith" {>= "1.7"}
"ocplib-endian" {>= "1.0"}
- "base" {>= "v0.14.0"}
+ "base" {>= "v0.15.1"}
"stdio" {>= "v0.14.0"}
"cmdliner" {>= "1.1.1"}
"fmt" {>= "0.8.9"}
@@ -27,7 +27,7 @@ depends: [
"yojson" {>= "1.7.0"}
"menhirLib" {>= "20210310"}
"csv" {>= "2.4"}
- "why3" {>= "1.6.0"}
+ "why3" {= "1.6.0"}
"re" {>= "1.10.4"}
"fpath" {>= "0.7.3"}
"yaml" {>= "3.1.0"}
diff --git a/doc/conf.py b/doc/conf.py
index 22dc7b8d54ef97787d12dbbb8e61bb3e87219e7f..2e45e7bca5698da02cd44e90464083b17412fe62 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -29,9 +29,9 @@ author = 'The CAISAR Development Team'
# built documents.
#
# The short X.Y version.
-version = '0.2'
+version = '1.0'
# The full version, including alpha/beta/rc tags.
-release = '0.2'
+release = '1.0'
# -- General configuration ---------------------------------------------------
diff --git a/doc/index.rst b/doc/index.rst
index 694f329274fa453c6fa500fdf42041a85257dcf1..6ccf4ea49a075e96962f7bffede89ecbb5ac1836 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -18,7 +18,7 @@ The CAISAR Platform
François Bobot,
Julien Girard
-:Version: |version|, June 2023
+:Version: |version|, December 2023
:Copyright: 2020--2023 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
.. _Confiance.ai: https://www.confiance.ai/
diff --git a/docker/Dockerfile.template b/docker/Dockerfile.template
index c19e786ec8bc26ee47f6da5e9fe8133476c5ac45..d19c0718d008c479207ae1797ad42f76a9b9a2eb 100644
--- a/docker/Dockerfile.template
+++ b/docker/Dockerfile.template
@@ -2,7 +2,7 @@
# #
# This file is part of CAISAR. #
# #
-# Copyright (C) 2022 #
+# Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/docker/Makefile b/docker/Makefile
index 900ed3f12520f797d82af2b493ee898942f4ad3d..f1dea8e450b60092c6859edf18eaedee6d15beb6 100644
--- a/docker/Makefile
+++ b/docker/Makefile
@@ -2,7 +2,7 @@
# #
# This file is part of CAISAR. #
# #
-# Copyright (C) 2022 #
+# Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/dune-project b/dune-project
index 1c4f8609b1ab9c7f4e20e4c95fc230f9896b9a42..bcb9f6e06396a4c3a2ac4f39cec65ea5851dc970 100644
--- a/dune-project
+++ b/dune-project
@@ -1,6 +1,6 @@
(lang dune 3.8)
(name caisar)
-(version 0.2)
+(version 1.0)
(using dune_site 0.1)
@@ -27,7 +27,7 @@
(piqilib (>= 0.6.14))
(zarith (>= 1.7))
(ocplib-endian (>= 1.0))
- (base (>= v0.14.0))
+ (base (>= v0.15.1))
(stdio (>= v0.14.0))
(cmdliner (>= 1.1.1))
(fmt (>= 0.8.9))
@@ -35,7 +35,7 @@
(yojson (>= 1.7.0))
(menhirLib (>= 20210310))
(csv (>= 2.4))
- (why3 (>= 1.6.0))
+ (why3 (= 1.6.0))
(re (>= 1.10.4))
(fpath (>= 0.7.3))
(yaml (>= 3.1.0))
diff --git a/flake.nix b/flake.nix
index b21c53897806032caf5a80af1bcc029ff9234a80..c0e7b900984a9f29753d0e00135513bc5ce19c45 100644
--- a/flake.nix
+++ b/flake.nix
@@ -41,7 +41,7 @@
caisar = ocamlPkgs.buildDunePackage
{
pname = "caisar";
- version = "0.2.0";
+ version = "1.0.0";
duneVersion = "3";
minimalOCamlVersion = "4.13";
installTargets = "all doc";
diff --git a/src/main.ml b/src/main.ml
index 25137c1cb385975d0fb21cc4757e8c7426f26694..73bcadc8b19d3aff28e05b2a3fed4817f0a3f19f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -417,7 +417,7 @@ let default_info =
`P "Submit bug reports to https://git.frama-c.com/pub/caisar/issues";
]
in
- let version = "0.2" in
+ let version = "1.0" in
let exits = Cmd.Exit.defaults in
Cmd.info caisar ~version ~doc ~sdocs ~exits ~man
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 31d5dbc82d8f0d2f74e1911c7d934bbcd44a0cc4..3ee65d62b90286f4ba18d4981f7e1912e1226224 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -2,7 +2,7 @@
(* *)
(* This file is part of CAISAR. *)
(* *)
-(* Copyright (C) 2022 *)
+(* Copyright (C) 2023 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/stdlib/interpretation.mlw b/stdlib/interpretation.mlw
index 68a0d7073228d708da194a9710e25d3ffc1548d8..031993d7272b4b2cccfa584985d97ac17a33cac8 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/interpretation.mlw
@@ -2,7 +2,7 @@
(* *)
(* This file is part of CAISAR. *)
(* *)
-(* Copyright (C) 2022 *)
+(* Copyright (C) 2023 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/tests/help.t b/tests/help.t
index 4dfb127e17f8c96d067602e54c906ed5901fe04a..872cb9f9c24bae36d8479245e11e4e853ab0382a 100644
--- a/tests/help.t
+++ b/tests/help.t
@@ -1,3 +1,3 @@
Test help
$ caisar --version
- 0.2
+ 1.0