From 55eb079ecd986aef2ad1a52592d1b3eaa532bf1f Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 15 May 2024 15:47:00 +0200
Subject: [PATCH] [chore] Private logging library
---
flake.nix | 2 +-
lib/ir/dune | 2 +-
lib/nnet/dune | 2 +-
lib/onnx/dune | 2 +-
lib/ovo/dune | 2 +-
lib/xgboost/dune | 2 +-
src/autodetect.ml | 1 +
src/dune | 2 +-
src/interpretation/interpreter.ml | 1 +
src/interpretation/interpreter_theory.ml | 1 +
src/main.ml | 1 +
src/proof_strategy.ml | 1 +
src/saver.ml | 1 +
src/transformations/nn2smt.ml | 1 +
src/transformations/utils.ml | 1 +
src/verification.ml | 1 +
utils/dune | 4 ++--
17 files changed, 18 insertions(+), 9 deletions(-)
diff --git a/flake.nix b/flake.nix
index 73f1d55..dadbee7 100644
--- a/flake.nix
+++ b/flake.nix
@@ -30,7 +30,7 @@
(nix-filter.lib.inDirectory "config")
(nix-filter.lib.inDirectory "stdlib")
(nix-filter.lib.inDirectory "doc")
- (nix-filter.lib.inDirectory "logging")
+ (nix-filter.lib.inDirectory "utils")
];
};
};
diff --git a/lib/ir/dune b/lib/ir/dune
index f212db4..4b24a3c 100644
--- a/lib/ir/dune
+++ b/lib/ir/dune
@@ -11,7 +11,7 @@
ppx_deriving.iter
ppx_deriving.fold))
(inline_tests)
- (libraries base ocamlgraph fmt stdio caisar.utils.log))
+ (libraries base ocamlgraph fmt stdio caisar_logging))
(env
(dev
diff --git a/lib/nnet/dune b/lib/nnet/dune
index e6d8d31..b6180d7 100644
--- a/lib/nnet/dune
+++ b/lib/nnet/dune
@@ -1,5 +1,5 @@
(library
(name nnet)
(public_name caisar.nnet)
- (libraries base csv caisar.utils.log)
+ (libraries base csv caisar_logging)
(synopsis "NNet parser for CAISAR"))
diff --git a/lib/onnx/dune b/lib/onnx/dune
index b2bcb09..37c850e 100644
--- a/lib/onnx/dune
+++ b/lib/onnx/dune
@@ -1,7 +1,7 @@
(library
(name onnx)
(public_name caisar.onnx)
- (libraries base stdio ocaml-protoc-plugin ocplib-endian caisar.ir caisar.utils.log)
+ (libraries base stdio ocaml-protoc-plugin ocplib-endian caisar.ir caisar_logging)
(synopsis "ONNX parser for CAISAR"))
(rule
diff --git a/lib/ovo/dune b/lib/ovo/dune
index 5317286..690e65c 100644
--- a/lib/ovo/dune
+++ b/lib/ovo/dune
@@ -1,5 +1,5 @@
(library
(name ovo)
(public_name caisar.ovo)
- (libraries base csv caisar.utils.log)
+ (libraries base csv caisar_logging)
(synopsis "OVO parser for CAISAR"))
diff --git a/lib/xgboost/dune b/lib/xgboost/dune
index 6ad494f..d0ad55c 100644
--- a/lib/xgboost/dune
+++ b/lib/xgboost/dune
@@ -4,4 +4,4 @@
(preprocess
(pps ppx_deriving.show ppx_deriving_yojson))
(flags -w -30)
- (libraries csv caisar.utils.log))
+ (libraries csv caisar_logging))
diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3c3f38e..9446e27 100644
--- a/src/autodetect.ml
+++ b/src/autodetect.ml
@@ -22,6 +22,7 @@
open Why3
open Base
+module Logging = Caisar_logging.Logging
let rec lookup_file dirs filename =
match dirs with
diff --git a/src/dune b/src/dune
index 6d61dd7..88921d5 100644
--- a/src/dune
+++ b/src/dune
@@ -21,7 +21,7 @@
yaml.unix
fpath
zarith
- caisar.utils.log
+ caisar_logging
caisar.xgboost)
(preprocess
(pps
diff --git a/src/interpretation/interpreter.ml b/src/interpretation/interpreter.ml
index 128ec43..ff82e51 100644
--- a/src/interpretation/interpreter.ml
+++ b/src/interpretation/interpreter.ml
@@ -23,6 +23,7 @@
module IRE = Interpreter_reduction_engine
module ITypes = Interpreter_types
open Base
+module Logging = Caisar_logging.Logging
let builtin_of_constant env known_map (name, value) =
let decls =
diff --git a/src/interpretation/interpreter_theory.ml b/src/interpretation/interpreter_theory.ml
index 55b5688..cc9d55f 100644
--- a/src/interpretation/interpreter_theory.ml
+++ b/src/interpretation/interpreter_theory.ml
@@ -22,6 +22,7 @@
module IRE = Interpreter_reduction_engine
module ITypes = Interpreter_types
+module Logging = Caisar_logging.Logging
open Base
(* TODO: Remove this and use common one. *)
diff --git a/src/main.ml b/src/main.ml
index d9b8041..f4f0fec 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -22,6 +22,7 @@
open Base
open Cmdliner
+module Logging = Caisar_logging.Logging
let caisar = "caisar"
diff --git a/src/proof_strategy.ml b/src/proof_strategy.ml
index 29a9789..e40381d 100644
--- a/src/proof_strategy.ml
+++ b/src/proof_strategy.ml
@@ -22,6 +22,7 @@
open Base
open Why3
+module Logging = Caisar_logging.Logging
let sls_model ~lookup sls =
let rec aux acc term =
diff --git a/src/saver.ml b/src/saver.ml
index 39e18c4..0971678 100644
--- a/src/saver.ml
+++ b/src/saver.ml
@@ -22,6 +22,7 @@
open Why3
open Base
+module Logging = Caisar_logging.Logging
let src = Logs.Src.create "SAVer" ~doc:"SAVer prover"
diff --git a/src/transformations/nn2smt.ml b/src/transformations/nn2smt.ml
index 34e4cca..a17c519 100644
--- a/src/transformations/nn2smt.ml
+++ b/src/transformations/nn2smt.ml
@@ -22,6 +22,7 @@
open Base
module IR = Ir.Nier_simple
+module Logging = Caisar_logging.Logging
let src =
Logs.Src.create "NN2SMT" ~doc:"Encoding of neural networks into SMT-LIB"
diff --git a/src/transformations/utils.ml b/src/transformations/utils.ml
index 8638ff6..10cba74 100644
--- a/src/transformations/utils.ml
+++ b/src/transformations/utils.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Base
+module Logging = Caisar_logging.Logging
let src = Logs.Src.create "TransformationsUtils" ~doc:"Transformation utils"
diff --git a/src/verification.ml b/src/verification.ml
index 45e6cb6..1eb9278 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -22,6 +22,7 @@
open Why3
open Base
+module Logging = Caisar_logging.Logging
module File = struct
type t =
diff --git a/utils/dune b/utils/dune
index 5a11529..a70bed4 100644
--- a/utils/dune
+++ b/utils/dune
@@ -1,5 +1,5 @@
(library
- (name logging)
- (public_name caisar.utils.log)
+ (name caisar_logging)
+ (package caisar)
(libraries base csv logs logs.cli logs.fmt fmt why3)
(synopsis "Logging utilities for CAISAR"))
--
GitLab