diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 21cc8bd1e39ede5588f11be9e9a8759f98eacd4d..7d588a88fab1b3438acac477772223afe4ef27c8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,6 +1,10 @@ variables: CAISAR_VERSION: "0.2.0" +default: + interruptible: true + tags: [ nix-v2 ] + stages: - build - test @@ -10,12 +14,7 @@ stages: build: stage: build script: - - nix --extra-experimental-features "nix-command flakes" build - - nix --extra-experimental-features "nix-command flakes" flake check - tags: - - nix-v2 - when: always - interruptible: true + - nix --extra-experimental-features "nix-command flakes" develop --command make test-ci # Optional and manual full rebuild using a clean docker image full_rebuild_and_test: @@ -40,16 +39,12 @@ full_rebuild_and_test: tags: - docker when: manual - interruptible: true test: stage: test script: + - nix --extra-experimental-features "nix-command flakes" build - nix --extra-experimental-features "nix-command flakes" flake check - tags: - - nix-v2 - when: always - interruptible: true ## Manual generation of the documentation @@ -61,10 +56,7 @@ documentation: paths: - result/share/doc/ocaml4.14.1-caisar-${CAISAR_VERSION}/html - result/share/doc/ocaml4.14.1-caisar-${CAISAR_VERSION}/latex - tags: - - nix-v2 when: manual - interruptible: true ################################################################################ ### PUBLIC diff --git a/flake.nix b/flake.nix index 01d199d6b2214ce7547792a2937160ea28a62683..495fda6cf14606d2bf777056c1eabd75cf94bb34 100644 --- a/flake.nix +++ b/flake.nix @@ -26,7 +26,9 @@ "Makefile" (nix-filter.lib.inDirectory "src") (nix-filter.lib.inDirectory "lib") - (nix-filter.lib.inDirectory "test") + (nix-filter.lib.inDirectory "tests") + (nix-filter.lib.inDirectory "config") + (nix-filter.lib.inDirectory "stdlib") (nix-filter.lib.inDirectory "doc") ]; }; @@ -49,6 +51,7 @@ pkgs.protobuf # For documentation pkgs.sphinxHook + pkgs.which ]; sphinxBuilders = [ "html" diff --git a/lib/ir/nier_cfg.ml b/lib/ir/nier_cfg.ml index 53e32cf741a17ec169cf6f076bc01f776aa9dd20..4e1753c4cbe83d295b40578e81fd5db3050f1923 100644 --- a/lib/ir/nier_cfg.ml +++ b/lib/ir/nier_cfg.ml @@ -486,7 +486,7 @@ module NierCFGDot = Graph.Graphviz.Dot (struct let graph_attributes _ = [] end) -let print_cfg_graph g = NierCFGDot.fprint_graph Caml.Format.std_formatter g +let print_cfg_graph g = NierCFGDot.fprint_graph Stdlib.Format.std_formatter g let out_cfg_graph g = let file = Out_channel.create "cfg.dot" in diff --git a/lib/nnet/nnet.ml b/lib/nnet/nnet.ml index b16b6f78202bbbdfc00cc945e38db77858e9e900..16b237b79521d393fd2165939085de4b58b72ba2 100644 --- a/lib/nnet/nnet.ml +++ b/lib/nnet/nnet.ml @@ -21,10 +21,10 @@ (**************************************************************************) open Base -module Format = Caml.Format -module Sys = Caml.Sys -module Filename = Caml.Filename -module Fun = Caml.Fun +module Format = Stdlib.Format +module Sys = Stdlib.Sys +module Filename = Stdlib.Filename +module Fun = Stdlib.Fun type t = { n_layers : int; diff --git a/lib/onnx/onnx.ml b/lib/onnx/onnx.ml index ffb3c775a75d87fb174ea4b8bb2f22d91476c690..355aa439d9c10cfb9ca06c6dcfba29b1a1d68b13 100644 --- a/lib/onnx/onnx.ml +++ b/lib/onnx/onnx.ml @@ -21,8 +21,8 @@ (**************************************************************************) open Base -module Format = Caml.Format -module Fun = Caml.Fun +module Format = Stdlib.Format +module Fun = Stdlib.Fun module Oproto = Onnx_protoc (* Autogenerated during compilation *) module Oprotom = Oproto.Onnx.ModelProto module NCFG = Ir.Nier_cfg diff --git a/lib/ovo/ovo.ml b/lib/ovo/ovo.ml index 42af2a06f8fa107f73a2f64400815024f2aec16c..90c2f48ef2f4d7e7ef407ee3fa20a792e4e09ca8 100644 --- a/lib/ovo/ovo.ml +++ b/lib/ovo/ovo.ml @@ -21,10 +21,10 @@ (**************************************************************************) open Base -module Format = Caml.Format -module Sys = Caml.Sys -module Filename = Caml.Filename -module Fun = Caml.Fun +module Format = Stdlib.Format +module Sys = Stdlib.Sys +module Filename = Stdlib.Filename +module Fun = Stdlib.Fun type t = { n_inputs : int; diff --git a/src/aimos.ml b/src/aimos.ml index 4343ead38b1614bb1edc9e3cd0c71a724969651c..371cdf0bff4016cd82d35f110b15facf2de079b3 100644 --- a/src/aimos.ml +++ b/src/aimos.ml @@ -27,9 +27,9 @@ let re_aimos_file = Re__Core.(compile (str "%{aimos_file}")) let write_config inputs_path models_path perturbation perturbation_path out_mode amplitude = - let config_file = Caml.Filename.temp_file "aimos-" ".yml" in + let config_file = Stdlib.Filename.temp_file "aimos-" ".yml" in let config_path = Fpath.v config_file in - let cwd = Caml.Sys.getcwd () in + let cwd = Stdlib.Sys.getcwd () in let ampli = Dataset.string_of_amplitude amplitude in let transformations = match ampli with diff --git a/src/autodetect.ml b/src/autodetect.ml index 4bf32804915a345c2216187f58d47f41e3f2efc7..3ab29fcb3875ca3c17bd391190a6afedf5b28b2c 100644 --- a/src/autodetect.ml +++ b/src/autodetect.ml @@ -25,10 +25,10 @@ open Base let rec lookup_file dirs filename = match dirs with - | [] -> raise Caml.Not_found + | [] -> raise Stdlib.Not_found | dir :: dirs -> - let file = Caml.Filename.concat dir filename in - if Caml.Sys.file_exists file then file else lookup_file dirs filename + let file = Stdlib.Filename.concat dir filename in + if Stdlib.Sys.file_exists file then file else lookup_file dirs filename let autodetection () = let debug = Logging.(is_debug_level src_autodetect) in @@ -49,6 +49,6 @@ let autodetection () = } :: acc) in - let config = Whyconf.init_config (Some Caml.Filename.null) in + let config = Whyconf.init_config (Some Stdlib.Filename.null) in let provers = Autodetection.compute_builtin_prover provers config data in Whyconf.set_provers config provers diff --git a/src/convert_xgboost.ml b/src/convert_xgboost.ml index c8373f4ee4c191ed94833313b7405bd91e1d87aa..34856a41fca089890c07075ba9ade22c8c3efdde 100644 --- a/src/convert_xgboost.ml +++ b/src/convert_xgboost.ml @@ -247,8 +247,8 @@ let prove_and_print ?memlimit ?timelimit env config prover task = let driver = Why3.Driver.load_driver_for_prover main env config_prover in (* let open Why3 in match String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver with | None -> Driver.load_driver_for_prover main env - config_prover | Some file -> let file = Caml.Filename.concat - (Caml.Filename.concat (List.hd_exn Dirs.Sites.config) "drivers") file in + config_prover | Some file -> let file = Stdlib.Filename.concat + (Stdlib.Filename.concat (List.hd_exn Dirs.Sites.config) "drivers") file in Driver.load_driver_file_and_extras main env file config_prover.extra_drivers in *) let command = diff --git a/src/interpretation.ml b/src/interpretation.ml index a5850f2a0906f53d3e523b30de9eee02271cd815..5886078cad58765d958db1f64d8c4443a61b4178 100644 --- a/src/interpretation.ml +++ b/src/interpretation.ml @@ -122,7 +122,7 @@ let value_int i = CRE.Value (Int i) let caisar_builtins : caisar_env CRE.built_in_theories list = let reconstruct () = (* Force the engine to reconstruct the original term. *) - raise Caml.Not_found + raise Stdlib.Not_found in let error_message ls = Fmt.str "Invalid arguments for '%a'" Pretty.print_ls ls @@ -258,7 +258,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list = ] -> let { env; cwd; _ } = CRE.user_env engine in let caisar_op = - let filename = Caml.Filename.concat cwd neural_network in + let filename = Stdlib.Filename.concat cwd neural_network in let nn = match id_string with | "NNet" -> NNet (Language.create_nn_nnet env filename) @@ -289,7 +289,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list = ] -> let { env; cwd; _ } = CRE.user_env engine in let caisar_op = - let filename = Caml.Filename.concat cwd dataset in + let filename = Stdlib.Filename.concat cwd dataset in let ds = Language.create_dataset_csv env filename in let dataset = DS_csv (Csv.load filename) in Dataset (ds, dataset) diff --git a/src/json.ml b/src/json.ml index d08217519e60046954879770d7ed7eb0d5e7e723..4adc054344010fa8ff4915c0645eef96914d86df 100644 --- a/src/json.ml +++ b/src/json.ml @@ -73,7 +73,7 @@ let pretty_output fmt = Fmt.fmt "%a" fmt pp_output let theory_of_input env input = let th_as_array = let model_parser = - let extension = Caml.Filename.(extension (basename input.model)) in + let extension = Stdlib.Filename.(extension (basename input.model)) in match String.lowercase extension with | ".nnet" -> Language.nnet_parser | ".onnx" -> Language.onnx_parser diff --git a/src/main.ml b/src/main.ml index 61f910b127874f4787ce94af33560448779ac2cc..3183ba7d2d2ff88b3fdb0823671b7bf93daabb30 100644 --- a/src/main.ml +++ b/src/main.ml @@ -422,4 +422,4 @@ let () = Logging.protect_main (fun () -> Cmd.group ~default:default_cmd default_info [ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ] - |> Cmd.eval ~catch:false |> Caml.exit) + |> Cmd.eval ~catch:false |> Stdlib.exit) diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml index 090820a1cca9550030ea2415c4c247e14b16433e..f908cf2d1004623a7dbcb81bc60a14518de826a9 100644 --- a/src/transformations/native_nn_prover.ml +++ b/src/transformations/native_nn_prover.ml @@ -103,7 +103,7 @@ let simplify_nn_application input_vars output_vars = | Some output_vars -> let index = Number.to_small_integer index in assert (index < List.length output_vars); - let ls = Caml.List.assoc index output_vars in + let ls = Stdlib.List.assoc index output_vars in Term.t_app_infer ls []) | _ -> Term.t_map do_simplify term in diff --git a/src/transformations/nn2smt.ml b/src/transformations/nn2smt.ml index cd5b28c7834e8bbaaf763090df193b92195503aa..5d7b91c4effc089dd9165ee0786ed2bca8b9a1c8 100644 --- a/src/transformations/nn2smt.ml +++ b/src/transformations/nn2smt.ml @@ -59,7 +59,7 @@ let term_of_data d ty = | Some g -> ( ( Re__Core.Group.get g 1, Re__Core.Group.get g 2, - try Re__Core.Group.get g 3 with Caml.Not_found -> "" )) + try Re__Core.Group.get g 3 with Stdlib.Not_found -> "" )) | None -> failwith "Wrong assertion in fp regex." in let exp = if String.equal exp "" then None else Some exp in diff --git a/src/verification.ml b/src/verification.ml index a6c4682711f67a15f82333c7caa873edc3c211b8..7106b0661dde2adb1f12d463ae2bc92bcce381ba 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -30,9 +30,9 @@ module File = struct | JSON of Json.input let of_json_input jin = - if Caml.Sys.file_exists jin.Json.model + if Stdlib.Sys.file_exists jin.Json.model then - if Caml.Sys.file_exists jin.property.dataset + if Stdlib.Sys.file_exists jin.property.dataset then if String.is_suffix jin.property.dataset ~suffix:".csv" then Ok (JSON jin) @@ -46,7 +46,7 @@ module File = struct let of_string s = if String.equal s "-" then Ok Stdin - else if Caml.Sys.file_exists s + else if Stdlib.Sys.file_exists s then Ok (File s) else Error (Fmt.str "No '%s' file or directory" s) @@ -297,10 +297,10 @@ let open_file ?format env file = match file with | File.Stdin -> ( Unix.getcwd (), - Env.(read_channel ?format base_language env "stdin" Caml.stdin) ) + Env.(read_channel ?format base_language env "stdin" Stdlib.stdin) ) | File file -> let mlw_files, _ = Env.(read_file ?format base_language env file) in - (Caml.Filename.dirname file, mlw_files) + (Stdlib.Filename.dirname file, mlw_files) | JSON jin -> let th = Json.theory_of_input env jin in (Unix.getcwd () (* TODO *), Wstdlib.Mstr.singleton th.th_name.id_string th) diff --git a/tests/filter_tmpdir.sh b/tests/filter_tmpdir.sh index cb7a66c1f6ada434a1389398dfe8e9cfc7387d48..fc7fcdd583011ff3bb829531314bc491878037be 100755 --- a/tests/filter_tmpdir.sh +++ b/tests/filter_tmpdir.sh @@ -1,3 +1,3 @@ -#!/bin/bash -eu +#!/bin/sh -eu exec sed -e "s&${TMPDIR:-/tmp}/[a-z0-9_./]*&\$TMPFILE&"