blob: 528e62179eb068bca85f9b60383cf12dd22c51cd (
plain) (
blame)
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
|
{ lib, buildDotnetModule, fetchFromGitHub, z3 }:
buildDotnetModule rec {
pname = "Boogie";
version = "3.2.1";
src = fetchFromGitHub {
owner = "boogie-org";
repo = "boogie";
rev = "v${version}";
sha256 = "sha256-89S3yBjEUHbQbuWWLe/pTMaDOCqDR04hNJwIRzh5xaI=";
};
projectFile = [ "Source/Boogie.sln" ];
nugetDeps = ./deps.nix;
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"
rm -f $out/bin/{Microsoft,NUnit3,System}.* "$out/bin"/*Tests
'';
doInstallCheck = true;
installCheckPhase = ''
$out/bin/boogie ${./install-check-file.bpl}
'';
meta = with lib; {
description = "Intermediate verification language";
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 = licenses.mspl;
maintainers = [ maintainers.taktoa ];
platforms = with platforms; (linux ++ darwin);
};
}
|
