Skip to content

acl2: build standard library as well #85903

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Aug 2, 2020
Merged

acl2: build standard library as well #85903

merged 1 commit into from
Aug 2, 2020
+411 −50

Conversation

kini
Copy link
Member

@kini kini commented Apr 24, 2020 •
edited
Loading

Motivation for this change

Before this commit, we only built the main ACL2 executable. Most users will also want the standard library (the "Community Books"), so after this commit, we build the entire make everything suite, which includes essentially everything provided in the ACL2 repository.

There's also a new top-level package called acl2-minimal which has just the core ACL2 executable, for those who really only want that.

Future work: modularize the build so that we can support multiple different subsets of the standard library. A lot of the stuff in this complete build is probably superfluous to almost all users. Also, because some of the books have unclear or idiosyncratic licenses, the full build will not be cached on cache.nixos.org, and installing it will mean spending a few hours building it. So it would be good to have a pared down build which excluded non-free books and things that people rarely or never use.

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
  • 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 nixpkgs-review --run "nixpkgs-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.

Sorry, something went wrong.

@ofborg ofborg bot added the 8.has: package (new) This PR adds a new package label Apr 24, 2020
@ofborg ofborg bot requested a review from 7c6f434c April 24, 2020 01:33
@kini kini force-pushed the acl2-update branch 4 times, most recently from 8fedbfb to ddbc250 Compare June 1, 2020 01:43
@kini kini marked this pull request as ready for review June 1, 2020 02:59
@kini
Copy link
Member Author

kini commented Jun 1, 2020

OK, I think this is ready for review at this point. Everything builds successfully, though there's plenty of stuff that could stand to be removed from the default distribution, as mentioned in the PR description.

@kini kini force-pushed the acl2-update branch 2 times, most recently from 18fcb47 to 1657113 Compare June 2, 2020 05:16
@kini
Copy link
Member Author

kini commented Jun 3, 2020

I'm not sure why ofBorg isn't able to evaluate acl2-minimal on AArch64; the error in the logs indicates that it tried to build the glucose attribute of the package, but why did it? glucose is not added to buildInputs unless certifyBooks is true, which in acl2-minimal it is not. So shouldn't laziness prevent the glucose attribute from being instantiated...?

@7c6f434c
Copy link
Member

I think the patch depends on ipasirglucose unconditionally, which depends on glucose, am I getting something wrong?

@kini
Copy link
Member Author

kini commented Jun 13, 2020

Unless I'm missing something, libipasirglucose4 doesn't depend on glucose, though. (Here's the expression: https://github.com/NixOS/nixpkgs/blob/b7d3837934c29d4a3fa5e7d30f117427de7ff158/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix)

@7c6f434c
Copy link
Member

Oh interesting. One would expect some problems on ARM, but mayb build-time problems…

@7c6f434c
Copy link
Member

Hm wait, a glucose wrapper is also an unconditional parameter to mkDerivation, no?

@wizeman
Copy link
Member

wizeman commented Aug 2, 2020

I only did a brief test with one of the books, but it worked perfectly for me. Thanks!

Mic92
Mic92 reviewed Aug 2, 2020
View reviewed changes
pkgs/top-level/all-packages.nix
@@ -9612,6 +9612,7 @@ in
### DEVELOPMENT / INTERPRETERS

acl2 = callPackage ../development/interpreters/acl2 { };
acl2-minimal = callPackage ../development/interpreters/acl2 { certifyBooks = false; };
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are using this? Otherwise I would propose to not build this at all and just have the option so that someone can use acl2.override ({ certifyBooks = false; })

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The current situation is that acl2 has no books but is cached at cache.nixos.org. After this PR, acl2-minimal will be what acl2 used to be, and acl2 will now have all the books compiled and certified etc., but will not be cached at cache.nixos.org and will be unavailable to people who don't want to turn on allowUnfree.

So I was concerned that if I didn't include acl2-minimal here, this PR could be considered a step backwards from the status quo, because while you could indeed do acl2.override ({ certifyBooks = false; }) to get the old package, it would no longer be cached at cache.nixos.org since it would have no attribute in all-packages.nix. So for people who wanted ACL2 without the books, this would be strictly worse than before.

But no, personally I would not use this acl2-minimal package.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would leave the decision to @7c6f434c if he wants to maintain to separate versions

@kini
Copy link
Member Author

kini commented Aug 2, 2020

I only did a brief test with one of the books, but it worked perfectly for me. Thanks!

Thanks for testing!

Hm wait, a glucose wrapper is also an unconditional parameter to mkDerivation, no?

I see, so maybe the better thing is to put glucose = ... in an outer let expression and only refer to it in the certifyBooks-gated buildInputs extension list. I'll give that a try.

@kini
acl2, acl2-minimal: build standard library, init
9a32d3d 
Before this commit, we only built the main ACL2 executable.  Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.

There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.

Future work: modularize the build so that we can support multiple
different subsets of the standard library.  A lot of the stuff in this
complete build is probably superfluous to almost all users.  Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it.  So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
@kini kini mentioned this pull request Aug 2, 2020
Closed
10 tasks
@7c6f434c 7c6f434c merged commit ee02ea6 into NixOS:master Aug 2, 2020
@kini kini deleted the acl2-update branch August 2, 2020 19:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Mic92 Mic92

@7c6f434c 7c6f434c

Assignees
No one assigned
Labels
8.has: package (new) This PR adds a new package 10.rebuild-darwin: 1-10 10.rebuild-linux: 1-10 11.by: package-maintainer This PR was created by the maintainer of the package it changes
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@kini @7c6f434c @wizeman @Mic92