diff options
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic')
14 files changed, 66 insertions, 44 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/abc/default.nix b/nixpkgs/pkgs/applications/science/logic/abc/default.nix index fe73f4f4d6e2..60454ca9ce99 100644 --- a/nixpkgs/pkgs/applications/science/logic/abc/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/abc/default.nix @@ -4,13 +4,13 @@ stdenv.mkDerivation rec { pname = "abc-verifier"; - version = "2021.11.12"; + version = "2022.03.04"; src = fetchFromGitHub { owner = "yosyshq"; repo = "abc"; - rev = "f6fa2ddcfc89099726d60386befba874c7ac1e0d"; - hash = "sha256-0rvMPZ+kL0m/GjlCLx3eXYQ0osQ2wQiS3+csqPl3U9s="; + rev = "d7ecb23eeee9c9b4924182ce570c2e33eb18abff"; + hash = "sha256-aufWRTggJNOaUFsjh5+HFDqEur+nuM0hZSsTfGptbks="; }; nativeBuildInputs = [ cmake ]; diff --git a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix index 837f25e320f7..096a648b4ddf 100644 --- a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix @@ -12,36 +12,33 @@ let }; useDune2 = true; - - nativeBuildInputs = [ which ]; - in let alt-ergo-lib = ocamlPackages.buildDunePackage rec { pname = "alt-ergo-lib"; - inherit version src useDune2 nativeBuildInputs; + inherit version src useDune2; configureFlags = pname; + nativeBuildInputs = [ which ]; buildInputs = with ocamlPackages; [ dune-configurator ]; propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex stdlib-shims zarith ]; }; in let alt-ergo-parsers = ocamlPackages.buildDunePackage rec { pname = "alt-ergo-parsers"; - inherit version src useDune2 nativeBuildInputs; + inherit version src useDune2; configureFlags = pname; - buildInputs = with ocamlPackages; [ menhir ]; + nativeBuildInputs = [ which ocamlPackages.menhir ]; propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]); }; in ocamlPackages.buildDunePackage { - inherit pname version src useDune2 nativeBuildInputs; + inherit pname version src useDune2; configureFlags = pname; - buildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [ - cmdliner menhir ]) - ; + nativeBuildInputs = [ which ocamlPackages.menhir ]; + buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ]; meta = { description = "High-performance theorem prover and SMT solver"; diff --git a/nixpkgs/pkgs/applications/science/logic/anders/default.nix b/nixpkgs/pkgs/applications/science/logic/anders/default.nix index 72e412fc3bdc..bb60b2b8321a 100644 --- a/nixpkgs/pkgs/applications/science/logic/anders/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/anders/default.nix @@ -13,7 +13,10 @@ ocamlPackages.buildDunePackage rec { sha256 = "sha256-JUiZoo2rNLfgs94TlJqUNzul/7ODisCjSFAzhgSp1z4="; }; - buildInputs = with ocamlPackages; [ zarith menhir ]; + strictDeps = true; + + nativeBuildInputs = [ ocamlPackages.menhir ]; + buildInputs = [ ocamlPackages.zarith ]; meta = with lib; { description = "Modal Homotopy Type System"; diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix index bdd2796addcd..29959be2fa97 100644 --- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix @@ -69,7 +69,9 @@ let { case = range "8.7" "8.10"; out = ocamlPackages_4_09; } { case = range "8.5" "8.6"; out = ocamlPackages_4_05; } ] ocamlPackages_4_12; - ocamlBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] + ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] + ++ optional (versionAtLeast "8.14") ocamlPackages.dune_2; + ocamlBuildInputs = [] ++ optional (!versionAtLeast "8.10") ocamlPackages.camlp5 ++ optional (!versionAtLeast "8.13") ocamlPackages.num ++ optional (versionAtLeast "8.13") ocamlPackages.zarith; @@ -79,7 +81,7 @@ self = stdenv.mkDerivation { passthru = { inherit coq-version; - inherit ocamlPackages ocamlBuildInputs; + inherit ocamlPackages ocamlBuildInputs ocamlNativeBuildInputs; # For compatibility inherit (ocamlPackages) ocaml camlp5 findlib num ; emacsBufferSetup = pkgs: '' @@ -129,6 +131,7 @@ self = stdenv.mkDerivation { }; nativeBuildInputs = [ pkg-config ] + ++ ocamlNativeBuildInputs ++ optional buildIde copyDesktopItems ++ optional (buildIde && versionAtLeast "8.10") wrapGAppsHook ++ optional (!versionAtLeast "8.6") gnumake42; @@ -137,7 +140,6 @@ self = stdenv.mkDerivation { (if versionAtLeast "8.10" then [ ocamlPackages.lablgtk3-sourceview3 glib gnome.adwaita-icon-theme ] else [ ocamlPackages.lablgtk ]) - ++ optional (versionAtLeast "8.14") ocamlPackages.dune_2 ; postPatch = '' @@ -168,7 +170,7 @@ self = stdenv.mkDerivation { prefixKey = "-prefix "; - buildFlags = [ "revision" "coq" "coqide" ] ++ optional (!versionAtLeast "8.14") "bin/votour"; + buildFlags = [ "revision" "coq" ] ++ optional buildIde "coqide" ++ optional (!versionAtLeast "8.14") "bin/votour"; enableParallelBuilding = true; createFindlibDestdir = true; @@ -179,7 +181,7 @@ self = stdenv.mkDerivation { icon = "coq"; desktopName = "CoqIDE"; comment = "Graphical interface for the Coq proof assistant"; - categories = "Development;Science;Math;IDE;GTK"; + categories = [ "Development" "Science" "Math" "IDE" "GTK" ]; }); postInstall = let suffix = if versionAtLeast "8.14" then "-core" else ""; in '' diff --git a/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix index 0f0410024251..aaac288b615d 100644 --- a/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, fetchurl, coreutils, nettools, java, polyml, z3, veriT, vampire, eprover-ho, rlwrap, makeDesktopItem }: +{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, rlwrap, perl, makeDesktopItem }: # nettools needed for hostname stdenv.mkDerivation rec { @@ -77,6 +77,10 @@ stdenv.mkDerivation rec { substituteInPlace lib/Tools/env \ --replace /usr/bin/env ${coreutils}/bin/env + substituteInPlace src/Tools/Setup/src/Environment.java \ + --replace 'cmd.add("/usr/bin/env");' "" \ + --replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");" + rm -r heaps '' + (if ! stdenv.isLinux then "" else '' arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} @@ -90,6 +94,24 @@ stdenv.mkDerivation rec { buildPhase = '' export HOME=$TMP # The build fails if home is not set + setup_name=$(basename contrib/isabelle_setup*) + + #The following is adapted from https://isabelle.sketis.net/repos/isabelle/file/Isabelle2021-1/Admin/lib/Tools/build_setup + TARGET_DIR="contrib/$setup_name/lib" + rm -rf "$TARGET_DIR" + mkdir -p "$TARGET_DIR/isabelle/setup" + declare -a ARGS=("-Xlint:unchecked") + + SOURCES="$(${perl}/bin/perl -e 'while (<>) { if (m/(\S+\.java)/) { print "$1 "; } }' "src/Tools/Setup/etc/build.props")" + for SRC in $SOURCES + do + ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC" + done + ${java}/bin/javac -d "$TARGET_DIR" -classpath ${scala}/lib/scala-compiler.jar "''${ARGS[@]}" + ${java}/bin/jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle + rm -rf "$TARGET_DIR/isabelle" + + # Prebuild HOL Session bin/isabelle build -v -o system_heaps -b HOL ''; @@ -114,7 +136,7 @@ stdenv.mkDerivation rec { icon = "isabelle"; desktopName = "Isabelle"; comment = meta.description; - categories = "Education;Science;Math;"; + categories = [ "Education" "Science" "Math" ]; }; meta = with lib; { diff --git a/nixpkgs/pkgs/applications/science/logic/key/default.nix b/nixpkgs/pkgs/applications/science/logic/key/default.nix index 762acbe4ec44..85a7ecb08c39 100644 --- a/nixpkgs/pkgs/applications/science/logic/key/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/key/default.nix @@ -61,7 +61,7 @@ in stdenv.mkDerivation rec { comment = meta.description; desktopName = "KeY"; genericName = "KeY"; - categories = "Science;"; + categories = [ "Science" ]; }) ]; diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix index 22e755bd852e..1eea97a0fd23 100644 --- a/nixpkgs/pkgs/applications/science/logic/lean/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -2,7 +2,7 @@ stdenv.mkDerivation rec { pname = "lean"; - version = "3.39.2"; + version = "3.41.0"; src = fetchFromGitHub { owner = "leanprover-community"; @@ -11,8 +11,8 @@ stdenv.mkDerivation rec { # from. this is then used to check whether an olean file should be # rebuilt. don't use a tag as rev because this will get replaced into # src/githash.h.in in preConfigure. - rev = "402f41cdedbd46a368fb7807bebe83550d887631"; - sha256 = "0jddakr07ixspw19xblpj1882vxxaljg3fflhn4myvigwzkav334"; + rev = "154ac72f4ff674bc4486ac611f926a3d6b999f9f"; + sha256 = "0mpxlfjq460x1vi3v6qzgjv74asg0qlhykd51pj347795x5b1hf1"; }; nativeBuildInputs = [ cmake ]; diff --git a/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix index 688c8c319bd8..67e699bc63fa 100644 --- a/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix @@ -20,7 +20,7 @@ stdenv.mkDerivation rec { exec = "logisim-evolution"; icon = "logisim-evolution"; comment = meta.description; - categories = "Education;"; + categories = [ "Education" ]; }) ]; diff --git a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix index b4741aaed86e..06dc024e6d23 100644 --- a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix @@ -20,7 +20,7 @@ stdenv.mkDerivation rec { exec = "logisim"; icon = "logisim"; comment = meta.description; - categories = "Education;"; + categories = [ "Education" ]; }) ]; diff --git a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix index e701fb2711f0..ef6f9b157d2f 100644 --- a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix @@ -6,13 +6,13 @@ stdenv.mkDerivation rec { pname = "opensmt"; - version = "2.2.0"; + version = "2.3.0"; src = fetchFromGitHub { owner = "usi-verification-and-security"; repo = "opensmt"; rev = "v${version}"; - sha256 = "sha256-6VkBGDzqG3mplpvFh5DIR0I1I2/J0Pi7xYk/yVn04Kg="; + sha256 = "sha256-5Gw9+J+3LHNUNbcHxsQR/ivWndL2P7yBt/Q35fBMg58="; }; nativeBuildInputs = [ cmake bison flex ]; diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix index 90a4aeb4f8ab..14b3055ab36b 100644 --- a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -11,10 +11,10 @@ stdenv.mkDerivation rec { pname = "tlaps"; - version = "1.4.3"; + version = "1.4.5"; src = fetchurl { - url = "https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-${version}.tar.gz"; - sha256 = "1w5z3ns5xxmhmp8r4x2kjmy3clqam935gmvx82imyxrr1bamx6gf"; + url = "https://tla.msr-inria.inria.fr/tlaps/dist/${version}/tlaps-${version}.tar.gz"; + sha256 = "c296998acd14d5b93a8d5be7ee178007ef179957465966576bda26944b1b7fca"; }; buildInputs = [ ocaml isabelle cvc3 perl wget which ]; @@ -52,7 +52,7 @@ stdenv.mkDerivation rec { homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html"; license = lib.licenses.bsd2; platforms = lib.platforms.unix; - maintainers = [ ]; + maintainers = with lib.maintainers; [ florentc ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix index 21c60d03ac1e..7b1ee4384c9e 100644 --- a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -18,10 +18,8 @@ let comment = "IDE for TLA+"; desktopName = name; genericName = comment; - categories = "Development"; - extraEntries = '' - StartupWMClass=TLA+ Toolbox - ''; + categories = [ "Development" ]; + startupWMClass = "TLA+ Toolbox"; }; diff --git a/nixpkgs/pkgs/applications/science/logic/why3/default.nix b/nixpkgs/pkgs/applications/science/logic/why3/default.nix index 78631486554a..0f3dab8038ee 100644 --- a/nixpkgs/pkgs/applications/science/logic/why3/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/why3/default.nix @@ -3,15 +3,15 @@ stdenv.mkDerivation rec { pname = "why3"; - version = "1.4.0"; + version = "1.4.1"; src = fetchurl { - url = "https://gforge.inria.fr/frs/download.php/file/38425/why3-${version}.tar.gz"; - sha256 = "0lw0cpx347zz9vvwqibmbxgs80fsd16scgk3isscvwxnajpc3rv8"; + url = "https://why3.gitlabpages.inria.fr/releases/${pname}-${version}.tar.gz"; + sha256 = "sha256:1rqyypzlvagrn43ykl0c5wxyvnry5fl1ykn3xcvlzgghk96yq3jq"; }; buildInputs = with ocamlPackages; [ - ocaml findlib ocamlgraph zarith menhir menhirLib + ocaml findlib ocamlgraph zarith menhir # Emacs compilation of why3.el emacs # Documentation @@ -26,7 +26,7 @@ stdenv.mkDerivation rec { coqPackages.coq coqPackages.flocq ]; - propagatedBuildInputs = with ocamlPackages; [ camlzip num re sexplib ]; + propagatedBuildInputs = with ocamlPackages; [ camlzip menhirLib num re sexplib ]; enableParallelBuilding = true; diff --git a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix index 2829cb59340b..0c20faceb54e 100644 --- a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "workcraft"; - version = "3.3.5"; + version = "3.3.6"; src = fetchurl { url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz"; - sha256 = "sha256-KErKYK3mmjp5uNdGQnjzUUIEwXT5fqbAPUunH72Mtig="; + sha256 = "sha256-5J4HOTz92ALUcZZr15jJ6vplc3KDwbFCXqjEhlOV4kE="; }; nativeBuildInputs = [ makeWrapper ]; |