diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 55bd624be55db2fafbf2774476be604cb5dc5308..29e99c729d6d41258e38cfb1058fe7ecbac0dbfa 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -6,8 +6,9 @@ tests: - opam pin --no-action . - opam depext colibri2 - opam install --deps-only . - - opam depext --install why3 + - 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? - make - - make tests + - make test tags: - docker diff --git a/colibri2.opam b/colibri2.opam index 14d78f6f9eff043bc5e3169a227af737a0c9e509..ae8ca35aef5707584e7e3a506ec61a66715ad920 100644 --- a/colibri2.opam +++ b/colibri2.opam @@ -13,6 +13,7 @@ license: "LGPL-3.0-only" homepage: "https://git.frama-c.com/bobot/colibrics" bug-reports: "https://git.frama-c.com/bobot/colibrics/issues" depends: [ + "colibrics" "containers" {>= "2.1"} "dolmen" {>= "0.5~dev"} "dolmen_type" {>= "0.5~dev"} diff --git a/dune-project b/dune-project index 50dd2013d4f830d596036d9a90d2df4c2e28801e..b758b5f529cac977a85b13db3416694c31e27363 100644 --- a/dune-project +++ b/dune-project @@ -30,6 +30,7 @@ (synopsis "A CP solver for smtlib") (description "A reimplementation of COLIBRI in OCaml") (depends + "colibrics" ("containers" (>= "2.1")) ("dolmen" (>= "0.5~dev")) ("dolmen_type" (>= "0.5~dev")) diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli index 36c65db1e422d9f17cb1a91bd95ac60b34ccc1f5..901e3b29644322bf3155a06445a12e175d9fc960 100644 --- a/src_colibri2/core/demon.mli +++ b/src_colibri2/core/demon.mli @@ -75,7 +75,7 @@ module Key: sig (** the Events.t in wakeup is a subset of the one given in watch *) end - module Register (D:S): sig + module Register (_:S): sig val init: Egraph.t -> unit (** to run for each new delay *) end diff --git a/src_colibri2/theories/quantifier/PC.ml b/src_colibri2/theories/quantifier/PC.ml index 485fa19fa739a844853c088ef1f88068c238b7ae..76c828be09f150182287660eb1929be3ed50281c 100644 --- a/src_colibri2/theories/quantifier/PC.ml +++ b/src_colibri2/theories/quantifier/PC.ml @@ -3,8 +3,7 @@ open Colibri2_popop_lib module T = struct open! Base - type t = { parent : F_Pos.t; child : F.t } - [@@deriving show, ord, hash, show, eq] + type t = { parent : F_Pos.t; child : F.t } [@@deriving show, ord, hash, eq] end include T diff --git a/src_colibri2/theories/quantifier/PP.ml b/src_colibri2/theories/quantifier/PP.ml index 1cebebf12219c955ffd0c8db6ce61a86358d9a2e..903815458c0456c1ff3e7a3ad570e1f8e5564212 100644 --- a/src_colibri2/theories/quantifier/PP.ml +++ b/src_colibri2/theories/quantifier/PP.ml @@ -4,7 +4,7 @@ module T = struct open! Base type t = { parent1 : F_Pos.t; parent2 : F_Pos.t } - [@@deriving show, ord, hash, show, eq] + [@@deriving show, ord, hash, eq] end include T