Skip to content

Commit

Permalink
wip add l4v
Browse files Browse the repository at this point in the history
  • Loading branch information
wucke13 committed Oct 16, 2024
1 parent eba85d7 commit e53b413
Show file tree
Hide file tree
Showing 4 changed files with 93 additions and 0 deletions.
16 changes: 16 additions & 0 deletions .github/workflows/nix.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,22 @@ jobs:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
- name: Build
run: nix build .#packages.x86_64-linux.guardonce --print-build-logs
x86_64-linux---packages---l4v:
name: x86_64-linux---packages---l4v
runs-on:
- ubuntu-latest
needs: []
steps:
- uses: actions/checkout@v4
- uses: cachix/install-nix-action@v25
with:
nix_path: nixpkgs=channel:nixos-unstable
- uses: cachix/cachix-action@v14
with:
name: dlr-ft
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
- name: Build
run: nix build .#packages.x86_64-linux.l4v --print-build-logs
x86_64-linux---packages---microkit-sdk:
name: x86_64-linux---packages---microkit-sdk
runs-on:
Expand Down
6 changes: 6 additions & 0 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,12 @@
camkes-deps = pkgs.python3Packages.camkes-deps;


#
### Proofs
#
l4v = pkgs.l4v;


#
### microkit(-sdk)
#
Expand Down
2 changes: 2 additions & 0 deletions overlay.nix
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ final: prev: {
# https://android.googlesource.com/tools/repo
fetchGoogleRepoTool = prev.callPackage pkgs/fetch-google-repo-tool.nix { };

# L4.verified
l4v = prev.callPackage pkgs/l4v.nix { };

# microkit
microkit-sdk = prev.callPackage pkgs/microkit-sdk.nix { };
Expand Down
69 changes: 69 additions & 0 deletions pkgs/l4v.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
{ stdenvNoCC
, fetchGoogleRepoTool
, which
, isabelle
, cmake
, mlton
, ninja
, pkgsCross
, python3Packages
}:

stdenvNoCC.mkDerivation (finalAttrs: {
pname = "L4.verified";
version = "1.11";

src = fetchGoogleRepoTool {
url = "https://github.com/seL4/verification-manifest";
rev = "2b434d1957eba420782f10f90e58f0b93ee3a4b7"; # 2024-10-11
manifest = "13.0.0.xml";
hash = "sha256-GTjofiun3TWlKdHRegWJNIitRzcZTGuSZQG1tmLpBg0=";
};
# src = fetchFromGitHub {
# owner = "seL4";
# repo = "l4v";
# rev = "autocorres-${finalAttrs.version}";
# hash = "sha256-Rv3lhx3CE7jW9P+nW3JiYZXnMmr+qFcAiK/TMziYxyE=";
# };

nativeBuildInputs = [
which
isabelle
mlton

cmake
ninja

# compilers
pkgsCross.aarch64-embedded.stdenv.cc.bintools
pkgsCross.aarch64-embedded.stdenv.cc.cc
pkgsCross.arm-embedded.stdenv.cc.bintools
pkgsCross.arm-embedded.stdenv.cc.cc
pkgsCross.riscv64-embedded.stdenv.cc.bintools
pkgsCross.riscv64-embedded.stdenv.cc.cc
];

preUnpack = ''
HOME="$PWD/home"
mkdir --parent -- "$HOME"
'';

dontUseCmakeConfigure = true;

preConfigure = ''
rm --force --recursive -- isabelle
ln --force --symbolic -- ${isabelle} isabelle
'';

preBuild = ''
cd l4v/proof
'';

buildPhase = ''
runHook preInstall
make all
runHook postInstall
'';
})

0 comments on commit e53b413

Please sign in to comment.