[CI] Stage0 is currently the version of colibri2 installed

     So this one must be generated static

.gitlab-ci.yml

+stages:
+  - test
+  - deploy
+
+.build-matrix:
+  parallel:
+    # https://docs.gitlab.com/ee/ci/yaml/README.html#parallel-matrix-jobs
+    matrix:
+    # - OCAML_COMPILER: "4.00.1"
+    # - OCAML_COMPILER: "4.01.0"
+    # - OCAML_COMPILER: "4.02.1"
+    # - OCAML_COMPILER: "4.02.3"
+    # - OCAML_COMPILER: "4.03.0"
+    # - OCAML_COMPILER: "4.04.2"
+    # - OCAML_COMPILER: "4.05.0"
+    # - OCAML_COMPILER: "4.06.1"
+    # - OCAML_COMPILER: "4.07.1"
+    # - OCAML_COMPILER: "4.08.1"
+    # - OCAML_COMPILER: "4.09.1"
+    # - OCAML_COMPILER: "4.10.0"
+    - OCAML_COMPILER: "4.12.0"
+
 tests:
-  stage: build
-  image: ocaml/opam:ubuntu-20.04-ocaml-4.11
+  stage: test
+  extends: .build-matrix # defines OCAML_COMPILER
+  #ocaml/opam:debian-10-opam
+  image: ocaml/opam@sha256:c92cd07b0dc0ed07ec1a779545c676f475c12bc646a5e44e3abbf9363caba94b
+  cache:
+    # https://docs.gitlab.com/ee/ci/yaml/#cache
+    key: $OCAML_COMPILER-debian
+    # keep a distinct cache for each compiler version
+    paths:
+      - _opam
+  rules:
+    - when: always
   script:
+  - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . $OCAML_COMPILER; fi
   - eval `opam config env`
-  - opam pin --no-action .
-  - opam depext colibri2
-  - opam install --deps-only .
-  - opam depext --install why3 core jingoo yojson logs core # For generation not done in release mode
-  - opam depext --install ounit2 # For tests move to opam file?
+  - opam install depext --yes
+  - sudo apt-get update
+  - opam pin --no-action --yes .
+  - opam depext --yes colibri2 colibrics farith
+  - opam install . --deps-only --locked --with-test --with-doc --yes
+  - opam depext --yes --install why3 core jingoo yojson logs core # For generation not done in release mode
+  - opam depext --yes --install ounit2 # For tests move to opam file?
   - make
   - make test
   tags:
@@ -15,25 +50,59 @@ tests:
 
 # generate static binary
 generate-static:
-  stage: build
-  # ocaml/opam:alpine-ocaml-4.12
-  image: ocaml/opam@sha256:6cf1b7f60ae67190d1d85dbedabd6d845e3f0b21944386bdbe894fc28273f4e6
+  stage: test
+  extends: .build-matrix # defines OCAML_COMPILER
+  # ocaml/opam:alpine-3.13-opam
+  image: ocaml/opam@sha256:db94e740f73340f00113f09e5da81fe93183f241ac5974393cc51dfbdcc17b2d
+  cache:
+    # https://docs.gitlab.com/ee/ci/yaml/#cache
+    key: $OCAML_COMPILER-alpine
+    # keep a distinct cache for each compiler version
+    paths:
+      - _opam
   script:
+  - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . $OCAML_COMPILER; fi
   - eval `opam config env`
   - sed -e "s/; FOR STATIC//" -i src_colibri2/bin/dune
-  - opam pin --no-action .
-  - opam depext colibri2
-  - opam install --deps-only .
-  - opam depext --install why3 core jingoo yojson logs core # For generation not done in release mode
-  - opam depext --install ounit2 # For tests move to opam file?
+  - opam install depext --yes
+  - opam pin --no-action --yes .
+  - opam depext --yes colibri2 colibrics farith
+  - opam install . --dry-run --deps-only --locked --with-test --with-doc --yes | awk '/-> installed/{print $3}' | xargs opam depext --yes
+  - opam install . --deps-only --locked --with-test --with-doc --yes
+  - opam depext --yes --install why3 core jingoo yojson logs core # For generation not done in release mode
+  - opam depext --yes --install ounit2 # For tests move to opam file?
   - make
   - make test
-  - dune install --destdir=destdir
-  - ldd destdir/bin/colibri2
+  - dune install --destdir=destdir --prefix=/
+  - cp destdir/bin/colibri2 colibri2
   tags:
     - docker
