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

acl2: build standard library as well #85903

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

Conversation

@kini
Copy link
Member

@kini kini commented Apr 24, 2020

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.
@kini kini force-pushed the kini:acl2-update branch from 5106a4f to 77b1aa3 Apr 24, 2020
@ofborg ofborg bot requested a review from 7c6f434c Apr 24, 2020
@kini kini force-pushed the kini:acl2-update branch from 77b1aa3 to 9f87818 Apr 24, 2020
@kini kini force-pushed the kini:acl2-update branch from 9f87818 to 07938d4 May 31, 2020
@kini kini force-pushed the kini:acl2-update branch from 07938d4 to 0f14e11 May 31, 2020
@kini kini force-pushed the kini:acl2-update branch 4 times, most recently from 8fedbfb to ddbc250 May 31, 2020
@kini kini force-pushed the kini:acl2-update branch from ddbc250 to 6bc7026 Jun 1, 2020
@kini kini marked this pull request as ready for review Jun 1, 2020
@kini
Copy link
Member Author

@kini 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 kini:acl2-update branch 2 times, most recently from 18fcb47 to 1657113 Jun 2, 2020
@kini
Copy link
Member Author

@kini 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...?

@kini kini force-pushed the kini:acl2-update branch from 1657113 to b7d3837 Jun 8, 2020
@7c6f434c
Copy link
Member

@7c6f434c 7c6f434c commented Jun 11, 2020

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

@kini
Copy link
Member Author

@kini 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

@7c6f434c 7c6f434c commented Jun 13, 2020

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

@7c6f434c
Copy link
Member

@7c6f434c 7c6f434c commented Jun 13, 2020

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

@kini kini force-pushed the kini:acl2-update branch from b7d3837 to c6d6094 Jul 31, 2020
@wizeman
Copy link
Member

@wizeman wizeman commented Aug 2, 2020

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

@@ -9612,6 +9612,7 @@ in
### DEVELOPMENT / INTERPRETERS

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

This comment has been minimized.

@Mic92

Mic92 Aug 2, 2020
Contributor

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; })

This comment has been minimized.

@kini

kini Aug 2, 2020
Author Member

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.

This comment has been minimized.

@Mic92

Mic92 Aug 2, 2020
Contributor

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

@kini
Copy link
Member Author

@kini 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 kini force-pushed the kini:acl2-update branch from c6d6094 to be1fed3 Aug 2, 2020
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 force-pushed the kini:acl2-update branch from be1fed3 to 9a32d3d Aug 2, 2020
@kini kini mentioned this pull request Aug 2, 2020
4 of 10 tasks complete
@7c6f434c 7c6f434c merged commit ee02ea6 into NixOS:master Aug 2, 2020
16 checks passed
16 checks passed
Evaluation Performance Report Evaluator Performance Report
Details
acl2, acl2-minimal, acl2-minimal.passthru.tests, acl2.passthru.tests on aarch64-linux Success
Details
acl2, acl2-minimal, acl2-minimal.passthru.tests, acl2.passthru.tests on x86_64-linux Success
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="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./pkgs/t
Details
grahamcofborg-eval-lib-tests nix-build --arg pkgs import ./. {} ./lib/tests/release.nix
Details
grahamcofborg-eval-nixos nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./nixos/
Details
grahamcofborg-eval-nixos-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./nixos/
Details
grahamcofborg-eval-nixos-options nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./nixos/
Details
grahamcofborg-eval-nixpkgs-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-tarball nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-unstable-jobset nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="9a32d3d"; rev="9a32d3d136b9832514da081bf56f2bfbdae191bb"; } ./pkgs/t
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
@kini kini deleted the kini:acl2-update branch Aug 2, 2020
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

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