Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

symbiyosys: add smt solver backends as optional deps #71402

Merged
merged 1 commit into from Dec 4, 2019

Conversation

@matthuszagh
Copy link
Contributor

@matthuszagh matthuszagh commented Oct 19, 2019

Motivation for this change

Symbioyosys requires at least one of these backends to provide useful functionality.

The super_prove backend has been omitted since it has not yet been packaged.

Things done

I've defaulted the dependencies to true, but let me know if it would be better to have these default to false. Yices is the default backend if we'd prefer to just default one of them to true.

  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nix-review --run "nix-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Ensured that relevant documentation is up to date
  • Fits CONTRIBUTING.md.
Notify maintainers

cc @

@emilazy
Copy link
Member

@emilazy emilazy commented Oct 19, 2019

I personally feel like it's best to not do dependency injection for the solver backends, especially because a download or build of all of them is going to add a lot to the already large toolchain download (nextpnr might need splitting up when it gains Xilinx 7 Series support, as it's already a pretty large download).

I used to have the toolchain injected into python3Packages.nmigen, but eventually concluded that a build tool that calls out to external tools should probably not inject dependencies for all the tools it could be used to invoke; it's more appropriate to inject those dependencies either at the application level (as is done in glasgow) or include the appropriate other tools along with the build tool in the derivation inputs.

That said, I wouldn't mind too much depending on just yices (the "preferred" backend, AIUI) and including it in propagatedBuildInputs by default, as it would make the common use-case work out of the box without adding unduly to the build/download weight.

@matthuszagh
Copy link
Contributor Author

@matthuszagh matthuszagh commented Oct 19, 2019

Sounds good to me. Is there any downside to including the non-default solvers as optional deps defaulting to false? That way they're still wrapped up with the package, but won't add to build/download weight.

@emilazy
Copy link
Member

@emilazy emilazy commented Oct 19, 2019

I guess I mostly just don't see too much of a difference between nativeBuildInputs = [ (symbiyosys.override { withBoolector = true; }) ]; and nativeBuildInputs = [ symbiyosys boolector ];, but I'm fine deferring to your or anyone else's opinions on this; I don't have a commit bit anyway ^^;

@matthuszagh
Copy link
Contributor Author

@matthuszagh matthuszagh commented Oct 19, 2019

You're right, it's minor. My preference here is that if I have a derivation that uses symbiyosys and then decide to remove it, it doesn't require that I remember to also remove boolector, which I only included in the first place because I was using symbiyosys.

@thoughtpolice
Copy link
Member

@thoughtpolice thoughtpolice commented Dec 3, 2019

Sorry this has taken so long to get back to. My basic position is this: I agree with @emilazy here, and I think generally injecting all of these backends is probably not a good idea by default. However, I also agree there's a balance to be struct between "works out of the box" and "minimal closure size", and having symbiyosys work out of the box is desirable.

Therefore, I'd like to see this PR simply add yices as a propagated build input, so things will work by default. But I would prefer if that were all it did, with no other options. The minor nit you mentioned is still real, but in general it's true a lot of other ways inside nixpkgs, and going against the grain here leads to a lot more code for us to maintain for a bunch of solvers going forward. Personally I normally use some 'outer' derivation to wrap the others together with a consistent setup in such cases, which is what I'd suggest going for in cases like this if alternative solvers are really needed for your uses.

Copy link
Member

@thoughtpolice thoughtpolice left a comment

(Putting on hold pending prior suggestions)

Symbioyosys requires at least smt solver backend
to work out of the box.
@matthuszagh matthuszagh force-pushed the matthuszagh:symbiyosys-backends branch from 6bbaf39 to 24783ce Dec 3, 2019
@matthuszagh
Copy link
Contributor Author

@matthuszagh matthuszagh commented Dec 3, 2019

@thoughtpolice I've adjusted the commit to reflect your suggestions. I completely agree with your reasoning. Also, thanks for the suggestion to use an outer derivation. I'd previously been using an overlay, but I like your solution better.

@ofborg ofborg bot requested a review from thoughtpolice Dec 3, 2019
@thoughtpolice
Copy link
Member

@thoughtpolice thoughtpolice commented Dec 4, 2019

@matthuszagh Thanks! Sorry again this took so long

@thoughtpolice thoughtpolice merged commit 9c7cd63 into NixOS:master Dec 4, 2019
15 checks passed
15 checks passed
Evaluation Performance Report Evaluator Performance Report
Details
grahamcofborg-eval ^.^!
Details
grahamcofborg-eval-check-maintainers matching changed paths to changed attrs...
Details
grahamcofborg-eval-check-meta config.nix: checkMeta = true
Details
grahamcofborg-eval-darwin nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A darwin-tested
Details
grahamcofborg-eval-nixos nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./nixos/release-combined.nix -A tested
Details
grahamcofborg-eval-nixos-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./nixos/release.nix -A manual
Details
grahamcofborg-eval-nixos-options nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./nixos/release.nix -A options
Details
grahamcofborg-eval-nixpkgs-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A manual
Details
grahamcofborg-eval-nixpkgs-tarball nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A tarball
Details
grahamcofborg-eval-nixpkgs-unstable-jobset nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A unstable
Details
grahamcofborg-eval-package-list nix-env -qa --json --file .
Details
grahamcofborg-eval-package-list-no-aliases nix-env -qa --json --file . --arg config { allowAliases = false; }
Details
symbiyosys on aarch64-linux Success
Details
symbiyosys on x86_64-linux Success
Details
@matthuszagh matthuszagh deleted the matthuszagh:symbiyosys-backends branch Dec 5, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

3 participants
You can’t perform that action at this time.