Merge pull request #22507 from layus/dafny-update
Add dafny; fixup Boogie
This commit is contained in:
commit
d099c1b96d
2 changed files with 53 additions and 3 deletions
|
@ -16986,6 +16986,8 @@ with pkgs;
|
|||
|
||||
### SCIENCE/PROGRAMMING
|
||||
|
||||
dafny = dotnetPackages.Dafny;
|
||||
|
||||
plm = callPackage ../applications/science/programming/plm { };
|
||||
|
||||
### SCIENCE/LOGIC
|
||||
|
@ -17000,6 +17002,8 @@ with pkgs;
|
|||
|
||||
aspino = callPackage ../applications/science/logic/aspino {};
|
||||
|
||||
boogie = dotnetPackages.Boogie;
|
||||
|
||||
coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
|
||||
make = pkgs.gnumake3;
|
||||
inherit (ocamlPackages_3_12_1) ocaml findlib;
|
||||
|
|
|
@ -221,8 +221,9 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
|
|||
# SOURCE PACKAGES
|
||||
|
||||
Boogie = buildDotnetPackage rec {
|
||||
baseName = "Boogie-unstable";
|
||||
baseName = "Boogie";
|
||||
version = "2017-01-03";
|
||||
name = "${baseName}-unstable-${version}";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "boogie-org";
|
||||
|
@ -238,8 +239,8 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
|
|||
outputFiles = [ "Binaries/*" ];
|
||||
|
||||
postInstall = ''
|
||||
mkdir -pv "$out/lib/dotnet/Boogie"
|
||||
ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/Boogie/z3.exe"
|
||||
mkdir -pv "$out/lib/dotnet/${baseName}"
|
||||
ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/${baseName}/z3.exe"
|
||||
'';
|
||||
|
||||
meta = with stdenv.lib; {
|
||||
|
@ -251,6 +252,51 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
|
|||
};
|
||||
};
|
||||
|
||||
Dafny = buildDotnetPackage rec {
|
||||
baseName = "Dafny";
|
||||
version = "1.9.8";
|
||||
|
||||
src = fetchurl {
|
||||
url = "https://github.com/Microsoft/dafny/archive/v${version}.tar.gz";
|
||||
sha256 = "0n4pk4cv7d2zsn4xmyjlxvpfl9avq79r06c7kzmrng24p3k4qj6s";
|
||||
};
|
||||
|
||||
preBuild = ''
|
||||
ln -s ${pkgs.z3} Binaries/z3
|
||||
'';
|
||||
|
||||
buildInputs = [ Boogie ];
|
||||
|
||||
xBuildFiles = [ "Source/Dafny.sln" ];
|
||||
xBuildFlags = [ ];
|
||||
|
||||
outputFiles = [ "Binaries/*" ];
|
||||
|
||||
# Do not wrap the z3 executable, only dafny-related ones.
|
||||
exeFiles = [ "Dafny*.exe" ];
|
||||
|
||||
# Dafny needs mono in its path.
|
||||
makeWrapperArgs = "--set PATH ${mono}/bin";
|
||||
|
||||
# Boogie as an input is not enough. Boogie libraries need to be at the same
|
||||
# place as Dafny ones. Same for "*.dll.mdb". No idea why or how to fix.
|
||||
postFixup = ''
|
||||
for lib in ${Boogie}/lib/dotnet/${Boogie.baseName}/*.dll{,.mdb}; do
|
||||
ln -s $lib $out/lib/dotnet/${baseName}/
|
||||
done
|
||||
# We generate our own executable scripts
|
||||
rm -f $out/lib/dotnet/${baseName}/dafny{,-server}
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "A programming language with built-in specification constructs";
|
||||
homepage = "http://research.microsoft.com/dafny";
|
||||
maintainers = with maintainers; [ layus ];
|
||||
license = licenses.MIT;
|
||||
platforms = with platforms; (linux ++ darwin);
|
||||
};
|
||||
};
|
||||
|
||||
Deedle = buildDotnetPackage rec {
|
||||
baseName = "Deedle";
|
||||
version = "1.2.0";
|
||||
|
|
Loading…
Reference in a new issue