pkgs/by-name/da/dafny/package.nix

   1 {
   2   lib,
   3   buildDotnetModule,
   4   fetchFromGitHub,
   5   runCommand,
   6   dafny,
   7   writeScript,
   8   jdk11,
   9   z3,
  10   dotnetCorePackages,
  11 }:
  12
  13 let
  14   examples = fetchFromGitHub {
  15     owner = "gaberch";
  16     repo = "Various-Algorithms-Verified-With-Dafny";
  17     rev = "50e451bbcd15e52e27d5bbbf66b0b4c4abbff41c";
  18     hash = "sha256-Ng5wve/4gQr/2hsFWUFFcTL3K2xH7dP9w8IrmvWMKyg=";
  19   };
  20
  21   tests = {
  22     verify = runCommand "dafny-test" { } ''
  23       mkdir $out
  24       cp ${examples}/SlowMax.dfy $out
  25       ${dafny}/bin/dafny verify --allow-warnings $out/SlowMax.dfy
  26     '';
  27
  28     # Broken, cannot compile generated .cs files for now
  29     #run = runCommand "dafny-test" { } ''
  30     #    mkdir $out
  31     #    cp ${examples}/SlowMax.dfy $out
  32     #    ${dafny}/bin/dafny run --allow-warnings $out/SlowMax.dfy
  33     #  '';
  34
  35     # TODO: Ensure then tests that dafny can generate to and compile other
  36     # languages (Java, Cpp, etc.)
  37   };
  38 in
  39 buildDotnetModule rec {
  40   pname = "Dafny";
  41   version = "4.9.1";
  42
  43   src = fetchFromGitHub {
  44     owner = "dafny-lang";
  45     repo = "dafny";
  46     tag = "v${version}";
  47     hash = "sha256-fCBaOF1mDrqJaUiATZAhzLjlK3NGVFnxdOwgHbOkkgY=";
  48   };
  49
  50   postPatch =
  51     let
  52       runtimeJarVersion = "4.9.1";
  53     in
  54     ''
  55       cp ${writeScript "fake-gradlew-for-dafny" ''
  56         mkdir -p build/libs/
  57         javac $(find -name "*.java" | grep "^./src/main") -d classes
  58         jar cf build/libs/DafnyRuntime-${runtimeJarVersion}.jar -C classes dafny
  59       ''} Source/DafnyRuntime/DafnyRuntimeJava/gradlew
  60
  61       # Needed to fix
  62       # "error NETSDK1129: The 'Publish' target is not supported without
  63       # specifying a target framework. The current project targets multiple
  64       # frameworks, you must specify the framework for the published
  65       # application."
  66       substituteInPlace Source/DafnyRuntime/DafnyRuntime.csproj \
  67         --replace-fail TargetFrameworks TargetFramework \
  68         --replace-fail "netstandard2.0;net452" net8.0
  69
  70       for f in Source/**/*.csproj ; do
  71         [[ "$f" == "Source/DafnyRuntime/DafnyRuntime.csproj" ]] && continue;
  72
  73         substituteInPlace $f \
  74           --replace-fail net6.0 net8.0
  75       done
  76     '';
  77
  78   dotnet-sdk = dotnetCorePackages.sdk_8_0;
  79   nativeBuildInputs = [ jdk11 ];
  80   nugetDeps = ./deps.json;
  81
  82   # Build just these projects. Building Source/Dafny.sln includes a bunch of
  83   # unnecessary components like tests.
  84   projectFile = [
  85     "Source/Dafny/Dafny.csproj"
  86     "Source/DafnyRuntime/DafnyRuntime.csproj"
  87     "Source/DafnyLanguageServer/DafnyLanguageServer.csproj"
  88   ];
  89
  90   executables = [ "Dafny" ];
  91
  92   # Help Dafny find z3
  93   makeWrapperArgs = [ "--prefix PATH : ${lib.makeBinPath [ z3 ]}" ];
  94
  95   postFixup = ''
  96     ln -s "$out/bin/Dafny" "$out/bin/dafny" || true
  97   '';
  98
  99   passthru.tests = tests;
 100
 101   meta = with lib; {
 102     description = "Programming language with built-in specification constructs";
 103     homepage = "https://research.microsoft.com/dafny";
 104     maintainers = with maintainers; [ layus ];
 105     license = licenses.mit;
 106     platforms = with platforms; (linux ++ darwin);
 107   };
 108 }