Merge pull request #255378 from mdarocha/move-boogie

boogie: 2.15.7 -> 3.0.4, move out of `dotnet-packages.nix`

pkgs/by-name/bo/boogie/install-check-file.bpl

@@ -0,0 +1,61 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+
+function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} mapconstint(int) : [X]int;
+function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;
+function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;
+function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;
+
+
+
+const FF: [X]bool;
+axiom FF == mapconstbool(false);
+
+const TT: [X]bool;
+axiom TT == mapconstbool(true);
+
+const MultisetEmpty: [X]int;
+axiom MultisetEmpty == mapconstint(0);
+
+function {:inline} MultisetSingleton(x: X) : [X]int
+{
+  MultisetEmpty[x := 1]
+}
+
+function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int
+{
+  mapadd(a, b)
+}
+
+function {:inline} MultisetMinus(a: [X]int, b: [X]int)  : [X]int
+{
+  mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))
+}
+
+procedure foo() {
+  var x: X;
+
+  assert FF != TT;
+  assert mapnot(FF) == TT;
+
+  assert MultisetSingleton(x) != MultisetEmpty;
+  assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);
+  assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;
+  assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;
+}

pkgs/by-name/bo/boogie/package.nix

@@ -0,0 +1,57 @@
+{ lib, buildDotnetModule, fetchFromGitHub, z3 }:
+
+buildDotnetModule rec {
+  pname = "Boogie";
+  version = "3.0.4";
+
+  src = fetchFromGitHub {
+    owner = "boogie-org";
+    repo = "boogie";
+    rev = "v${version}";
+    sha256 = "sha256-yebThnIOpZ5crYsSZtbDj8Gn6DznTNJ4T/TsFR3gWvs=";
+  };
+
+  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 = "An 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);
+  };
+}
+

pkgs/top-level/all-packages.nix

@@ -39693,8 +39693,6 @@ with pkgs;
 
   beluga = callPackage ../applications/science/logic/beluga { };
 
-  boogie = dotnetPackages.Boogie;
-
   cbmc = callPackage ../applications/science/logic/cbmc { };
 
   cadical = callPackage ../applications/science/logic/cadical { };

pkgs/top-level/dotnet-packages.nix

@@ -9,9 +9,13 @@
 , glib
 , mono
 , overrides ? {}
+, boogie
 }:
 
 let self = dotnetPackages // overrides; dotnetPackages = with self; {
+  # ALIASES FOR MOVED PACKAGES
+
+  Boogie = boogie;
 
   # BINARY PACKAGES
 
@@ -125,53 +129,6 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
 
   # SOURCE PACKAGES
 
-  Boogie = buildDotnetModule rec {
-    pname = "Boogie";
-    version = "2.15.7";
-
-    src = fetchFromGitHub {
-      owner = "boogie-org";
-      repo = "boogie";
-      rev = "v${version}";
-      sha256 = "16kdvkbx2zwj7m43cra12vhczbpj23wyrdnj0ygxf7np7c2aassp";
-    };
-
-    projectFile = [ "Source/Boogie.sln" ];
-    nugetDeps = ../development/dotnet-modules/boogie-deps.nix;
-
-    postInstall = ''
-        mkdir -pv "$out/lib/dotnet/${pname}"
-        ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/${pname}/z3.exe"
-
-        # 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
-    '';
-
-    meta = with lib; {
-      description = "An 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);
-    };
-  };
-
   MonoAddins = buildDotnetPackage rec {
     pname = "Mono.Addins";
     version = "1.2";