Build failure: acl2

[tani]

Steps To Reproduce

$ nix run nixpkgs#acl2

I have a suggestion regarding the build options for ACL2.
Currently, the build option for ACL2 is set to all, which tries to build all the recipes for ACL2.
This leads to the following issues:

• The build fails on both NixOS and nix on Ubuntu.

• The cause is that it tries to build Quicklisp.

• In the first place, all is an alias for regression-everything, and is a non-standard option as described below:

  A very full build, including very slow books. Most users will not want to use this target. It is useful for, e.g., regression testing before releases. Note that EXCLUDED_PREFIXES may not work with the regression-everything target.

• Therefore, I suggest building with the basic target, which is the standard build option.

  The default. This is a lightweight selection of books for reasoning about arithmetic, lists, sets, strings, I/O, etc., and other miscellaneous tools and macros. Many users may find "basic" to be a convenient starting place.

Build log

https://gist.github.com/tani/1895f5fbe5e490ba27c0b14649a247e7

Additional context

I would like to ask you the followings:

• Could you still install acl2 with your nix?
• Should I separate the package, something like acl2-basic?

Notify maintainers

@kini @raskin

Metadata

Please run nix-shell -p nix-info --run "nix-info -m" and paste the result.

[user@system:~]$ nix-shell -p nix-info --run "nix-info -m"
 - system: `"x86_64-linux"`
 - host os: `Linux 5.15.153.1-microsoft-standard-WSL2, NixOS, 24.11 (Vicuna), 24.11.20240926.1925c60`
 - multi-user?: `yes`
 - sandbox: `yes`
 - version: `nix-env (Nix) 2.18.7`
 - channels(root): `"nixos-24.05, nixos-wsl"`
 - nixpkgs: `/nix/store/fpivx4sjcp2vk4rp9nhliln5cwcp3kc6-source`

---

Add a :+1: reaction to issues you find important.

[tani]

