Skip to content

Commit

Permalink
Merge pull request #446 from Nadrieril/fix-opam
Browse files Browse the repository at this point in the history
  • Loading branch information
Nadrieril authored Oct 31, 2024
2 parents cb24cf8 + 74b7c40 commit 0ad01a2
Show file tree
Hide file tree
Showing 9 changed files with 157 additions and 128 deletions.
5 changes: 1 addition & 4 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,7 @@ tests/src/betree/target
#===================
# Generated by dune
#===================
charon-ml/_build
charon-ml/name_matcher_parser/_build
charon/_build
charon/src/_build
_build

#===================
# Generated by Charon
Expand Down
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ charon-tests:

# Run the Charon ML tests on the .ullbc and .llbc files generated by Charon
.PHONY: charon-ml-tests
charon-ml-tests: build-charon-ml charon-tests
charon-ml-tests: build-charon-ml
cd charon-ml && make tests

# Generate some of the ml code automatically from the rust definitions.
Expand Down
8 changes: 3 additions & 5 deletions charon-ml/tests/Tests.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,6 @@ let () =
with Not_found -> log#set_level EL.Info

(* Call the tests *)
let () = Test_Deserialize.run_tests "../../../tests/serialized"

let () =
Test_NameMatcher.run_tests
"../../../tests/serialized/ml-name-matcher-tests.llbc"
(* llbc files are copied into the `_build` dir by the `(deps)` rule in `./dune`. *)
let () = Test_Deserialize.run_tests "./serialized"
let () = Test_NameMatcher.run_tests "./serialized/ml-name-matcher-tests.llbc"
1 change: 0 additions & 1 deletion charon/src/bin/generate-ml/generated

This file was deleted.

53 changes: 31 additions & 22 deletions charon/src/bin/generate-ml/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -974,10 +974,19 @@ fn main() -> Result<()> {
CrateData::deserialize(deserializer)?.translated
};

generate_ml(crate_data, dir)
let output_dir = if std::env::var("IN_CI").as_deref() == Ok("1") {
dir.join("generated")
} else {
dir.join("../../../../charon-ml/src")
};
generate_ml(crate_data, dir.join("templates"), output_dir)
}

fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Result<()> {
fn generate_ml(
crate_data: TranslatedCrate,
template_dir: PathBuf,
output_dir: PathBuf,
) -> anyhow::Result<()> {
let manual_type_impls = &[
// Hand-written because we replace the `FileId` with the corresponding file name.
(
Expand Down Expand Up @@ -1244,8 +1253,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
#[rustfmt::skip]
let generate_code_for = vec![
GenerateCodeFor {
template: output_dir.join("templates/GAst.ml"),
target: output_dir.join("generated/GAst.ml"),
template: template_dir.join("GAst.ml"),
target: output_dir.join("GAst.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "statement_base",
Expand Down Expand Up @@ -1275,8 +1284,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
]),
},
GenerateCodeFor {
template: output_dir.join("templates/Expressions.ml"),
target: output_dir.join("generated/Expressions.ml"),
template: template_dir.join("Expressions.ml"),
target: output_dir.join("Expressions.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(None), &[
"VarId",
Expand Down Expand Up @@ -1316,8 +1325,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
]),
},
GenerateCodeFor {
template: output_dir.join("templates/Meta.ml"),
target: output_dir.join("generated/Meta.ml"),
template: template_dir.join("Meta.ml"),
target: output_dir.join("Meta.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(None), &[
"Loc",
Expand All @@ -1332,8 +1341,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
]),
},
GenerateCodeFor {
template: output_dir.join("templates/Types.ml"),
target: output_dir.join("generated/Types.ml"),
template: template_dir.join("Types.ml"),
target: output_dir.join("Types.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(None), &[
"ConstGenericVarId",
Expand Down Expand Up @@ -1420,8 +1429,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
]),
},
GenerateCodeFor {
template: output_dir.join("templates/Values.ml"),
target: output_dir.join("generated/Values.ml"),
template: template_dir.join("Values.ml"),
target: output_dir.join("Values.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "literal",
Expand All @@ -1441,8 +1450,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
]),
},
GenerateCodeFor {
template: output_dir.join("templates/LlbcAst.ml"),
target: output_dir.join("generated/LlbcAst.ml"),
template: template_dir.join("LlbcAst.ml"),
target: output_dir.join("LlbcAst.ml"),
markers: vec![
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "statement",
Expand All @@ -1453,8 +1462,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
],
},
GenerateCodeFor {
template: output_dir.join("templates/UllbcAst.ml"),
target: output_dir.join("generated/UllbcAst.ml"),
template: template_dir.join("UllbcAst.ml"),
target: output_dir.join("UllbcAst.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "statement",
Expand Down Expand Up @@ -1483,18 +1492,18 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu
]),
},
GenerateCodeFor {
template: output_dir.join("templates/GAstOfJson.ml"),
target: output_dir.join("generated/GAstOfJson.ml"),
template: template_dir.join("GAstOfJson.ml"),
target: output_dir.join("GAstOfJson.ml"),
markers: vec![(GenerationKind::OfJson, gast_types)],
},
GenerateCodeFor {
template: output_dir.join("templates/LlbcOfJson.ml"),
target: output_dir.join("generated/LlbcOfJson.ml"),
template: template_dir.join("LlbcOfJson.ml"),
target: output_dir.join("LlbcOfJson.ml"),
markers: vec![(GenerationKind::OfJson, llbc_types)],
},
GenerateCodeFor {
template: output_dir.join("templates/UllbcOfJson.ml"),
target: output_dir.join("generated/UllbcOfJson.ml"),
template: template_dir.join("UllbcOfJson.ml"),
target: output_dir.join("UllbcOfJson.ml"),
markers: vec![(GenerationKind::OfJson, ullbc_types)],
},
];
Expand Down
File renamed without changes.
110 changes: 21 additions & 89 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -24,104 +24,20 @@
craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;

