Skip to content

Commit

Permalink
CI: nix files for coq coverage example and library
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Nov 28, 2024
1 parent 13b86ce commit 197d1a3
Show file tree
Hide file tree
Showing 6 changed files with 126 additions and 53 deletions.
66 changes: 33 additions & 33 deletions .github/workflows/extract_and_run_coq.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,40 +14,40 @@ jobs:

- name: ⤵ Install hax
run: |
nix profile install --verbose ./hax
nix build .\#coq-coverage-example
- name: build coverage example
working-directory: hax/examples/coverage
run: |
nix run . into coq
# - name: build coverage example
# working-directory: hax/examples/coverage
# run: |
# nix run . into coq

- name: install annotated core for coq
working-directory: hax/proof-libs/coq/coq/generated-core
run: |
nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
nix-shell --packages coq coqPackages.coq-record-update --run "make" && \
nix-shell --packages coq coqPackages.coq-record-update --run "sudo make install"
# - name: install annotated core for coq
# working-directory: hax/proof-libs/coq/coq/generated-core
# run: |
# nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
# nix-shell --packages coq coqPackages.coq-record-update --run "make" && \
# nix-shell --packages coq coqPackages.coq-record-update --run "sudo make install"

- name: run coq - coverage
working-directory: hax/examples/coverage/proofs/coq/extraction
run: |
sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here.
nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
nix-shell --packages coq coqPackages.coq-record-update --run "make"
# - name: run coq - coverage
# working-directory: hax/examples/coverage/proofs/coq/extraction
# run: |
# sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here.
# nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
# nix-shell --packages coq coqPackages.coq-record-update --run "make"

- name: build and run coq on tests
env:
FILES: assert attribute-opaque enum-struct-variant
NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions
run: |
for f in $FILES; do \
cd hax/tests/$f && \
nix run . into coq && \
cd ../../..
done
for f in $FILES; do \
cd hax/tests/$f/proofs/coq/extraction && \
nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
nix-shell --packages coq coqPackages.coq-record-update --run "make" && \
cd ../../../../../../
done
# - name: build and run coq on tests
# env:
# FILES: assert attribute-opaque enum-struct-variant
# NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions
# run: |
# for f in $FILES; do \
# cd hax/tests/$f && \
# nix run . into coq && \
# cd ../../..
# done
# for f in $FILES; do \
# cd hax/tests/$f/proofs/coq/extraction && \
# nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
# nix-shell --packages coq coqPackages.coq-record-update --run "make" && \
# cd ../../../../../../
# done
26 changes: 26 additions & 0 deletions examples/commonArgs.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
{
craneLib,
lib,
}:
let
matches = re: path: !builtins.isNull (builtins.match re path);
in
{
version = "0.0.1";
src = lib.cleanSourceWith {
src = craneLib.path ./..;
filter = path: type:
# We include only certain files. FStar files under the example
# directory are listed out. Same for proverif (*.pvl) files.
( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?|pv))$" path
&& !matches ".*examples/.*[.]fsti?$" path
) || ("directory" == type);
};
doCheck = false;
cargoVendorDir = craneLib.vendorMultipleCargoDeps {
cargoLockList = [
./Cargo.lock
../Cargo.lock
];
};
}
38 changes: 38 additions & 0 deletions examples/coverage/default.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
{
stdenv,
lib,
hax,
coqPackages,
gnused,
craneLib,
bat,
coqGeneratedCore ? import ../../proof-libs/coq/coq {inherit stdenv coqPackages;},
}:
let
commonArgs = import ../commonArgs.nix {inherit craneLib lib;};
cargoArtifacts = craneLib.buildDepsOnly commonArgs;
in
craneLib.mkCargoDerivation (commonArgs
// {
inherit cargoArtifacts;
pname = "coverage";
doCheck = false;
buildPhaseCargoCommand = ''
cd examples/coverage
cargo hax into coq
cd proofs/coq/extraction
echo -e "-R ${coqGeneratedCore}/lib/coq/user-contrib/Core Core\n$(cat _CoqProject)" > _CoqProject
coq_makefile -f _CoqProject -o Makefile
make
'';
buildInputs = [
hax
coqPackages.coq-record-update
coqPackages.coq
gnused
];
})


# COQLIB
21 changes: 1 addition & 20 deletions examples/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -9,26 +9,7 @@
jq,
proverif,
}: let
matches = re: path: !builtins.isNull (builtins.match re path);
commonArgs = {
version = "0.0.1";
src = lib.cleanSourceWith {
src = craneLib.path ./..;
filter = path: type:
# We include only certain files. FStar files under the example
# directory are listed out. Same for proverif (*.pvl) files.
( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?|pv))$" path
&& !matches ".*examples/.*[.]fsti?$" path
) || ("directory" == type);
};
doCheck = false;
cargoVendorDir = craneLib.vendorMultipleCargoDeps {
cargoLockList = [
./Cargo.lock
../Cargo.lock
];
};
};
commonArgs = import ./commonArgs.nix {inherit craneLib lib;};
cargoArtifacts = craneLib.buildDepsOnly commonArgs;
in
craneLib.mkCargoDerivation (commonArgs
Expand Down
6 changes: 6 additions & 0 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,12 @@
check-examples = checks.examples;
check-readme-coherency = checks.readme-coherency;

coq-coverage-example = pkgs.callPackage ./examples/coverage {
inherit (packages) hax;
inherit (pkgs) coqPackages;
inherit craneLib;
};

rust-by-example-hax-extraction = pkgs.stdenv.mkDerivation {
name = "rust-by-example-hax-extraction";
phases = ["installPhase"];
Expand Down
22 changes: 22 additions & 0 deletions proof-libs/coq/coq/default.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
{
stdenv ? (import <nixpkgs> {}).stdenv,
coqPackages ? (import <nixpkgs> {}).coqPackages,
}:
stdenv.mkDerivation {
name = "hax-coq-generated-core";
src = ./generated-core;
buildPhase = ''
coq_makefile -f _CoqProject -o Makefile
make
'';
installPhase = ''
export DESTDIR=$out
make install
mv $out/nix/store/*/lib $out
rm -rf $out/nix
'';
buildInputs = [
coqPackages.coq-record-update
coqPackages.coq
];
}

0 comments on commit 197d1a3

Please sign in to comment.