Bump dolmen version

colibri2.opam

@@ -15,9 +15,9 @@ bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
 depends: [
   "colibrilib" {= version}
   "containers" {>= "3.6.1"}
-  "dolmen" {>= "0.7"}
-  "dolmen_type" {>= "0.7"}
-  "dolmen_loop" {>= "0.7"}
+  "dolmen" {>= "0.8"}
+  "dolmen_type" {>= "0.8"}
+  "dolmen_loop" {>= "0.8"}
   "cmdliner" {>= "1.1.1"}
   "base" {>= "v0.14.2"}
   "gen" {>= "1.0"}
@@ -36,7 +36,7 @@ depends: [
   "farith"
   "ounit2" {>= "2.2.4" & with-test}
   "ocaml" {>= "4.12"}
-  "ocplib-simplex" {>= "0.4"}
+  "ocplib-simplex" {= "0.4"}
   "odoc" {with-doc}
 ]
 build: [

colibri2/bin/dune

@@ -44,26 +44,6 @@
    %{target}
    (run true))))
 
-; Colibri2 stage1
-
-(executable
- (name colibri2_stage1)
- ; (public_name colibri2)
- ; (package colibri2)
- (flags
-  -linkall
-  ; FOR STATIC -ccopt -static
-  )
- (libraries colibri2_main colibri2.theories.LRA.stages.stage1)
- (modules colibri2_stage1))
-
-(rule
- (target colibri2_stage1.ml)
- (action
-  (with-outputs-to
-   %{target}
-   (run true))))
-
 ; Colibri2 stage2
 
 (executable

colibrics.opam

@@ -9,9 +9,9 @@ homepage: "https://colibri.frama-c.com"
 bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
 depends: [
   "ppx_deriving_yojson" {>= "3.6.1"}
-  "dolmen" {>= "0.7"}
-  "dolmen_type" {>= "0.7"}
-  "dolmen_loop" {>= "0.7"}
+  "dolmen" {>= "0.8"}
+  "dolmen_type" {>= "0.8"}
+  "dolmen_loop" {>= "0.8"}
   "dune" {>= "3.0"}
   "zarith" {>= "1.12"}
   "cmdliner" {>= "1.1.1"}

colibrics/lib/dune

@@ -55,53 +55,53 @@
 
 ;; Doesn't extract anything currently
 
-(rule
- (deps
-  cp.mlw
-  all.mlw
-  utils/tagtbl.mlw
-  utils/extstd.mlw
-  cp_c.drv
-  constraints/simple.mlw)
- (targets
-  int63.c
-  bool.c
-  impl0.c
-  var.c
-  var0.c
-  type.c
-  domb.c
-  domi.c
-  simple.c
-  constrainthelpers.c
-  all.c
-  api.c
-  apidefensive.c)
- (action
-  (run
-   why3
-   extract
-   -L
-   .
-   -D
-   c
-   -D
-   cp_c.drv
-   -o
-   .
-   --modular
-   utils.extstd.Int63
-   utils.extstd.Bool
-   cp.Impl0
-   cp.Var
-   cp.Var0
-   cp.Type
-   cp.DomI
-   cp.DomB
-   constraints.simple.Simple
-   cp.ConstraintHelpers
-   all.All
-   all.API
-   all.APIDefensive)))
+; (rule
+;  (deps
+;   cp.mlw
+;   all.mlw
+;   utils/tagtbl.mlw
+;   utils/extstd.mlw
+;   cp_c.drv
+;   constraints/simple.mlw)
+;  (targets
+;   int63.c
+;   bool.c
+;   impl0.c
+;   var.c
+;   var0.c
+;   type.c
+;   domb.c
+;   domi.c
+;   simple.c
+;   constrainthelpers.c
+;   all.c
+;   api.c
+;   apidefensive.c)
+;  (action
+;   (run
+;    why3
+;    extract
+;    -L
+;    .
+;    -D
+;    c
+;    -D
+;    cp_c.drv
+;    -o
+;    .
+;    --modular
+;    utils.extstd.Int63
+;    utils.extstd.Bool
+;    cp.Impl0
+;    cp.Var
+;    cp.Var0
+;    cp.Type
+;    cp.DomI
+;    cp.DomB
+;    constraints.simple.Simple
+;    cp.ConstraintHelpers
+;    all.All
+;    all.API
+;    all.APIDefensive)))
 
 (copy_files constraints/*.ml)

dune-project

@@ -19,9 +19,9 @@
   (description "The core of Colibrics is formally proved using Why3.")
   (depends
     ("ppx_deriving_yojson" (>= "3.6.1"))
-    ("dolmen" (>= "0.7"))
-    ("dolmen_type" (>= "0.7"))
-    ("dolmen_loop" (>= "0.7"))
+    ("dolmen" (>= "0.8"))
+    ("dolmen_type" (>= "0.8"))
+    ("dolmen_loop" (>= "0.8"))
     "dune"
     ("zarith" (>= "1.12"))
     ("cmdliner" (>= 1.1.1))
@@ -56,9 +56,9 @@
          (depends
            ("colibrilib" (= :version))
            ("containers" (>= "3.6.1"))
-           ("dolmen" (>= "0.7"))
-           ("dolmen_type" (>= "0.7"))
-           ("dolmen_loop" (>= "0.7"))
+           ("dolmen" (>= "0.8"))
+           ("dolmen_type" (>= "0.8"))
+           ("dolmen_loop" (>= "0.8"))
            ("cmdliner" (>= 1.1.1))
            ("base" (>= v0.14.2))
            ("gen" (>= 1.0))