charon = pkgs.callPackage ./nix/charon.nix { inherit craneLib rustToolchain; };
charon-ml = pkgs.callPackage ./nix/charon-ml.nix { inherit charon; };

# Check rust files are correctly formatted.
charon-check-fmt = charon.passthru.check-fmt;
# Check that the crate builds with the "rustc" feature off.
charon-check-no-rustc = charon.passthru.check-no-rustc;

# A utility that extracts the llbc of a crate using charon. This uses
# `crane` to handle dependencies and toolchain management.
extractCrateWithCharon = { name, src, charonFlags ? "", craneExtraArgs ? { } }:
craneLib.buildPackage ({
inherit name;
src = pkgs.lib.cleanSourceWith {
inherit src;
filter = path: type: (craneLib.filterCargoSources path type);
};
cargoArtifacts = craneLib.buildDepsOnly { inherit src; };
buildPhase = ''
${charon}/bin/charon ${charonFlags} --dest $out/llbc
'';
dontInstall = true;
} // craneExtraArgs);
# Check ocaml files are correctly formatted.
charon-ml-check-fmt = charon-ml.charon-ml-check-fmt;
# Run ocaml tests
charon-ml-tests = charon-ml.charon-ml-tests;

# Runs charon on the whole rustc ui test suite.
rustc-tests = pkgs.callPackage ./nix/rustc-tests.nix { inherit charon rustToolchain; };

ocamlPackages = pkgs.ocamlPackages;
easy_logging = ocamlPackages.buildDunePackage rec {
pname = "easy_logging";
version = "0.8.2";
src = pkgs.fetchFromGitHub {
owner = "sapristi";
repo = "easy_logging";
rev = "v${version}";
sha256 = "sha256-Xy6Rfef7r2K8DTok7AYa/9m3ZEV07LlUeMQSRayLBco=";
};
buildInputs = [ ocamlPackages.calendar ];
};
charon-name_matcher_parser =
ocamlPackages.buildDunePackage {
pname = "name_matcher_parser";
version = "0.1.0";
duneVersion = "3";
nativeBuildInputs = with ocamlPackages; [
menhir
];
propagatedBuildInputs = with ocamlPackages; [
ppx_deriving
visitors
zarith
menhirLib
];
src = ./charon-ml;
};
mk-charon-ml = doCheck:
ocamlPackages.buildDunePackage {
pname = "charon";
version = "0.1.0";
duneVersion = "3";
OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
preCheck =
if doCheck then ''
mkdir -p tests/serialized
cp ${charon}/tests-llbc/* tests/serialized
'' else
"";
propagatedBuildInputs = with ocamlPackages; [
core
ppx_deriving
visitors
easy_logging
zarith
yojson
calendar
charon-name_matcher_parser
];
src = ./charon-ml;
inherit doCheck;
};
charon-ml = mk-charon-ml false;
charon-ml-tests = mk-charon-ml true;

charon-ml-check-fmt = pkgs.stdenv.mkDerivation {
name = "charon-ml-check-fmt";
src = ./charon-ml;
buildInputs = [
ocamlPackages.dune_3
ocamlPackages.ocaml
ocamlPackages.ocamlformat
];
buildPhase = ''
if ! dune build @fmt; then
echo 'ERROR: Ocaml code is not formatted. Run `make format` to format the project files'.
exit 1
fi
'';
installPhase = "touch $out";
};

# Check that the generated ocaml files match what is committed to the repo.
check-generated-ml = pkgs.runCommand "check-generated-ml" { } ''
mkdir generated
Expand Down Expand Up @@ -150,6 +66,22 @@
fi
touch $out
'';

# A utility that extracts the llbc of a crate using charon. This uses
# `crane` to handle dependencies and toolchain management.
extractCrateWithCharon = { name, src, charonFlags ? "", craneExtraArgs ? { } }:
craneLib.buildPackage ({
inherit name;
src = pkgs.lib.cleanSourceWith {
inherit src;
filter = path: type: (craneLib.filterCargoSources path type);
};
cargoArtifacts = craneLib.buildDepsOnly { inherit src; };
buildPhase = ''
${charon}/bin/charon ${charonFlags} --dest $out/llbc
'';
dontInstall = true;
} // craneExtraArgs);
in
{
packages = {
Expand Down
99 changes: 99 additions & 0 deletions nix/charon-ml.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
{ lib
, charon
, fetchFromGitHub
, ocamlPackages
, runCommand
, stdenv
}:
let
easy_logging = ocamlPackages.buildDunePackage rec {
pname = "easy_logging";
version = "0.8.2";
src = fetchFromGitHub {
owner = "sapristi";
repo = "easy_logging";
rev = "v${version}";
sha256 = "sha256-Xy6Rfef7r2K8DTok7AYa/9m3ZEV07LlUeMQSRayLBco=";
};
buildInputs = [ ocamlPackages.calendar ];
};

# We need both `charon-ml` and the `dune-project` file.
src = lib.cleanSourceWith {
src = ./..;
filter =
path: type:
(lib.hasPrefix (toString ../charon-ml) path)
|| (lib.hasPrefix (toString ../dune-project) path);
};

charon-name_matcher_parser =
ocamlPackages.buildDunePackage {
pname = "name_matcher_parser";
version = "0.1.0";
duneVersion = "3";
inherit src;

nativeBuildInputs = with ocamlPackages; [
menhir
];
propagatedBuildInputs = with ocamlPackages; [
ppx_deriving
visitors
zarith
menhirLib
];
};

charon-ml-check-fmt = stdenv.mkDerivation {
name = "charon-ml-check-fmt";
inherit src;

buildInputs = [
ocamlPackages.dune_3
ocamlPackages.ocaml
ocamlPackages.ocamlformat
];
buildPhase = ''
if ! dune build @fmt; then
echo 'ERROR: Ocaml code is not formatted. Run `make format` to format the project files'.
exit 1
fi
'';
installPhase = "touch $out";
};

mk-charon-ml = doCheck:
ocamlPackages.buildDunePackage {
pname = "charon";
version = "0.1.0";
duneVersion = "3";
inherit src;

OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
preCheck =
if doCheck then ''
mkdir -p charon-ml/tests/serialized
cp ${charon}/tests-llbc/* charon-ml/tests/serialized
'' else
"";
propagatedBuildInputs = with ocamlPackages; [
core
ppx_deriving
visitors
easy_logging
zarith
yojson
calendar
charon-name_matcher_parser
];
inherit doCheck;

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

charon-ml = mk-charon-ml false;
charon-ml-tests = mk-charon-ml true;

in
charon-ml
Loading

0 comments on commit 0ad01a2

Please sign in to comment.