Here is an example of a `basic' target.

{
  inputs = {
    flake-utils.url = "github:numtide/flake-utils";
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
  };

  outputs = inputs:
    inputs.flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = (import (inputs.nixpkgs) {
          inherit system;
          config.allowUnfree = true;
          overlays = [
            (self: super: {
              acl2 = super.acl2.overrideAttrs (old: {
                certifyBooksPhase = ''
                  # Certify the community books
                  pushd $out/share/${old.pname}/books
                  makeFlags="ACL2=$out/share/${old.pname}/saved_acl2"
                  buildFlags="basic"
                  buildPhase

                  # Clean up some stuff to save space
                  find -name '*@useless-runes.lsp' -execdir rm {} +  # saves ~1GB of space
                  find -name '*.cert.out' -execdir gzip {} +         # saves ~400MB of space

                  popd
                '';
              });
            })
          ];
        });
      in {
        devShell = pkgs.mkShell {
          buildInputs = [
            pkgs.acl2
          ];
        };
      }
    );
}

[hacscred]

Distributions (which NixOS is) run tests typically to cover their bottoms.

The tests need to be fixed. An individual user might use your process to work around an immediate problem for their non-critical problem, but should Intel use such a build to verify their FPU? No. Do we want people to trust NixOS builds to be professional level builds suitable for use in a business? Yes.

As such, as practical as it is, it would not make nixpkgs better. If nobody wants to maintain acl2, then in the long run it will just be removed from nixpkgs. Since businesses depend on it, I think they will just reach for their wallet.

Unless you have other concerns, please close this or link to an upstream issue.

Nixpkgs is not the place to fix this.

[tani]

I would like to ask the maintainers as I mentioned the above.

---

I argue that this should be fixed within nixpkgs.

First, your point seems to be that "the test failure is not the responsibility of nixpkgs, and it should be reported upstream," correct? For those unfamiliar with using ACL2, let me clarify that the error mentioned above is not related to a "test." I assume you inferred it was a test due to the name "certify," but this is not a test. It is not the kind of test you are referring to. The issue occurs during the signature phase of the books (which are the standard libraries in ACL2 terminology). This indicates that the libraries cannot be loaded. Furthermore, since the build is failing, it cannot even be installed.

As proof that this is about the use of the standard libraries and not tests, note that nixpkgs also includes a package called acl2-minimal which disables the libraries. This is not a matter of testing, but rather whether or not the libraries are included.

Additionally, your argument about improper build options is not a valid counterpoint. Upstream has explicitly stated that all is not necessary for common use cases. They have announced that basic is the standard installation method. Blaming the developer for a failed build caused by using settings that go against their intent seems unreasonable, doesn’t it?

Let’s also take a look at how other package managers handle the build:

• Homebrew - In the project root, make USE_QUICKLISP=0 all basic has the same effect as running make basic in the books directory.

In other words, it is failing due to non-standard build options that differ from those used by other package managers. Does nix run nixpkgs#acl2 work in your environment? If not, that should be fixed. And if it works using the developer’s recommended standard method, it would be best to follow that. If it works in your environment, please let me know how you did it.

[tani]

The error mentioned above has been fixed in this pull request, and we are currently waiting for the release. The build error should be resolved soon. With that in mind, I would like to discuss whether the build option all (which signs all libraries, including unnecessary ones) is truly necessary.

[hacscred]

Homebrew is not a professional distribution of software. It can't be seriously compared to nixpkgs.

Your argument can also be applied to build g++ without the standard C++ library and we see nobody arguing for that.

Nixpkgs is not a basic build environment. It has a higher bar than Homebrew (just look at the name). Homebrew was created to make more software work on MacBooks. Nix was created to demonstrate the last word in software packaging (it just did that so well that people picked it up). Please stop pretending Homebrew and nixpkgs are equals. They have never been equal.

Can you explain why you want to have this changed? I like Hydra running all the tests, because I then don't have to anymore. It saves computation for many users. That's why build farms exist in the first place.

The build in nixpkgs is the "release build" the developers are talking about.

[tani]

certify phase is not for testing. I am requesting to use the standard build.

[tani]

I would like to ask you the followings:

• Could you still install acl2 with your nix?
• Should I separate the package, something like acl2-basic?

[tani]

From the perspective of testing, if I may say so, a file that is certified is marked as correct in ACL2. Therefore, when building with the 'basic' option, the libraries built with 'basic' are guaranteed to be correct, and files that were not built with 'basic' cannot be loaded. In other words, regarding your concern about professional use, rest assured that the 'basic' option will still guarantee correct operation.

Have you used ACL2 before, and are your comments based on that experience?

[7c6f434c]

An individual user might use your process to work around an immediate problem for their non-critical problem, but should Intel use such a build to verify their FPU? No.

The issue really looks like a «completeness» not «correctness» issue (also after looking at the fix) so this is not a good argument.

Do we want people to trust NixOS builds to be professional level builds suitable for use in a business? Yes.

Actually, no. If upstream says «typical users generally want this», and that part works, packaging this is reasonable. Specific code needs of specific businesses are not our problem ever; specific needs of the business's employees might be, if those are contributing.

[kini]

@hacscred As a maintainer of this package, as far as I am concerned, this is a perfectly valid ticket to open. I think you don't understand what "book certification" means in the context of ACL2.

@tani Thanks for your report. I was able to replicate the build failure on my NixOS machine, although the build worked fine for me as late as a couple of months ago (on SBCL 2.3.0). As you later pointed out, this is a bug related to recent versions of SBCL. Because the acl2 package is marked as "unfree" (because of problematic licensing of some of the community books), cache.nixos.org doesn't build it, otherwise this would have been noticed by the person who upgraded SBCL. I think our options for directly fixing the bug are

1. backporting the fix from ACL2 upstream as a patch; or,
2. if master there has moved too far since the 8.5 release (which it may well have), abandoning stable version 8.5 and upgrading the acl2 in nixpkgs to a snapshot version from current master
3. reintroducing an older version of SBCL in nixpkgs (separately from the existing up-to-date SBCL of course) to build ACL2 from

BTW I think you meant to ping @7c6f434c rather than @raskin as the second maintainer here. (I see that he has already found the ticket though :slightly_smiling_face:) The default.nix file lists [ kini raskin ] as the maintainers of the package, but that's not a list of github usernames, it's a list of attributes in maintainers/maintainer-list.nix where you can look up the maintainers' email addresses and github usernames.

[hacscred]

Having one Nix expression with multiple outputs, especially when the build objects are reused/shared, would be an improvement to nixpkgs, which may accomplish your goal, which still isn't clear.

You are claiming there are "unnecessary libraries", which suggests libraries that have no use to anyone on the planet. That seems hard to prove.

Regarding 7c6f434c, some Intel engineer probably uses some libraries (since they funded part of it), so if it's not there their internal targets can't be met, which makes it a correctness problem for them.

I agree that it's a completeness issue on the level you were talking about.

The default for a build system should be to build as much as possible. Certification would be a part of that for a theorem proving system (and they are in NixOS doe other systems). For something like a nightly build, one would probably disable some features and Nix expressions for building random commits do exist.

One good way of packaging acl2 is having one artifact for the code and one for the library with Nix attributes existing to install both of them by just referring to pkgs.acl2.

Also, I am not sure why you want to make builds have less features. If you are on some exotic hardware architecture and need to build everything, you could just write some basic overrides to also accomplish your goal. I don't understand why you want to argue to make a system that already works, worse.

[hacscred]

Kini, you would be wrong to believe that. The certification process is completely standard and also done by other theorem provers.

[kini]

@tani Regarding your suggestion to create a cut down version of the acl2 package that contains fewer books, as you pointed out in one of your followup comments, we actually already have acl2-minimal which merely builds ACL2 itself and none of the books. (And since it is unencumbered by the licensing problems found in the books directory, it's built by Hydra and cached on cache.nixos.org and everything.)

Unfortunately the standard build instructions for ACL2 from upstream generally make the assumption that you have the entire source directory checked out somewhere writable, e.g. in your home directory. Yes, they say that basic is an appropriate make target for someone wanting to get started, but the assumption is that if the user ever needs to use a book that isn't included in the basic target, then they can certify that particular book with cert.pl, or just run a broader make target in the books dir, and immediately start using it.

But in a distribution packaging context, this doesn't make as much sense. In particular, in NixOS, build artifacts are immutable. We do whatever we do during the build process, and then after that the entire source tree is frozen in $out/share/acl2/, so whatever books were not certified during the build are not possible to certify anymore afterwards. This is because ACL2 requires a certificate file to be in the same absolute directory (after resolving symlinks) as the book it is certifying, and that directory is now read-only.

Given that fact, I decided that it would be best if we just certified as many books as possible during the initial build, so that users won't encounter an uncertified book in the community books. The downsides of this are that it makes the build very slow, makes the output artifact very large, and increases the surface area of bugs which can break the build (such as this one where a new version of SBCL doesn't break the make basic target but it does break the make all target).

Ideally, I think, we would treat this similarly to other programming languages in nixpkgs, where there's a package for the central compiler or interpreter (ACL2 in this case) and then separate packages for each of its libraries. That will allow people to only build and install the libraries they are personally interested in, and bugs that crop up will be isolated to the package for the specific library triggering that bug.

There are some problems that need to be solved in order to adopt this approach, though.

1. As mentioned before, ACL2 cares at a deep level about the precise absolute path of a book and its certificate file. We may need to either patch ACL2 to or trick it somehow in order to accept a situation where it sees what looks like a source tree with books and certificates etc. but is actually a construct of symlinks pointing to files in various Nix store paths. There is a technical effort required here but also a philosophical question of whether such a modification would invalidate the correctness guarantees made by the ACL2 authors. Users may object to such patching of ACL2's correctness-ensuring mechanisms.
2. The community books that ship with the ACL2 source code are not really naturally separated into independent "libraries"; there is a lot of cross-importing (i.e. use of (INCLUDE-BOOK)) between them, because the developers assume that all users have all the books available (i.e. present on the system and either already certified or possible to certify in the future), because they are distributed with ACL2 itself. So we as the maintainers would have to make some decision about how to split up the books into separate packages and at what granularity.

Personally I do not have the bandwidth to tackle either of these two problems, which is why I've left the Nix expression as just building the entire community books, even though I know most users only use a small fraction of that. But if someone is willing to work on the modularization project I outlined above, I'd be happy to support its uptake into nixpkgs.

It may be worthwhile looking into what Debian does here; as I recall, they do split the community books into multiple modular packages, though they may not run into problem # 1 above because on Debian all packages install to the standard FHS directories rather than being isolated from each other like on NixOS.

Finally, I'll just add that I personally haven't been using ACL2 for the last 5 years or so, though I do try to build this package once in a while to make sure it's still working, upgrade it to the latest stable version, etc. So I may not be up to speed on the latest upstream developments.

[kini]

@hacscred I apologize if I misunderstood you. Your reference to "tests" led me to believe you were confusing book certification with the test suite found in many other packages, which are not treated as part of the "build" and we often would patch out for convenience, whereas that cannot be done here without affecting the functionality of the package for users.

In any case, I disagree with you that this ticket shouldn't have been opened. The reporter found that the nix expression currently in master on nixpkgs fails to build, without any modification. That seems like the definition of a nixpkgs-specific issue that should be reported here.

[7c6f434c]

The default for a build system should be to build as much as possible.

This is not, in fact, aligned with the actual Nixpkgs practices