diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 892fcdebe69fe70023b1501d7b2032eade92cdb6..a014512e6b9eda5595d36d92f4f02ce6d9349c65 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,17 +1,29 @@
-variables:
- CAISAR_VERSION: "2.0.0"
- TAG: "2.0"
-
default:
interruptible: true
tags: [ nix-v2 ]
stages:
+ - prepare
- build
- test
- doc
- make_public
+env:
+ stage: prepare
+ script:
+ - export VERSION=$(cat VERSION)
+ - export MAJOR=$(echo $VERSION | cut -d'.' -f1)
+ - export MINOR=$(echo $VERSION | cut -d'.' -f2)
+ - echo "VERSION=$VERSION" >> build.env
+ - echo "MAJOR=$MAJOR" >> build.env
+ - echo "MINOR=$MINOR" >> build.env
+ - echo "TAG=$MAJOR.$MINOR" >> build.env
+ - cat build.env
+ artifacts:
+ reports:
+ dotenv: build.env
+
build:
stage: build
script:
@@ -66,8 +78,8 @@ documentation:
- nix --extra-experimental-features "nix-command flakes" build
artifacts:
paths:
- - result/share/doc/ocaml4.14.1-caisar-${CAISAR_VERSION}/html
- - result/share/doc/ocaml4.14.1-caisar-${CAISAR_VERSION}/latex
+ - result/share/doc/ocaml4.14.1-caisar-${VERSION}/html
+ - result/share/doc/ocaml4.14.1-caisar-${VERSION}/latex
when: manual
################################################################################
diff --git a/Makefile b/Makefile
index 578e218cd687cd17ea346ec8da4cad7f9e87d6d3..12dc6ee2b7193ddff8367b704bf350455153d5a2 100644
--- a/Makefile
+++ b/Makefile
@@ -36,17 +36,24 @@ view-doc: doc
###################################
PROJECT_ID=1082
-TAG=$(shell dune-release tag -f --yes > /dev/null 2>&1 && git describe --tags --abbrev=0)
+VERSION=$(shell cat VERSION)
+MAJOR=$(shell echo $(VERSION) | cut -d'.' -f1)
+MINOR=$(shell echo $(VERSION) | cut -d'.' -f2)
+REV=$(shell echo $(VERSION) | cut -d'.' -f3)
+TAG=$(MAJOR).$(MINOR)
PKG="caisar-$(TAG).tbz"
PACKAGE_URL="https://git.frama-c.com/api/v4/projects/$(PROJECT_ID)/packages/generic/caisar/$(TAG)/$(PKG)"
DESCRIPTION="$(shell sed -n -e "p;n;:next;/^##/Q;p;n;b next" CHANGES.md | perl -pe 's/\n/\\n/')"
release:
+ @echo "Proceed to release CAISAR with release version $(TAG)? (y/n)?"
+ @read yesno; test "$$yesno" = y
+ @bash update_headers.sh
@echo -n $(DESCRIPTION)
@echo "Is the CHANGES.md correct for $(TAG) (y/n)?"
@read yesno; test "$$yesno" = y
dune-release tag $(TAG)
- dune-release distrib --skip-build --skip-lint
+ dune-release distrib --skip-build --skip-lint -t $(TAG) -V $(TAG)
curl --header "PRIVATE-TOKEN: $(GITLAB_TOKEN)" \
--upload-file _build/$(PKG) \
$(PACKAGE_URL)
diff --git a/VERSION b/VERSION
new file mode 100644
index 0000000000000000000000000000000000000000..227cea215648b1af34a87c9acf5b707fe02d2072
--- /dev/null
+++ b/VERSION
@@ -0,0 +1 @@
+2.0.0
diff --git a/configurator.ml b/configurator.ml
new file mode 100644
index 0000000000000000000000000000000000000000..389343b9219ae7a04ef2fd96044a626655594d3b
--- /dev/null
+++ b/configurator.ml
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module C = Configurator.V1
+
+module Version = struct
+ type t = {
+ major : string;
+ minor : string;
+ ext : string;
+ }
+
+ let get configurator =
+ let out_VERSION =
+ let out = C.Process.run configurator "cat" [ "VERSION" ] in
+ if out.exit_code <> 0 then C.die "Cannot read VERSION.";
+ out.stdout
+ in
+ let re_version = Str.regexp {|\([0-9]+\)\.\([0-9]\)\(.*\)|} in
+ let major, minor, ext =
+ if Str.string_match re_version out_VERSION 0
+ then
+ ( Str.matched_group 1 out_VERSION,
+ Str.matched_group 2 out_VERSION,
+ try Str.matched_group 3 out_VERSION with Not_found -> "" )
+ else C.die "Cannot read VERSION."
+ in
+ { major; minor; ext }
+
+ let pp_sed fmt version =
+ Format.fprintf fmt "s|@VERSION@|%s.%s%s|g" version.major version.minor
+ version.ext
+end
+
+let configure configurator =
+ let version = Version.get configurator in
+ let config_sed = open_out "config.sed" in
+ let fmt = Format.formatter_of_out_channel config_sed in
+ Format.fprintf fmt "@[%a@]@." Version.pp_sed version;
+ close_out config_sed
+
+let () = C.main ~name:"caisar_config" configure
diff --git a/doc/conf.py b/doc/conf.py
index e7f85be9bebfee6103e169fa5e229a6bfefbac7c..6365e24cede66a5bde6b73d8d257eb4c4bbfaa69 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -28,11 +28,11 @@ author = 'The CAISAR Development Team'
# |version| and |release|, also used in various other places throughout the
# built documents.
#
-# The short X.Y version.
-version = '2.0'
# The full version, including alpha/beta/rc tags.
-release = '2.0'
-
+with open('../VERSION') as f:
+ release = f.readline().rstrip()
+# The short X.Y version.
+version = '.'.join(release.split('.')[:2])
# -- General configuration ---------------------------------------------------
diff --git a/dune b/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7ca25ff9716a2a8b6d6a94300467dfc86dcecba0
--- /dev/null
+++ b/dune
@@ -0,0 +1,10 @@
+(executable
+ (name configurator)
+ (modules configurator)
+ (libraries dune-configurator str))
+
+(rule
+ (deps VERSION)
+ (targets config.sed)
+ (action
+ (run ./configurator.exe)))
diff --git a/flake.nix b/flake.nix
index 4709453778456b0e204a9c1a7923c78fca93b420..aa2f38f655778e25200bc7c9355baded7d4432a7 100644
--- a/flake.nix
+++ b/flake.nix
@@ -23,6 +23,9 @@
".ocamlformat"
"dune-project"
"Makefile"
+ "dune"
+ "configurator.ml"
+ "VERSION"
(nix-filter.lib.inDirectory "src")
(nix-filter.lib.inDirectory "examples")
(nix-filter.lib.inDirectory "lib")
@@ -66,6 +69,7 @@
re
fpath
dune-site
+ dune-configurator
fmt
logs
cmdliner
diff --git a/src/config.ml.in b/src/config.ml.in
new file mode 100644
index 0000000000000000000000000000000000000000..40a89a362bc41317304e4ce8331d1b9a1394184c
--- /dev/null
+++ b/src/config.ml.in
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let version = "@VERSION@"
diff --git a/src/config.mli b/src/config.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d297b06fbae0fda11d53fa01092c14db2948b861
--- /dev/null
+++ b/src/config.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+val version : string
diff --git a/src/dune b/src/dune
index 3afbd8c904c6c573cbaf7bb2378a4875921f17cb..1720e0cc43f86ab82444c4a0779ac06788ca8296 100644
--- a/src/dune
+++ b/src/dune
@@ -4,6 +4,7 @@
(flags
(:standard -open Caisar_logging))
(libraries
+ dune-configurator
menhirLib
yojson
cmdliner
@@ -39,3 +40,11 @@
(generate_sites_module
(module dirs)
(sites caisar))
+
+(rule
+ (targets config.ml)
+ (deps config.ml.in ../config.sed)
+ (action
+ (with-stdout-to
+ config.ml
+ (run sed -f ../config.sed config.ml.in))))
diff --git a/src/main.ml b/src/main.ml
index 9407ee17ec35b62ce1577de9983bc983b8f50762..abb4736bd114d10681f1f8597dcda0f011c7d063 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -433,7 +433,7 @@ let default_info =
`P "Submit bug reports to https://git.frama-c.com/pub/caisar/issues";
]
in
- let version = "1.0" in
+ let version = Config.version in
let exits = Cmd.Exit.defaults in
Cmd.info caisar ~version ~doc ~sdocs ~exits ~man
diff --git a/tests/bin/inspect_onnx.py b/tests/bin/inspect_onnx.py
index 1708b6b3aa3acfcf6704a5b22c712429be85ef6a..2018924a25f7be44de0e0ead974546be58167ba9 100644
--- a/tests/bin/inspect_onnx.py
+++ b/tests/bin/inspect_onnx.py
@@ -1,3 +1,5 @@
+#!/usr/bin/env python3
+
import onnx
from google.protobuf.json_format import MessageToDict
import os, sys
diff --git a/tests/dune b/tests/dune
index 8cdc54b64145997a1aabb149a57aeebd13e873b5..b32da34844252ecb61030cc200e0f601418c509b 100644
--- a/tests/dune
+++ b/tests/dune
@@ -21,7 +21,7 @@
../examples/mnist/csv/single_image.csv
../lib/xgboost/example/california.csv
../lib/xgboost/example/california.json
- )
+ ../VERSION)
(package caisar))
(cram
@@ -40,5 +40,6 @@
../examples/acasxu/nets/onnx/ACASXU_1_1.onnx
../examples/acasxu/nets/onnx/ACASXU_1_9.onnx
../lib/xgboost/example/california.csv
- ../lib/xgboost/example/california.json)
+ ../lib/xgboost/example/california.json
+ ../VERSION)
(package caisar))
diff --git a/tests/help.t b/tests/help.t
deleted file mode 100644
index 872cb9f9c24bae36d8479245e11e4e853ab0382a..0000000000000000000000000000000000000000
--- a/tests/help.t
+++ /dev/null
@@ -1,3 +0,0 @@
-Test help
- $ caisar --version
- 1.0
diff --git a/tests/version.t b/tests/version.t
new file mode 100644
index 0000000000000000000000000000000000000000..58efd93de36c17057c0b13ccaba2c44dc2765421
--- /dev/null
+++ b/tests/version.t
@@ -0,0 +1,2 @@
+Test version
+ $ caisar --version > CAISAR_VERSION && cmp CAISAR_VERSION ../VERSION
diff --git a/update_headers.sh b/update_headers.sh
old mode 100755
new mode 100644
index 9bd23b9513bd556ccb1ca65d5c7665e530fcd1c8..1ec154834ccf82d4e7d36443a3c627664c3edba2
--- a/update_headers.sh
+++ b/update_headers.sh
@@ -1,5 +1,14 @@
#!/usr/bin/env bash
-set -xe
+# set -xe
NEW_DATE=$(date "+%Y")
-OLD_DATE=$(date -d '1 year ago' "+%Y")
-find . \( -type d -name .git -prune \) \( -type d -name ._build -prune \) -o -type f -print0 | xargs -0 sed -i 's/(C) '${OLD_DATE}'/(C) '${NEW_DATE}'/g'
+OLD_DATE=$(sed "5q;d" src/main.ml | awk '{print $4}')
+
+if [ "$OLD_DATE" != "$NEW_DATE" ]; then
+ echo "Replacing $OLD_DATE by $NEW_DATE in headers."
+ find . -type d \( -name .git -o -name _build \) -prune -o -type f -print0 | xargs -0 sed -i 's/(C) '"${OLD_DATE}"'/(C) '"${NEW_DATE}"'/g'
+ echo "Done."
+ exit 0
+else
+ echo "Year $OLD_DATE in header src/main.ml is current date, no need to update the headers."
+ exit 0
+fi