71 lines
2.1 KiB
Nix
71 lines
2.1 KiB
Nix
{
|
|
lib,
|
|
buildDotnetModule,
|
|
fetchFromGitHub,
|
|
z3,
|
|
dotnetCorePackages,
|
|
nix-update-script,
|
|
}:
|
|
|
|
buildDotnetModule rec {
|
|
pname = "Boogie";
|
|
version = "3.5.5";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "boogie-org";
|
|
repo = "boogie";
|
|
tag = "v${version}";
|
|
hash = "sha256-OuNzxzcoWrDCmUfQNXEif5wIY+L5jql14231m7nNBe4=";
|
|
};
|
|
|
|
dotnet-sdk = dotnetCorePackages.sdk_8_0;
|
|
projectFile = [ "Source/Boogie.sln" ];
|
|
nugetDeps = ./deps.json;
|
|
|
|
# [...]Microsoft.NET.Publish.targets(248,5): error MSB3021: Unable to copy file "[...]/NUnit3.TestAdapter.pdb" to "[...]/NUnit3.TestAdapter.pdb". Access to the path '[...]/NUnit3.TestAdapter.pdb' is denied. [[...]/ExecutionEngineTests.csproj]
|
|
enableParallelBuilding = false;
|
|
|
|
executables = [ "BoogieDriver" ];
|
|
|
|
makeWrapperArgs = [
|
|
"--prefix PATH : ${z3}/bin"
|
|
];
|
|
|
|
postInstall = ''
|
|
# so that this derivation can be used as a vim plugin to install syntax highlighting
|
|
vimdir=$out/share/vim-plugins/boogie
|
|
install -Dt $vimdir/syntax/ Util/vim/syntax/boogie.vim
|
|
mkdir $vimdir/ftdetect
|
|
echo 'au BufRead,BufNewFile *.bpl set filetype=boogie' > $vimdir/ftdetect/bpl.vim
|
|
mkdir -p $out/share/nvim
|
|
ln -s $out/share/vim-plugins/boogie $out/share/nvim/site
|
|
'';
|
|
|
|
postFixup = ''
|
|
ln -s "$out/bin/BoogieDriver" "$out/bin/boogie"
|
|
'';
|
|
|
|
doInstallCheck = true;
|
|
installCheckPhase = ''
|
|
$out/bin/boogie ${./install-check-file.bpl}
|
|
'';
|
|
|
|
passthru.updateScript = nix-update-script { };
|
|
|
|
meta = {
|
|
description = "Intermediate verification language";
|
|
changelog = "https://github.com/boogie-org/boogie/releases/tag/${src.tag}";
|
|
homepage = "https://github.com/boogie-org/boogie";
|
|
longDescription = ''
|
|
Boogie is an intermediate verification language (IVL), intended as a
|
|
layer on which to build program verifiers for other languages.
|
|
|
|
This derivation may be used as a vim plugin to provide syntax highlighting.
|
|
'';
|
|
license = lib.licenses.mspl;
|
|
mainProgram = "boogie";
|
|
maintainers = with lib.maintainers; [ taktoa ];
|
|
platforms = with lib.platforms; linux ++ darwin;
|
|
};
|
|
}
|