From b0d00352bbd47f347a4997a8d61f8956607710ae Mon Sep 17 00:00:00 2001 From: mdarocha Date: Sat, 16 Sep 2023 00:18:14 +0200 Subject: [PATCH 1/2] boogie: move out of dotnet-packages.nix dotnet-packages.nix is deprecated and being removed --- .../bo/boogie/deps.nix} | 0 pkgs/by-name/bo/boogie/package.nix | 49 ++++++++++++++++++ pkgs/top-level/all-packages.nix | 2 - pkgs/top-level/dotnet-packages.nix | 51 ++----------------- 4 files changed, 53 insertions(+), 49 deletions(-) rename pkgs/{development/dotnet-modules/boogie-deps.nix => by-name/bo/boogie/deps.nix} (100%) create mode 100644 pkgs/by-name/bo/boogie/package.nix diff --git a/pkgs/development/dotnet-modules/boogie-deps.nix b/pkgs/by-name/bo/boogie/deps.nix similarity index 100% rename from pkgs/development/dotnet-modules/boogie-deps.nix rename to pkgs/by-name/bo/boogie/deps.nix diff --git a/pkgs/by-name/bo/boogie/package.nix b/pkgs/by-name/bo/boogie/package.nix new file mode 100644 index 000000000000..8f15c0631256 --- /dev/null +++ b/pkgs/by-name/bo/boogie/package.nix @@ -0,0 +1,49 @@ +{ lib, buildDotnetModule, fetchFromGitHub, z3 }: + +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 = ./deps.nix; + + postInstall = '' + mkdir -pv "$out/lib/dotnet/${pname}" + ln -sv "${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); + }; +} + diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 929cdaf3ab50..d9ea09940bd8 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -39695,8 +39695,6 @@ with pkgs; beluga = callPackage ../applications/science/logic/beluga { }; - boogie = dotnetPackages.Boogie; - cbmc = callPackage ../applications/science/logic/cbmc { }; cadical = callPackage ../applications/science/logic/cadical { }; diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix index 5445b9cbcb49..661603b2ba1f 100644 --- a/pkgs/top-level/dotnet-packages.nix +++ b/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"; From 7006d97373cbaf64e522dd2673c6c2220ebf81a9 Mon Sep 17 00:00:00 2001 From: mdarocha Date: Sat, 16 Sep 2023 00:25:31 +0200 Subject: [PATCH 2/2] boogie: 2.15.7 -> 3.0.4 Also add install check to verify all dependencies (ie. z3) work --- pkgs/by-name/bo/boogie/install-check-file.bpl | 61 +++++++++++++++++++ pkgs/by-name/bo/boogie/package.nix | 18 ++++-- 2 files changed, 74 insertions(+), 5 deletions(-) create mode 100644 pkgs/by-name/bo/boogie/install-check-file.bpl diff --git a/pkgs/by-name/bo/boogie/install-check-file.bpl b/pkgs/by-name/bo/boogie/install-check-file.bpl new file mode 100644 index 000000000000..8548c612d06e --- /dev/null +++ b/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; +} diff --git a/pkgs/by-name/bo/boogie/package.nix b/pkgs/by-name/bo/boogie/package.nix index 8f15c0631256..44811a33b637 100644 --- a/pkgs/by-name/bo/boogie/package.nix +++ b/pkgs/by-name/bo/boogie/package.nix @@ -2,22 +2,25 @@ buildDotnetModule rec { pname = "Boogie"; - version = "2.15.7"; + version = "3.0.4"; src = fetchFromGitHub { owner = "boogie-org"; repo = "boogie"; rev = "v${version}"; - sha256 = "16kdvkbx2zwj7m43cra12vhczbpj23wyrdnj0ygxf7np7c2aassp"; + sha256 = "sha256-yebThnIOpZ5crYsSZtbDj8Gn6DznTNJ4T/TsFR3gWvs="; }; projectFile = [ "Source/Boogie.sln" ]; nugetDeps = ./deps.nix; - postInstall = '' - mkdir -pv "$out/lib/dotnet/${pname}" - ln -sv "${z3}/bin/z3" "$out/lib/dotnet/${pname}/z3.exe" + 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 @@ -32,6 +35,11 @@ buildDotnetModule rec { 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";