Skip to content
Snippets Groups Projects
Commit f98ca871 authored by Aymeric Varasse's avatar Aymeric Varasse :innocent:
Browse files

Merge branch 'stable/1.0' into 'master' 

[release] Release 1.0

See merge request laiser/caisar!116
parents 19ec196f d9054057
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 47 additions and 30 deletions
.gitlab-ci.yml
+ 4
− 3
View file @ f98ca871
variables: variables:
CAISAR_VERSION: "0.2.0" CAISAR_VERSION: "1.0.0"
TAG: "1.0"
default: default:
interruptible: true interruptible: true
...@@ -76,7 +77,7 @@ make_public: ...@@ -76,7 +77,7 @@ make_public:
script: script:
- echo "$CAISAR_PUBLIC_SSH_PRIVATE_KEY" | base64 -d > ci/caisar-public/id_ed25519 - echo "$CAISAR_PUBLIC_SSH_PRIVATE_KEY" | base64 -d > ci/caisar-public/id_ed25519
- chmod 400 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: tags:
- docker - docker
rules: rules:
...@@ -95,7 +96,7 @@ make_public_confianceai: ...@@ -95,7 +96,7 @@ make_public_confianceai:
script: script:
- echo "$CAISAR_PUBLIC_SSH_PRIVATE_KEY" | base64 -d > ci/caisar-public/id_ed25519 - echo "$CAISAR_PUBLIC_SSH_PRIVATE_KEY" | base64 -d > ci/caisar-public/id_ed25519
- chmod 400 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: tags:
- docker - docker
rules: rules:
......
CHANGES.md
+ 24
− 8
View file @ f98ca871
## Unreleased # 1.0 (08-12-2023)
- Add command line option --goal (or, -g) to verify only the provided list of - [language] Extended WhyML for AI systems. It is now possible to model with
goals, either from all theories or from the specified ones. 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 - [doc] Update the documentation to cover the new interpretation language. Add
theories (ie, all their goals). contribution guide.
- Add command line option --define (or -D) to define the value of a declared - [cmdline] Add command line option `--goal` (or, `-g`) to verify only the
constant in any specification file to verify. 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) # 0.2.1 (19-09-2023)
...@@ -22,7 +36,9 @@ ...@@ -22,7 +36,9 @@
- [prover] Integration of the - [prover] Integration of the
[$\alpha-\beta-$CROWN](https://github.com/stanleybak/nnenum) prover. [$\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 - [prover] Add printer for VNN-LIB format for property specification as
supported by nnenum and $\alpha-\beta-$CROWN provers. supported by nnenum and $\alpha-\beta-$CROWN provers.
......
bin/abcrown.sh
+ 1
− 1
View file @ f98ca871
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
# # # #
# This file is part of CAISAR. # # This file is part of CAISAR. #
# # # #
# Copyright (C) 2022 # # Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies # # CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) # # alternatives) #
# # # #
......
bin/dummyversion.py
+ 1
− 1
View file @ f98ca871
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
# # # #
# This file is part of CAISAR. # # This file is part of CAISAR. #
# # # #
# Copyright (C) 2022 # # Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies # # CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) # # alternatives) #
# # # #
......
bin/nnenum.sh
+ 1
− 1
View file @ f98ca871
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
# # # #
# This file is part of CAISAR. # # This file is part of CAISAR. #
# # # #
# Copyright (C) 2022 # # Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies # # CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) # # alternatives) #
# # # #
......
caisar.opam
+ 3
− 3
View file @ f98ca871
# This file is generated by dune, edit dune-project instead # This file is generated by dune, edit dune-project instead
opam-version: "2.0" opam-version: "2.0"
version: "0.2" version: "1.0"
synopsis: synopsis:
"A platform for characterizing the safety and robustness of artificial intelligence based software" "A platform for characterizing the safety and robustness of artificial intelligence based software"
maintainer: [ maintainer: [
...@@ -19,7 +19,7 @@ depends: [ ...@@ -19,7 +19,7 @@ depends: [
"piqilib" {>= "0.6.14"} "piqilib" {>= "0.6.14"}
"zarith" {>= "1.7"} "zarith" {>= "1.7"}
"ocplib-endian" {>= "1.0"} "ocplib-endian" {>= "1.0"}
"base" {>= "v0.14.0"} "base" {>= "v0.15.1"}
"stdio" {>= "v0.14.0"} "stdio" {>= "v0.14.0"}
"cmdliner" {>= "1.1.1"} "cmdliner" {>= "1.1.1"}
"fmt" {>= "0.8.9"} "fmt" {>= "0.8.9"}
...@@ -27,7 +27,7 @@ depends: [ ...@@ -27,7 +27,7 @@ depends: [
"yojson" {>= "1.7.0"} "yojson" {>= "1.7.0"}
"menhirLib" {>= "20210310"} "menhirLib" {>= "20210310"}
"csv" {>= "2.4"} "csv" {>= "2.4"}
"why3" {>= "1.6.0"} "why3" {= "1.6.0"}
"re" {>= "1.10.4"} "re" {>= "1.10.4"}
"fpath" {>= "0.7.3"} "fpath" {>= "0.7.3"}
"yaml" {>= "3.1.0"} "yaml" {>= "3.1.0"}
......
doc/conf.py
+ 2
− 2
View file @ f98ca871
...@@ -29,9 +29,9 @@ author = 'The CAISAR Development Team' ...@@ -29,9 +29,9 @@ author = 'The CAISAR Development Team'
# built documents. # built documents.
# #
# The short X.Y version. # The short X.Y version.
version = '0.2' version = '1.0'
# The full version, including alpha/beta/rc tags. # The full version, including alpha/beta/rc tags.
release = '0.2' release = '1.0'
# -- General configuration --------------------------------------------------- # -- General configuration ---------------------------------------------------
......
doc/index.rst
+ 1
− 1
View file @ f98ca871
...@@ -18,7 +18,7 @@ The CAISAR Platform ...@@ -18,7 +18,7 @@ The CAISAR Platform
François Bobot, François Bobot,
Julien Girard Julien Girard
:Version: |version|, June 2023 :Version: |version|, December 2023
:Copyright: 2020--2023 CEA (Commissariat à l'énergie atomique et aux énergies alternatives) :Copyright: 2020--2023 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
.. _Confiance.ai: https://www.confiance.ai/ .. _Confiance.ai: https://www.confiance.ai/
......
docker/Dockerfile.template
+ 1
− 1
View file @ f98ca871
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
# # # #
# This file is part of CAISAR. # # This file is part of CAISAR. #
# # # #
# Copyright (C) 2022 # # Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies # # CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) # # alternatives) #
# # # #
......
docker/Makefile
+ 1
− 1
View file @ f98ca871
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
# # # #
# This file is part of CAISAR. # # This file is part of CAISAR. #
# # # #
# Copyright (C) 2022 # # Copyright (C) 2023 #
# CEA (Commissariat à l'énergie atomique et aux énergies # # CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) # # alternatives) #
# # # #
......
dune-project
+ 3
− 3
View file @ f98ca871
(lang dune 3.8) (lang dune 3.8)
(name caisar) (name caisar)
(version 0.2) (version 1.0)
(using dune_site 0.1) (using dune_site 0.1)
...@@ -27,7 +27,7 @@ ...@@ -27,7 +27,7 @@
(piqilib (>= 0.6.14)) (piqilib (>= 0.6.14))
(zarith (>= 1.7)) (zarith (>= 1.7))
(ocplib-endian (>= 1.0)) (ocplib-endian (>= 1.0))
(base (>= v0.14.0)) (base (>= v0.15.1))
(stdio (>= v0.14.0)) (stdio (>= v0.14.0))
(cmdliner (>= 1.1.1)) (cmdliner (>= 1.1.1))
(fmt (>= 0.8.9)) (fmt (>= 0.8.9))
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
(yojson (>= 1.7.0)) (yojson (>= 1.7.0))
(menhirLib (>= 20210310)) (menhirLib (>= 20210310))
(csv (>= 2.4)) (csv (>= 2.4))
(why3 (>= 1.6.0)) (why3 (= 1.6.0))
(re (>= 1.10.4)) (re (>= 1.10.4))
(fpath (>= 0.7.3)) (fpath (>= 0.7.3))
(yaml (>= 3.1.0)) (yaml (>= 3.1.0))
......
flake.nix
+ 1
− 1
View file @ f98ca871
...@@ -41,7 +41,7 @@ ...@@ -41,7 +41,7 @@
caisar = ocamlPkgs.buildDunePackage caisar = ocamlPkgs.buildDunePackage
{ {
pname = "caisar"; pname = "caisar";
version = "0.2.0"; version = "1.0.0";
duneVersion = "3"; duneVersion = "3";
minimalOCamlVersion = "4.13"; minimalOCamlVersion = "4.13";
installTargets = "all doc"; installTargets = "all doc";
......
src/main.ml
+ 1
− 1
View file @ f98ca871
...@@ -417,7 +417,7 @@ let default_info = ...@@ -417,7 +417,7 @@ let default_info =
`P "Submit bug reports to https://git.frama-c.com/pub/caisar/issues"; `P "Submit bug reports to https://git.frama-c.com/pub/caisar/issues";
] ]
in in
let version = "0.2" in let version = "1.0" in
let exits = Cmd.Exit.defaults in let exits = Cmd.Exit.defaults in
Cmd.info caisar ~version ~doc ~sdocs ~exits ~man Cmd.info caisar ~version ~doc ~sdocs ~exits ~man
......
stdlib/caisar.mlw
+ 1
− 1
View file @ f98ca871
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* *) (* *)
(* This file is part of CAISAR. *) (* This file is part of CAISAR. *)
(* *) (* *)
(* Copyright (C) 2022 *) (* Copyright (C) 2023 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *) (* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *) (* alternatives) *)
(* *) (* *)
......
stdlib/interpretation.mlw
+ 1
− 1
View file @ f98ca871
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* *) (* *)
(* This file is part of CAISAR. *) (* This file is part of CAISAR. *)
(* *) (* *)
(* Copyright (C) 2022 *) (* Copyright (C) 2023 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *) (* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *) (* alternatives) *)
(* *) (* *)
......
tests/help.t
+ 1
− 1
View file @ f98ca871
Test help Test help
$ caisar --version $ caisar --version
0.2 1.0
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment