From 641607e35997d9f4e652ca1b58b021efab364d1a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 14 Dec 2022 17:23:41 +0100
Subject: [PATCH] Bump dolmen version
---
colibri2.opam | 8 ++--
colibri2/bin/dune | 20 ----------
colibrics.opam | 6 +--
colibrics/lib/dune | 96 +++++++++++++++++++++++-----------------------
dune-project | 12 +++---
5 files changed, 61 insertions(+), 81 deletions(-)
diff --git a/colibri2.opam b/colibri2.opam
index b0593c8d7..8c522e291 100644
--- a/colibri2.opam
+++ b/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: [
diff --git a/colibri2/bin/dune b/colibri2/bin/dune
index ecb413746..4972cdcbe 100644
--- a/colibri2/bin/dune
+++ b/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
diff --git a/colibrics.opam b/colibrics.opam
index 1d6645128..47f877875 100644
--- a/colibrics.opam
+++ b/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"}
diff --git a/colibrics/lib/dune b/colibrics/lib/dune
index 6404a361e..3b9d8472d 100644
--- a/colibrics/lib/dune
+++ b/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)
diff --git a/dune-project b/dune-project
index 63cf17c55..a268a6e45 100644
--- a/dune-project
+++ b/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))
--
GitLab