summary refs log tree commit diff
path: root/pkgs/applications/science/logic
diff options
context:
space:
mode:
authorAlyssa Ross <hi@alyssa.is>2020-03-26 17:17:48 +0000
committerAlyssa Ross <hi@alyssa.is>2020-03-26 17:36:07 +0000
commit70e58881128ed8170821840138ab08fc5cdd3c11 (patch)
tree1bf0d3d977878df5b58493ea02b2e6c79df3ba22 /pkgs/applications/science/logic
parenta9847c36e6aa003998c1ef5518e5710658ca5770 (diff)
parent90dcc3360327e250536eeeca7fe9d887c9f7a817 (diff)
downloadnixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.tar
nixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.tar.gz
nixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.tar.bz2
nixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.tar.lz
nixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.tar.xz
nixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.tar.zst
nixpkgs-70e58881128ed8170821840138ab08fc5cdd3c11.zip
Merge remote-tracking branch 'nixpkgs/master' into master
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r--pkgs/applications/science/logic/abc/default.nix39
-rw-r--r--pkgs/applications/science/logic/acgtk/default.nix11
-rw-r--r--pkgs/applications/science/logic/alt-ergo/default.nix44
-rw-r--r--pkgs/applications/science/logic/elan/default.nix8
-rw-r--r--pkgs/applications/science/logic/hol_light/default.nix7
-rw-r--r--pkgs/applications/science/logic/lean/default.nix7
-rw-r--r--pkgs/applications/science/logic/mcy/default.nix44
-rw-r--r--pkgs/applications/science/logic/monosat/default.nix24
-rw-r--r--pkgs/applications/science/logic/potassco/clingcon.nix43
-rw-r--r--pkgs/applications/science/logic/satallax/default.nix5
-rw-r--r--pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch21
-rw-r--r--pkgs/applications/science/logic/symbiyosys/default.nix42
-rw-r--r--pkgs/applications/science/logic/why3/default.nix10
-rw-r--r--pkgs/applications/science/logic/workcraft/default.nix6
14 files changed, 239 insertions, 72 deletions
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix
index 8551a3ee4ca..a33cc92c7ce 100644
--- a/pkgs/applications/science/logic/abc/default.nix
+++ b/pkgs/applications/science/logic/abc/default.nix
@@ -1,35 +1,32 @@
-{ fetchFromGitHub, stdenv, readline, cmake }:
+{ stdenv, fetchFromGitHub
+, readline, cmake
+}:
 
-let
-  rev = "71f2b40320127561175ad60f6f2428f3438e5243";
-in stdenv.mkDerivation {
-  pname = "abc-verifier";
-  version = "2020-01-11";
+stdenv.mkDerivation rec {
+  pname   = "abc-verifier";
+  version = "2020.03.05";
 
   src = fetchFromGitHub {
-    inherit rev;
-    owner = "berkeley-abc";
-    repo = "abc";
-    sha256 = "15sn146ajxql7l1h8rsag5lhn4spwvgjhwzqawfr78snzadw8by3";
+    owner  = "berkeley-abc";
+    repo   = "abc";
+    rev    = "ed90ce20df9c7c4d6e1db5d3f786f9b52e06bab1";
+    sha256 = "01sw67pkrb6wzflkxbkxzwsnli3nvp0yxwp3j1ngb3c0j86ri437";
   };
 
-  passthru.rev = rev;
-
   nativeBuildInputs = [ cmake ];
   buildInputs = [ readline ];
 
   enableParallelBuilding = true;
+  installPhase = "mkdir -p $out/bin && mv abc $out/bin";
 
-  installPhase = ''
-    mkdir -p $out/bin
-    mv abc $out/bin
-  '';
+  # needed by yosys
+  passthru.rev = src.rev;
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "A tool for squential logic synthesis and formal verification";
-    homepage    = https://people.eecs.berkeley.edu/~alanmi/abc;
-    license     = stdenv.lib.licenses.mit;
-    platforms   = stdenv.lib.platforms.unix;
-    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+    homepage    = "https://people.eecs.berkeley.edu/~alanmi/abc";
+    license     = licenses.mit;
+    platforms   = platforms.unix;
+    maintainers = with maintainers; [ thoughtpolice ];
   };
 }
