about summary refs log tree commit diff
path: root/pkgs/applications/science/logic
diff options
context:
space:
mode:
authorAustin Seipp <aseipp@pobox.com>2020-02-27 21:50:47 -0600
committerAustin Seipp <aseipp@pobox.com>2020-02-27 21:52:15 -0600
commit3d8efecda121f83febc89b45ee89d0625f84b4c5 (patch)
tree5a7b1d6bd080e0062bd363576dc95aa87f31c3b3 /pkgs/applications/science/logic
parent572a63faf8d63332f31c6318c3fc510821dc9fbc (diff)
downloadnixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.tar
nixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.tar.gz
nixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.tar.bz2
nixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.tar.lz
nixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.tar.xz
nixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.tar.zst
nixlib-3d8efecda121f83febc89b45ee89d0625f84b4c5.zip
symbiyosys: fix calls to external programs
48085826f broke symbiyosys when it needed to call `yosys-abc`: when
`ABCEXTERNAL` is set in the Makefile, then `yosys-abc` is not built.

But in general `sby` was just calling programs out of the ambient
environment. Fix that for most programs it can invoke: it now has a
direct dependency on boolector, aiger, abc, yosys, etc.

This also does some other minor clean up.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r--pkgs/applications/science/logic/symbiyosys/default.nix36
1 files changed, 24 insertions, 12 deletions
diff --git a/pkgs/applications/science/logic/symbiyosys/default.nix b/pkgs/applications/science/logic/symbiyosys/default.nix
index d6ff7a8b4a73..6b41a44a3583 100644
--- a/pkgs/applications/science/logic/symbiyosys/default.nix
+++ b/pkgs/applications/science/logic/symbiyosys/default.nix
@@ -1,4 +1,7 @@
-{ stdenv, fetchFromGitHub, yosys, bash, python3, yices }:
+{ stdenv, fetchFromGitHub
+, bash, python3, yosys
+, yices, boolector, aiger, abc-verifier
+}:
 
 stdenv.mkDerivation {
   pname = "symbiyosys";
@@ -11,9 +14,24 @@ stdenv.mkDerivation {
     sha256 = "1pwbirszc80r288x81nx032snniqgmc80i09bbha2i3zd0c3pj5h";
   };
 
-  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"' ': "${abc-verifier}/bin/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;