-#  rules:
-#    - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
+  rules:
+    - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
+      when: manual
+      allow_failure: true
+    - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
+  artifacts:
+   expose_as: 'Colibri2 binary'
+   paths:
+    - colibri2
+
+starexec:
+  stage: deploy
+  # ocaml/opam:alpine-3.13-opam
+  image: ocaml/opam@sha256:db94e740f73340f00113f09e5da81fe93183f241ac5974393cc51dfbdcc17b2d
+  rules:
+    - when: manual
+  dependencies:
+    - generate-static
+  script:
+    - mkdir bin
+    - mv colibri2 bin/
+    - mv misc/starexec_run_default bin/
   artifacts:
+   expose_as: 'Starexec'
+   name: 'colibri2_starexec_$CI_COMMIT_SHORT_SHA'
    paths:
-    - destdir/bin/colibri2
+    - bin/
+  tags:
+    - docker

colibri2.opam

@@ -21,6 +21,7 @@ depends: [
   "cmdliner"
   "gen"
   "dune" {>= "2.8"}
+  "dune-build-info"
   "zarith"
   "ppx_deriving" {> "4.1.5"}
   "ppx_optcomp"

dune-project

@@ -44,6 +44,7 @@
            "cmdliner"
            "gen"
            "dune"
+           "dune-build-info"
            "zarith"
            ("ppx_deriving" (> "4.1.5"))
            "ppx_optcomp"

misc/starexec_run_default

+#!/bin/sh
+
+exec $(dirname $0)/colibri2 $1

src_colibri2/bin/dune

@@ -13,6 +13,7 @@
   dolmen.std
   dolmen_type
   dolmen_loop
+  dune-build-info
   ; colibrics
   ; <- Here insert new theories ! ->
   colibri2.solver
@@ -29,7 +30,9 @@
  (name colibri2_stage0)
  (public_name colibri2)
  (package colibri2)
- (flags -linkall)
+ (flags -linkall
+        ; FOR STATIC -ccopt -static
+ )
  (libraries colibri2_main colibri2.theories.LRA.stages.stage0)
  (modules colibri2_stage0))
 

src_colibri2/bin/main.ml

@@ -31,7 +31,10 @@ let () =
     `S Cmdliner.Manpage.s_authors;
     `P "Francois Bobot <francois.bobot@cea.fr>"
   ] in
-  let info = Cmdliner.Term.info ~man ~version:"0.1" "dolmen" in
+  let version = match Build_info.V1.version () with
+    | None -> "n/a"
+    | Some v -> Build_info.V1.Version.to_string v in
+  let info = Cmdliner.Term.info ~man ~version "Colibri2" in
   let theories = Colibri2_core.Egraph.default_theories () in
   let st,step_limit,show_steps = match Cmdliner.Term.eval (Options.state theories, info) with
     | `Version | `Help -> exit 0

src_colibri2/bin/options.ml

@@ -234,13 +234,13 @@ let state theories =
     let doc = "Stop the program after a time lapse of $(docv).
                  Accepts usual suffixes for durations : s,m,h,d.
                  Without suffix, default to a time in seconds." in
-    Arg.(value & opt c_time 300. & info ["t"; "time"] ~docv:"TIME" ~doc ~docs)
+    Arg.(value & opt c_time infinity & info ["t"; "time"] ~docv:"TIME" ~doc ~docs)
   in
   let size =
     let doc = "Stop the program if it tries and use more the $(docv) memory space. " ^
               "Accepts usual suffixes for sizes : k,M,G,T. " ^
               "Without suffix, default to a size in octet." in
-    Arg.(value & opt c_size 1_000_000_000. & info ["s"; "size"] ~docv:"SIZE" ~doc ~docs)
+    Arg.(value & opt c_size infinity & info ["s"; "size"] ~docv:"SIZE" ~doc ~docs)
   in
   let in_lang =
     let doc = Format.asprintf
@@ -257,7 +257,7 @@ let state theories =
   in
   let input =
     let doc = "Input problem file. If no file is specified,
-               dolmen will enter interactive mode and read on stdin." in
+               Colibri2 will enter interactive mode and read on stdin." in
     Arg.(value & pos 0 input_source_conv `Stdin & info [] ~docv:"FILE" ~doc)
   in
   let header_check =

src_colibri2/solver/input.ml

@@ -251,7 +251,7 @@ let handle_stmt ?(show_checksat_result=true) ?(show_steps=false) ?limit ~set_tru
     | `Get_option _
     | `Get_model
     | `Reset_assertions
-    | `Set_option _ -> invalid_arg "Unimplemented stmt"
+    | `Set_option _ -> invalid_arg (Format.asprintf "Unimplemented stmt: %a" Typer.print stmt)
     | `Push i -> push st.State.solve_state i
     | `Pop i -> pop st.State.solve_state i
     | `Decls _ -> (* nothing to do handled by dolmen *) ()