blob: bf0c19d7e359135fb209a4c899eac93b5a57118b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
{
description = "Aeneas";
inputs = {
charon.url = "github:aeneasverif/charon";
flake-utils.follows = "charon/flake-utils";
nixpkgs.follows = "charon/nixpkgs";
hacl-nix.url = "github:hacl-star/hacl-nix";
};
outputs = { self, charon, flake-utils, nixpkgs, hacl-nix }:
flake-utils.lib.eachSystem [ "x86_64-linux" ] (system:
let
pkgs = import nixpkgs { inherit system; };
ocamlPackages = pkgs.ocamlPackages;
coqPackages = pkgs.coqPackages;
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 ];
};
ocamlgraph = ocamlPackages.buildDunePackage rec {
pname = "ocamlgraph";
version = "2.0.0";
src = pkgs.fetchurl {
url = "https://github.com/backtracking/ocamlgraph/releases/download/2.0.0/ocamlgraph-2.0.0.tbz";
sha256 = "20fe267797de5322088a4dfb52389b2ea051787952a8a4f6ed70fcb697482609";
};
buildInputs = [ ocamlPackages.stdlib-shims ocamlPackages.graphics ];
};
unionFind = ocamlPackages.buildDunePackage rec {
pname = "unionFind";
version = "20220122";
src = pkgs.fetchurl {
url = "https://gitlab.inria.fr/fpottier/unionFind/-/archive/20220122/archive.tar.gz";
sha512 = "c49dd3f9a6689f6a5efe39c26efe2c137f8812b4be6ee76c2cc20068cf86ad73c0ac97ec9a543245dddb63792ce8c1904576b3435bf419cc7837bc5e368eee6d";
};
buildInputs = [];
};
aeneas = ocamlPackages.buildDunePackage {
pname = "aeneas";
version = "0.1.0";
src = ./compiler;
buildInputs = [ easy_logging ocamlgraph unionFind charon.packages.${system}.charon-ml ]
++ (with ocamlPackages; [
calendar
core_unix
ppx_deriving
visitors
yojson
zarith
]);
afterBuild = ''
echo charon.packages.${system}.tests
'';
};
# Run the translation on various files.
# Make sure we don't need to recompile the package whenever we make
# unnecessary changes - we list the exact files and folders the package
# depends upon.
aeneas-tests = pkgs.stdenv.mkDerivation {
name = "aeneas_tests";
src = pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
path == toString ./Makefile
|| pkgs.lib.hasPrefix (toString ./compiler) path
|| pkgs.lib.hasPrefix (toString ./backends) path
|| pkgs.lib.hasPrefix (toString ./tests) path;
};
buildPhase = ''
# We need to provide the paths to the Charon tests derivations
export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests}
export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius}
# Copy the Aeneas executable, and update the path to it
cp ${aeneas}/bin/aeneas_driver aeneas.exe
export AENEAS_EXE=./aeneas.exe
# Run the tests
make tests -j
'';
# Tests don't generate anything new as the generated files are
# versionned, but the installation phase still needs to prodocue
# something, otherwise Nix will consider the build has failed.
installPhase = "touch $out";
};
# Replay the F* proofs.
aeneas-verify-fstar = pkgs.stdenv.mkDerivation {
name = "aeneas_verify_fstar";
src = ./tests/fstar;
FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe";
buildPhase= ''
make prepare-projects
make verify -j
'';
# The tests don't generate anything
installPhase = "touch $out";
};
# Replay the Coq proofs.
aeneas-verify-coq = pkgs.stdenv.mkDerivation {
name = "aeneas_verify_coq";
src = ./tests/coq;
buildInputs = [ pkgs.coq ];
buildPhase= ''
make prepare-projects
make verify -j
'';
# The tests don't generate anything
installPhase = "touch $out";
};
in {
packages = {
inherit aeneas;
default = aeneas;
};
checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq; };
hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq; };
});
}
|
