Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ charon/tests/cargo/**/target

# Temporary files we don't want to commit
charon-ml/tests/serialized
charon-ml/tests/test-outputs/*
/bin

# Generated by charon
Expand Down
9 changes: 6 additions & 3 deletions charon-ml/tests/Tests.ml
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,13 @@ let () =
log#set_level EL.Debug
with Not_found -> log#set_level EL.Info

let llbc_dir =
try Unix.getenv "CHARON_TESTS_DIR" with Not_found -> "../../charon/tests/ui"

(* Call the tests *)
(* llbc files are copied into the `_build` dir by the `(deps)` rule in `./dune`. *)
let () = Test_Deserialize.run_tests "test-outputs"
let () = Test_NameMatcher.run_tests "test-outputs/ml-name-matcher-tests.llbc"
let () = Test_Deserialize.run_tests llbc_dir
let () = Test_NameMatcher.run_tests (llbc_dir ^ "/ml-name-matcher-tests.llbc")

let () =
Test_NameMatcher.run_tests "test-outputs/ml-mono-name-matcher-tests.llbc"
Test_NameMatcher.run_tests (llbc_dir ^ "/ml-mono-name-matcher-tests.llbc")
2 changes: 1 addition & 1 deletion charon-ml/tests/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,5 @@
(modes byte exe)
(modules Tests Test_Deserialize Test_NameMatcher)
(deps
(glob_files_rec ./test-outputs/*))
(glob_files_rec ../../charon/tests/ui/*))
(libraries charon))
1 change: 0 additions & 1 deletion charon-ml/tests/test-outputs

This file was deleted.

1 change: 1 addition & 0 deletions dune
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(data_only_dirs charon)
16 changes: 10 additions & 6 deletions nix/charon-ml.nix
Original file line number Diff line number Diff line change
Expand Up @@ -71,12 +71,6 @@ let
duneVersion = "3";
inherit src;

OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
preCheck =
if doCheck then ''
ln -sf ${charon}/tests-llbc charon-ml/tests/test-outputs
'' else
"";
propagatedBuildInputs = with ocamlPackages; [
core
ppx_deriving
Expand All @@ -89,7 +83,17 @@ let
unionFind
ocaml-ng.ocamlPackages_4_14.ppx_tools # to view the output of visitor derivation
];

OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
CHARON_TESTS_DIR = lib.optionalString doCheck "${charon}/tests-llbc"; # Tell the tests where to find the llbc files.

inherit doCheck;
preBuild = ''
# This refers to a directory that doesn't exist in the current
# environment. We don't need dune here because tests can access the
# files directly, so we remove the dependency clause.
sed -i 's#(glob_files_rec [^)]*)##' charon-ml/tests/dune
'';

passthru = { inherit charon-ml-tests charon-ml-check-fmt; };
};
Expand Down