diff --git a/pkgs/applications/science/logic/acgtk/default.nix b/pkgs/applications/science/logic/acgtk/default.nix
index 729aef4e21c..b7dc9571247 100644
--- a/pkgs/applications/science/logic/acgtk/default.nix
+++ b/pkgs/applications/science/logic/acgtk/default.nix
@@ -2,15 +2,16 @@
 
 stdenv.mkDerivation {
 
-  name = "acgtk-1.5.0";
+  pname = "acgtk";
+  version = "1.5.1";
 
   src = fetchurl {
-    url = http://calligramme.loria.fr/acg/software/acg-1.5.0-20181019.tar.gz;
-    sha256 = "14n003gxzw5w79hlpw1ja4nq97jqf9zqyg00ihvpxw4bv9jlm8jm";
+    url = https://acg.loria.fr/software/acg-1.5.1-20191113.tar.gz;
+    sha256 = "17595qfwhzz5q091ak6i6bg5wlppbn8zfn58x3hmmmjvx2yfajn1";
   };
 
   buildInputs = [ dune ] ++ (with ocamlPackages; [
-    ocaml findlib ansiterminal cairo2 fmt logs menhir mtime ocf
+    ocaml findlib ansiterminal cairo2 cmdliner fmt logs menhir mtime yojson
   ]);
 
   buildPhase = "dune build";
@@ -18,7 +19,7 @@ stdenv.mkDerivation {
   inherit (dune) installPhase;
 
   meta = with stdenv.lib; {
-    homepage = http://calligramme.loria.fr/acg/;
+    homepage = https://acg.loria.fr/;
     description = "A toolkit for developing ACG signatures and lexicon";
     license = licenses.cecill20;
     inherit (ocamlPackages.ocaml.meta) platforms;
diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix
index f83480cfbaf..ad931c23d53 100644
--- a/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -1,26 +1,48 @@
-{ fetchurl, stdenv, which, dune, ocamlPackages }:
+{ fetchurl, lib, which, ocamlPackages }:
 
-stdenv.mkDerivation rec {
+let
   pname = "alt-ergo";
-  version = "2.3.0";
+  version = "2.3.1";
 
   src = fetchurl {
     url    = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${pname}-${version}.tar.gz";
     name   = "${pname}-${version}.tar.gz";
-    sha256 = "1ycr3ff0gacq1aqzs16n6swgfniwpim0m7rvhcam64kj0a80c6bz";
+    sha256 = "124n836alqm13245hcnxixzc6a15rip919shfflvxqnl617mkmhg";
   };
 
-  buildInputs = [ dune which ] ++ (with ocamlPackages; [
-    ocaml findlib camlzip lablgtk menhir num ocplib-simplex psmt2-frontend seq zarith
-  ]);
-
   preConfigure = "patchShebangs ./configure";
 
+  nativeBuildInputs = [ which ];
+
+in
+
+let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-lib";
+  inherit version src preConfigure nativeBuildInputs;
+  configureFlags = pname;
+  propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex zarith ];
+}; in
+
+let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-parsers";
+  inherit version src preConfigure nativeBuildInputs;
+  configureFlags = pname;
+  buildInputs = with ocamlPackages; [ menhir ];
+  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+}; in
+
+ocamlPackages.buildDunePackage {
+
+  inherit pname version src preConfigure nativeBuildInputs;
+
+  configureFlags = pname;
+
+  buildInputs = [ alt-ergo-parsers ocamlPackages.menhir ];
+
   meta = {
     description = "High-performance theorem prover and SMT solver";
     homepage    = "https://alt-ergo.ocamlpro.com/";
-    license     = stdenv.lib.licenses.ocamlpro_nc;
-    platforms   = stdenv.lib.platforms.linux ++ stdenv.lib.platforms.darwin;
-    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+    license     = lib.licenses.ocamlpro_nc;
+    maintainers = [ lib.maintainers.thoughtpolice ];
   };
 }
diff --git a/pkgs/applications/science/logic/elan/default.nix b/pkgs/applications/science/logic/elan/default.nix
index b77f5110521..ea3b0585099 100644
--- a/pkgs/applications/science/logic/elan/default.nix
+++ b/pkgs/applications/science/logic/elan/default.nix
@@ -2,16 +2,16 @@
 
 rustPlatform.buildRustPackage rec {
   pname = "elan";
-  version = "0.7.5";
+  version = "0.8.0";
 
   src = fetchFromGitHub {
     owner = "kha";
     repo = "elan";
     rev = "v${version}";
-    sha256 = "1147f3lzr6lgvf580ppspn20bdwnf6l8idh1h5ana0p0lf5a0dn1";
+    sha256 = "0n2ncssjcmp3x5kbnci7xbq5fgcihlr3vaglyhhwzrxkjy2vpmpd";
   };
 
-  cargoSha256 = "0vja1cq6z7jlr4nzfdzn4gl8l31yld82zmgzwihnalif13q3fcps";
+  cargoSha256 = "1pkg0n7kxckr0zhr8dr12b9fxg5q185kj3r9k2rmnkj2dpa2mxh3";
 
   nativeBuildInputs = [ pkgconfig ];
 
@@ -22,7 +22,7 @@ rustPlatform.buildRustPackage rec {
   postInstall = ''
     pushd $out/bin
     mv elan-init elan
-    for link in lean leanpkg leanchecker; do
+    for link in lean leanpkg leanchecker leanc; do
       ln -s elan $link
     done
     popd
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index d799b52d115..69ffb87e767 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, runtimeShell, fetchFromGitHub, ocaml, num, camlp5 }:
+{ stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, num, camlp5 }:
 
 let
   load_num =
@@ -30,6 +30,11 @@ stdenv.mkDerivation {
     sha256 = "0sxsk8z08ba0q5aixdyczcx5l29lb51ba4ip3d2fry7y604kjsx6";
   };
 
+  patches = [(fetchpatch {
+    url = https://salsa.debian.org/ocaml-team/hol-light/-/raw/master/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch;
+    sha256 = "180qmxbrk3vb1ix7j77hcs8vsar91rs11s5mm8ir5352rz7ylicr";
+  })];
+
   buildInputs = [ ocaml camlp5 ];
   propagatedBuildInputs = [ num ];
 
diff --git a/pkgs/applications/science/logic/lean/default.nix b/pkgs/applications/science/logic/lean/default.nix
index 726bac5c50e..cfd645a3c73 100644
--- a/pkgs/applications/science/logic/lean/default.nix
+++ b/pkgs/applications/science/logic/lean/default.nix
@@ -2,13 +2,13 @@
 
 stdenv.mkDerivation rec {
   pname = "lean";
-  version = "3.5.1";
+  version = "3.7.2";
 
   src = fetchFromGitHub {
     owner  = "leanprover-community";
     repo   = "lean";
     rev    = "v${version}";
-    sha256 = "0m7knf1hfbn2v6p6kmqxlx8c40p5nzv8d975w2xwljaccc42j1yp";
+    sha256 = "0d9lz0mbxyaaykkvk2p8w2hcif9cx0ksihgh7qhxf417bz6msgc1";
   };
 
   nativeBuildInputs = [ cmake ];
@@ -21,7 +21,8 @@ stdenv.mkDerivation rec {
 
   meta = with stdenv.lib; {
     description = "Automatic and interactive theorem prover";
-    homepage    = https://leanprover.github.io/;
+    homepage    = "https://leanprover.github.io/";
+    changelog   = "https://github.com/leanprover-community/lean/blob/v${version}/doc/changes.md";
     license     = licenses.asl20;
     platforms   = platforms.unix;
     maintainers = with maintainers; [ thoughtpolice gebner ];
diff --git a/pkgs/applications/science/logic/mcy/default.nix b/pkgs/applications/science/logic/mcy/default.nix
new file mode 100644
index 00000000000..a9366d56058
--- /dev/null
+++ b/pkgs/applications/science/logic/mcy/default.nix
@@ -0,0 +1,44 @@
+{ stdenv, fetchFromGitHub
+, yosys, symbiyosys, python3
+}:
+
+let
+  python = python3.withPackages (p: with p; [ flask ]);
+in
+stdenv.mkDerivation {
+  pname = "mcy";
+  version = "2020.03.21";
+
+  src = fetchFromGitHub {
+    owner  = "YosysHQ";
+    repo   = "mcy";
+    rev    = "bac92b8aad9bf24714fda70d3750bb50d6d96177";
+    sha256 = "0mmg6zd5cbn8g0am9c3naamg0lq67yyy117fzn2ydigcyia7vmnp";
+  };
+
+  buildInputs = [ python ];
+  patchPhase = ''
+    substituteInPlace mcy.py \
+      --replace yosys '${yosys}/bin/yosys' \
+      --replace 'os.execvp("mcy-dash"' "os.execvp(\"$out/bin/mcy-dash\""
+    substituteInPlace mcy-dash.py \
+      --replace 'app.run(debug=True)' 'app.run(host="0.0.0.0",debug=True)'
+  '';
+
+  # the build needs a bit of work...
+  buildPhase = "true";
+  installPhase = ''
+    mkdir -p $out/bin $out/share/mcy/dash
+    install mcy.py      $out/bin/mcy      && chmod +x $out/bin/mcy
+    install mcy-dash.py $out/bin/mcy-dash && chmod +x $out/bin/mcy-dash
+    cp -r dash/. $out/share/mcy/dash/.
+  '';
+
+  meta = {
+    description = "Mutation-based coverage testing for hardware designs, with Yosys";
+    homepage    = "https://github.com/YosysHQ/mcy";
+    license     = stdenv.lib.licenses.isc;
+    maintainers = with stdenv.lib.maintainers; [ thoughtpolice ];
+    platforms   = stdenv.lib.platforms.all;
+  };
+}
diff --git a/pkgs/applications/science/logic/monosat/default.nix b/pkgs/applications/science/logic/monosat/default.nix
index c0512b74488..ba0e787af72 100644
--- a/pkgs/applications/science/logic/monosat/default.nix
+++ b/pkgs/applications/science/logic/monosat/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, cmake, zlib, gmp, jdk8,
+{ stdenv, fetchpatch, fetchFromGitHub, cmake, zlib, gmp, jdk8,
   # The JDK we use on Darwin currenly makes extensive use of rpaths which are
   # annoying and break the python library, so let's not bother for now
   includeJava ? !stdenv.hostPlatform.isDarwin, includeGplCode ? true }:
@@ -20,9 +20,17 @@ let
     inherit rev sha256;
   };
 
+  patches = [
+    # Python 3.8 compatibility
+    (fetchpatch {
+      url = https://github.com/sambayless/monosat/commit/a5079711d0df0451f9840f3a41248e56dbb03967.patch;
+      sha256 = "1p2y0jw8hb9c90nbffhn86k1dxd6f6hk5v70dfmpzka3y6g1ksal";
+    })
+  ];
+
   core = stdenv.mkDerivation {
     name = "${pname}-${version}";
-    inherit src;
+    inherit src patches;
     buildInputs = [ cmake zlib gmp jdk8 ];
 
     cmakeFlags = [
@@ -48,20 +56,22 @@ let
   };
 
   python = { buildPythonPackage, cython }: buildPythonPackage {
-    inherit pname version src;
-
-    # The top-level "source" is what fetchFromGitHub gives us. The rest is inside the repo
-    sourceRoot = "source/src/monosat/api/python/";
+    inherit pname version src patches;
 
     propagatedBuildInputs = [ core cython ];
 
     # This tells setup.py to use cython, which should produce faster bindings
     MONOSAT_CYTHON = true;
 
+    # After patching src, move to where the actually relevant source is. This could just be made
+    # the sourceRoot if it weren't for the patch.
+    postPatch = ''
+      cd src/monosat/api/python
+    '' +
     # The relative paths here don't make sense for our Nix build
     # TODO: do we want to just reference the core monosat library rather than copying the
     # shared lib? The current setup.py copies the .dylib/.so...
-    postPatch = ''
+    ''
       substituteInPlace setup.py \
         --replace 'library_dir = "../../../../"' 'library_dir = "${core}/lib/"'
     '';
diff --git a/pkgs/applications/science/logic/potassco/clingcon.nix b/pkgs/applications/science/logic/potassco/clingcon.nix
new file mode 100644
index 00000000000..1203822d86e
--- /dev/null
+++ b/pkgs/applications/science/logic/potassco/clingcon.nix
@@ -0,0 +1,43 @@
+{ stdenv
+, fetchFromGitHub
+, cmake
+, bison
+, re2c
+}:
+
+stdenv.mkDerivation rec {
+  pname = "clingcon";
+  version = "3.3.0";
+
+  src = fetchFromGitHub {
+    owner = "potassco";
+    repo = "${pname}";
+    rev = "v${version}";
+    fetchSubmodules = true;
+    sha256 = "1q7517h10jfvjdk2czq8d6y57r8kr1j1jj2k2ip2qxkpyfigk4rs";
+   };
+
+  # deal with clingcon through git submodules recursively importing
+  # an outdated version of libpotassco which uses deprecated <xlocale.h> header in .cpp files
+  postPatch = ''
+    find ./ -type f -exec sed -i 's/<xlocale.h>/<locale.h>/g' {} \;
+  '';
+
+  nativeBuildInputs = [ cmake bison re2c ];
+
+  cmakeFlags = [
+    "-DCLINGCON_MANAGE_RPATH=ON"
+    "-DCLINGO_BUILD_WITH_PYTHON=OFF"
+    "-DCLINGO_BUILD_WITH_LUA=OFF"
+  ];
+
+  meta = {
+    inherit version;
+    description = "Extension of clingo to handle constraints over integers";
+    license = stdenv.lib.licenses.gpl3; # for now GPL3, next version MIT!
+    platforms = stdenv.lib.platforms.unix;
+    homepage = "https://potassco.org/";
+    downloadPage = "https://github.com/potassco/clingcon/releases/";
+    changelog = "https://github.com/potassco/clingcon/releases/tag/v${version}";
+  };
+}
diff --git a/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix
index 7249eb991d3..d3ceeadbf9a 100644
--- a/pkgs/applications/science/logic/satallax/default.nix
+++ b/pkgs/applications/science/logic/satallax/default.nix
@@ -9,6 +9,11 @@ stdenv.mkDerivation rec {
     sha256 = "1kvxn8mc35igk4vigi5cp7w3wpxk2z3bgwllfm4n3h2jfs0vkpib";
   };
 
+  patches = [
+    # GCC9 doesn't allow default value in friend declaration.
+    ./fix-declaration-gcc9.patch
+  ];
+
   preConfigure = ''
     mkdir fake-tools
     echo "echo 'Nix-build-host.localdomain'" > fake-tools/hostname
diff --git a/pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch b/pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch
new file mode 100644
index 00000000000..1933fc25c4d
--- /dev/null
+++ b/pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch
@@ -0,0 +1,21 @@
+diff --git i/minisat/core/SolverTypes.h w/minisat/core/SolverTypes.h
+--- i/minisat/core/SolverTypes.h
++++ w/minisat/core/SolverTypes.h
+@@ -47,7 +47,7 @@ struct Lit {
+     int     x;
+ 
+     // Use this as a constructor:
+-    friend Lit mkLit(Var var, bool sign = false);
++    friend Lit mkLit(Var var, bool sign);
+ 
+     bool operator == (Lit p) const { return x == p.x; }
+     bool operator != (Lit p) const { return x != p.x; }
+@@ -55,7 +55,7 @@ struct Lit {
+ };
+ 
+ 
+-inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
++inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
+ inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
+ inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+ inline  bool sign      (Lit p)              { return p.x & 1; }
diff --git a/pkgs/applications/science/logic/symbiyosys/default.nix b/pkgs/applications/science/logic/symbiyosys/default.nix
index d6ff7a8b4a7..b180cf307f0 100644
--- a/pkgs/applications/science/logic/symbiyosys/default.nix
+++ b/pkgs/applications/science/logic/symbiyosys/default.nix
@@ -1,19 +1,37 @@
-{ stdenv, fetchFromGitHub, yosys, bash, python3, yices }:
+{ stdenv, fetchFromGitHub
+, bash, python3, yosys
+, yices, boolector, aiger
+}:
 
 stdenv.mkDerivation {
   pname = "symbiyosys";
-  version = "2020.02.08";
+  version = "2020.03.24";
 
   src = fetchFromGitHub {
     owner  = "YosysHQ";
     repo   = "SymbiYosys";
-    rev    = "500b526131f434b9679732fc89515dbed67c8d7d";
-    sha256 = "1pwbirszc80r288x81nx032snniqgmc80i09bbha2i3zd0c3pj5h";
+    rev    = "8a62780b9df4d2584e41cdd42cab92fddcd75b31";
+    sha256 = "0ss5mrzwff2dny8kfciqbrz67m6k52yvc1shd7gk3qb99x7g7fp8";
   };
 
-  buildInputs = [ python3 yosys ];
+  buildInputs = [ python3 ];
+  patchPhase = ''
+    patchShebangs .
 
-  propagatedBuildInputs = [ yices ];
+    # Fix up Yosys imports
+    substituteInPlace sbysrc/sby.py \
+      --replace "##yosys-sys-path##" \
+                "sys.path += [p + \"/share/yosys/python3/\" for p in [\"$out\", \"${yosys}\"]]"
+
+    # Fix various executable references
+    substituteInPlace sbysrc/sby_core.py \
+      --replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"' \
+      --replace ': "btormc"'       ': "${boolector}/bin/btormc"' \
+      --replace ': "yosys"'        ': "${yosys}/bin/yosys"' \
+      --replace ': "yosys-smtbmc"' ': "${yosys}/bin/yosys-smtbmc"' \
+      --replace ': "yosys-abc"'    ': "${yosys}/bin/yosys-abc"' \
+      --replace ': "aigbmc"'       ': "${aiger}/bin/aigbmc"' \
+  '';
 
   buildPhase = "true";
   installPhase = ''
@@ -21,19 +39,13 @@ stdenv.mkDerivation {
 
     cp sbysrc/sby_*.py $out/share/yosys/python3/
     cp sbysrc/sby.py $out/bin/sby
-    chmod +x $out/bin/sby
 
-    # Fix up shebang and Yosys imports
-    patchShebangs $out/bin/sby
-    substituteInPlace $out/bin/sby \
-      --replace "##yosys-sys-path##" \
-                "sys.path += [p + \"/share/yosys/python3/\" for p in [\"$out\", \"${yosys}\"]]"
-    substituteInPlace $out/share/yosys/python3/sby_core.py \
-      --replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"'
+    chmod +x $out/bin/sby
   '';
+
   meta = {
     description = "Tooling for Yosys-based verification flows";
-    homepage    = https://symbiyosys.readthedocs.io/;
+    homepage    = "https://symbiyosys.readthedocs.io/";
     license     = stdenv.lib.licenses.isc;
     maintainers = with stdenv.lib.maintainers; [ thoughtpolice emily ];
     platforms   = stdenv.lib.platforms.all;
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index eeb3a6b6d36..e5764461819 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -1,4 +1,4 @@
-{ callPackage, fetchurl, stdenv
+{ callPackage, fetchurl, fetchpatch, stdenv
 , ocamlPackages, coqPackages, rubber, hevea, emacs }:
 
 stdenv.mkDerivation {
@@ -30,7 +30,13 @@ stdenv.mkDerivation {
   enableParallelBuilding = true;
 
   # Remove unnecessary call to which
-  patches = [ ./configure.patch ];
+  patches = [ ./configure.patch
+    # Compatibility with js_of_ocaml 3.5
+    (fetchpatch {
+      url = "https://gitlab.inria.fr/why3/why3/commit/269ab313382fe3e64ef224813937314748bf7cf0.diff";
+      sha256 = "0i92wdnbh8pihvl93ac0ma1m5g95jgqqqj4kw6qqvbbjjqdgvzwa";
+    })
+  ];
 
   configureFlags = [ "--enable-verbose-make" ];
 
diff --git a/pkgs/applications/science/logic/workcraft/default.nix b/pkgs/applications/science/logic/workcraft/default.nix
index c0d6d541d6b..685d6ee4861 100644
--- a/pkgs/applications/science/logic/workcraft/default.nix
+++ b/pkgs/applications/science/logic/workcraft/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   pname = "workcraft";
-  version = "3.2.5";
+  version = "3.2.6";
 
   src = fetchurl {
     url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz";
-    sha256 = "11dk00b17yhk7cv8zms4nlffc0qwgsapimzr8csb89qmgabd7rj3";
+    sha256 = "1sfbxmk71gp7paw4l5azqr0lsgsyp4308gx2jz8w4k3nasfshz25";
   };
 
   buildInputs = [ makeWrapper ];
@@ -23,7 +23,7 @@ stdenv.mkDerivation rec {
   '';
 
   meta = {
-    homepage = https://workcraft.org/;
+    homepage = "https://workcraft.org/";
     description = "Framework for interpreted graph modeling, verification and synthesis";
     platforms = stdenv.lib.platforms.linux;
     license = stdenv.lib.licenses.mit;