Build failure: acl2 #346392
Comments
|
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
];
};
}
);
} |
|
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. |
|
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 Additionally, your argument about improper build options is not a valid counterpoint. Upstream has explicitly stated that Let’s also take a look at how other package managers handle the build:
In other words, it is failing due to non-standard build options that differ from those used by other package managers. Does |
|
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 |
|
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. |
|
certify phase is not for testing. I am requesting to use the standard build. |
|
I would like to ask you the followings:
|
|
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? |
The issue really looks like a «completeness» not «correctness» issue (also after looking at the fix) so this is not a good argument.
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. |
|
@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
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 🙂) The |
|
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. |
|
Kini, you would be wrong to believe that. The certification process is completely standard and also done by other theorem provers. |
|
@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 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 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 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 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.
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. |
|
@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. |
This is not, in fact, aligned with the actual Nixpkgs practices |
Upstream doesn't even guarantee any particular compiler (like SBCL) to work, which means that the build process in nixpkgs indeed doesn't follow the upstream specification. It's good that this issue was opened, since whoever packaged it, didn't do it right. I disagree that existing nixpkgs practices is an argument that can be substantiated with numbers by you at this time, which makes it an invalid argument. Kini basically said what I proposed, but splitting it up even further. He also says to build as much as possible. Of course, there are such things as reasonable judgement. For example, a library precomputing all winning chess moves would probably not run on nixpkgs. |
|
(I think the provided build log was basically useless, because it can't be read on a phone. ) |
Though I want to provide users with as much of a fully batteries-included experience as possible, I'm not opposed to cutting down the libraries provided by the acl2 package in nixpkgs, if that's deemed to better adhere to nixpkgs practices. I'll defer to @7c6f434c in this regard since he's much more active in the Nix community than I am and has a better grasp on this. But let's not forget, this suggestion of cutting down the included books is completely orthogonal to the build failure. @tani suggested it as one possible way to address the build failure, but there are several other less drastic ways to fix the failure, which I listed above. I think @tani perhaps didn't realize this when he first opened the issue because he wasn't aware that this package has been built successfully on SBCL 2.3.0 as recently as a couple of months ago. The package is not fundamentally broken because of the large number of certified books; it just has a bug when combined with newer SBCL versions. Let's keep this discussion focused on fixing the build failure since that is after all the title of the issue, "Build failure: acl2". We can discuss reworking the structure of the package in a different ticket if necessary. |
I think you're quite misreading the intent of that statement, which is from the ACL2 developer docs. First of all, it's aimed at developers of ACL2, not users or distro maintainers trying to build it:
The particular statement you quoted is saying that in order to discover ACL2 bugs so that they can be fixed, it's important for upstream developers to make sure to build ACL2 against many different Lisps for testing purposes. It is certainly not a statement that "upstream doesn't guarantee any particular compiler to work". Obviously it's a best-effort "guarantee", and sometimes Lisps will introduce breaking changes like what has apparently happened with SBCL, but the upstream devs then try to adapt to those changes and commit fixes and workarounds to the ACL2 source code. |
|
I count a maintainer of the nixpkgs expression to be an ACL2 developer, because preferably such a person understands the ACL2 codebase. (I certainly do.) I certainly would never identify myself as a mere user. Anyway, I shared my perspective. I will see what happens next. |
Thank you for your responses. First, I would like to express my gratitude for maintaining this recipe. I have been following the discussion, and I completely agree with Kini’s ultimate goal of solving the build failure as our top priority. As a user who wants to use this package with Nix, I am actively participating with that desire in mind. To achieve this goal, I made two suggestions at the beginning of the issue: either splitting the package into a buildable subset or shrinking the recipe. Then, Kini suggested an excellent approach—to backport patches to ACL2 itself. I found Kini’s suggestion very reasonable, so I investigated this further and successfully created the patch. I am pleased to report that we have resolved the build issue. For now, incorporating this patch should be sufficient to consider the issue resolved. Thank you for your suggestion. Now, after the good news, I must share some bad news—the reason for the delay in my report. While I completed the patch quickly, to confirm that the build works locally, I needed to acquire a powerful computing environment (16 CPUs, 60GB of RAM) and set up a fresh Nix environment on that machine to verify the build. It took more than 6 hours (with 16 CPUs) to complete the installation of this package. I have no objection to integrating the patch and releasing it as is, as my goal is to use ACL2. From here, I would like to engage in a constructive discussion on how ACL2 users can easily use it via Nix. As shown below, if you install the basic version, it can be installed with a 8-minute certification phase. Since the certification phase does not run every time, we cannot generally say that the long installation time is an issue. But what about the 6-hour installation time? Additionally, ACL2’s codebase includes the following statement: Furthermore, the full build (not basic) includes proof code from past ACL2-related conferences (in the workshop/ directory). This is no longer just a library, but includes records from past workshops. Should users really need to run their machines for 6 hours on the first installation to build all of this? The standard ACL2 build takes 8 minutes, so why should we execute all of this? If I were to create the ACL2 package like Kini and submit it here, I would understand the caution of making "all" an option. So, I’m not criticizing past choices, but rather, I’d like to discuss how we can make it more user-friendly. One idea is to separate ACL2 into something like acl2-minimal, acl2-basic, and acl2-full, as other distributions like Texlive have done. Or, we could allow users to select options for ACL2 during installation. The method proposed by Kini—installing acl2-minimal and letting users manually install the books—is theoretically possible. However, since the current version has hooks that delete all the books during post-installation, if we adopt that idea, we will need to modify acl2-minimal. If that happens, I’m willing to help edit the code and assist with maintenance. Please allow me to do so. First of all, I am grateful that I could improve ACL2 by writing a patch and getting it to work. Depending on the maintainers’ decision, it’s also fine to close the issue here after merging the patch and continue the discussion in a separate issue. I leave it to your discretion. Lastly, I am neither a developer of ACL2 itself nor a Nix maintainer. However, as an OSS volunteer, I am willing to put in the work, write patches, and spend time experimenting to improve Nix. Patch for ACL2 (click here)diff --git a/books/quicklisp/base.lisp b/books/quicklisp/base.lisp
index 0e0f957b1f..4e47fabdcc 100644
--- a/books/quicklisp/base.lisp
+++ b/books/quicklisp/base.lisp
@@ -51,9 +51,13 @@
;; reason to want the Quicklisp files to live somewhere other than your ACL2
;; books directory.
(getenv$ "QUICKLISP_ASDF_HOME" state)
- (let ((dir (if err
- (er hard? 'getenv$ "getenv failed")
- (or override-dir (cbd)))))
+ (let* ((dir (if err
+ (er hard? 'getenv$ "getenv failed")
+ (or override-dir (cbd))))
+ (dir-last (- (length dir) 1))
+ (dir (if (eql #\/ (char dir dir-last))
+ (subseq dir 0 dir-last)
+ dir)))
(progn$
(setenv$ "XDG_CONFIG_HOME" (concatenate 'string dir "/asdf-home/config"))
(setenv$ "XDG_DATA_HOME" (concatenate 'string dir "/asdf-home/data"))
diff --git a/books/quicklisp/bundle/local-projects/fastnumio/read-hex.lisp b/books/quicklisp/bundle/local-projects/fastnumio/read-hex.lisp
index bf0355e3b9..b7d1712d62 100644
--- a/books/quicklisp/bundle/local-projects/fastnumio/read-hex.lisp
+++ b/books/quicklisp/bundle/local-projects/fastnumio/read-hex.lisp
@@ -315,9 +315,13 @@
(assert (equal (sb-bignum::%bignum-ref (1- (expt 2 80)) 0) (1- (expt 2 64))))
(assert (equal (sb-bignum::%bignum-ref (1- (expt 2 80)) 1) (1- (expt 2 16))))
(assert (typep (1- (expt 2 64)) 'sb-bignum::bignum-element-type))
+
+ (defun high32-bits (i)
+ (ldb (byte 32 32) i))
+
(let* ((x #xfeedf00ddeadd00ddeadbeef99998888)
(digit (sb-bignum::%bignum-ref x 0))
- (high32 (sb-bignum::%digit-logical-shift-right digit 32))
+ (high32 (high32-bits digit))
(low32 (logand digit #xFFFFFFFF)))
(assert (typep high32 'fixnum))
(assert (typep low32 'fixnum))
@@ -418,7 +422,7 @@
; (format t "got high = #x~x, end is now ~d~%" high32 end)
; (format t "Installing chunk ~d <-- #x~x,#x~x~%" u64pos high32 low32)
(setf (sb-bignum::%bignum-ref ans u64pos)
- (logior (sb-bignum::%ashl high32 32)
+ (logior (ash high32 32)
low32))
(incf u64pos))
diff --git a/books/quicklisp/bundle/local-projects/fastnumio/write-hex.lisp b/books/quicklisp/bundle/local-projects/fastnumio/write-hex.lisp
index abbe3e60c7..15903a43a4 100644
--- a/books/quicklisp/bundle/local-projects/fastnumio/write-hex.lisp
+++ b/books/quicklisp/bundle/local-projects/fastnumio/write-hex.lisp
@@ -27,6 +27,9 @@
; DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis <[email protected]>
+;
+; Modifications by Stephen Westfold <[email protected]> to work with sbcl ARM64
+; and improved efficiency with sbcl x86-64
(in-package "FASTNUMIO")
@@ -375,7 +378,83 @@
;; we want to print and POS says how many we need. So write them.
(write-string arr stream)))
+;; Versions that are more efficient for 64 bit machines
+;; These need to be inline to avoid unnecessary boxing of 64-bit words to bignums
+(declaim (inline write-hex-u64-without-leading-zeroes))
+(defun write-hex-u64-without-leading-zeroes (val stream)
+ ;; Completely portable.
+ (declare (type (unsigned-byte 64) val))
+ (if (eql val 0)
+ (write-char #\0 stream)
+ (let ((pos 1) ;; **see below
+ (shift -60)
+ (nibble 0)
+ (arr (make-array 16 :element-type 'character)))
+ (declare (type string arr)
+ (dynamic-extent arr)
+ (type (unsigned-byte 64) pos)
+ (type fixnum shift)
+ (type (unsigned-byte 4) nibble))
+ ;; Skip past any leading zeroes. Note that we already checked for the
+ ;; all-zero case above, so we know a nonzero digit exists and that we
+ ;; will eventually exit the loop.
+ (loop do
+ (setq nibble
+ (the (unsigned-byte 4)
+ (logand #xF (the (unsigned-byte 64)
+ (ash (the (unsigned-byte 64) val)
+ (the (integer -60 0) shift))))))
+ (incf shift 4)
+ (unless (eql nibble 0)
+ (loop-finish)))
+ ;; At this point we know we are standing at a nonzero digit and that
+ ;; its value is already in nibble. Install its value into the array.
+ (setf (schar arr 0) (hex-digit-to-char nibble))
+ ;; ** above we initialized pos to 1, so we don't need to increment
+ ;; it here. Shift has also already been incremented.
+ (loop do
+ (when (> shift 0)
+ (loop-finish))
+ (setq nibble
+ (the (unsigned-byte 4)
+ (logand #xF (the (unsigned-byte 64)
+ (ash (the (unsigned-byte 64) val)
+ (the (integer -60 0) shift))))))
+ (setf (schar arr pos) (hex-digit-to-char nibble))
+ (incf pos)
+ (incf shift 4))
+ ;; At the end of all of this, the array is populated with the digits
+ ;; we want to print and POS says how many we need. So write them.
+ (write-string arr stream :end pos)))
+ stream)
+(declaim (inline write-hex-u64-with-leading-zeroes))
+(defun write-hex-u64-with-leading-zeroes (val stream)
+ ;; Completely portable.
+ (declare (type (unsigned-byte 64) val))
+ (let ((pos 0)
+ (shift -60)
+ (nibble 0)
+ (arr (make-array 16 :element-type 'character)))
+ (declare (type string arr)
+ (dynamic-extent arr)
+ (type fixnum pos)
+ (type fixnum shift)
+ (type (unsigned-byte 4) nibble))
+ (loop do
+ (when (> shift 0)
+ (loop-finish))
+ (setq nibble
+ (the (unsigned-byte 4)
+ (logand #xF (the (unsigned-byte 64)
+ (ash (the (unsigned-byte 64) val)
+ (the (integer -60 0) shift))))))
+ (incf shift 4)
+ (setf (schar arr pos) (hex-digit-to-char nibble))
+ (incf pos))
+ ;; At the end of all of this, the array is populated with the digits
+ ;; we want to print and POS says how many we need. So write them.
+ (write-string arr stream)))
; CCL specific bignum printing.
;
@@ -426,7 +505,6 @@
(setq chunk (ccl::uvref val pos))
(write-hex-u32-with-leading-zeroes chunk stream))))))
-
; SBCL specific bignum printing.
;
; Note: SBCL on Linux X86-64 represents bignums as vectors of 64-bit 'digits',
@@ -443,10 +521,22 @@
(assert (equal (sb-bignum::%bignum-ref (1- (expt 2 80)) 1) (1- (expt 2 16))))
(assert (typep (1- (expt 2 64)) 'sb-bignum::bignum-element-type))
+ ;; (declaim (inline digit-logical-shift-right))
+ ;; (defun digit-logical-shift-right (digit sh)
+ ;; (sb-bignum::%digit-logical-shift-right digit sh))
+
+ (declaim (inline high32-bits))
+ (defun high32-bits (i)
+ (ldb (byte 32 32) i))
+
+ (declaim (inline low32-bits))
+ (defun low32-bits (i)
+ (ldb (byte 32 0) i))
+
(let* ((x #xfeedf00ddeadd00ddeadbeef99998888)
(digit (sb-bignum::%bignum-ref x 0))
- (high32 (sb-bignum::%digit-logical-shift-right digit 32))
- (low32 (logand digit #xFFFFFFFF)))
+ (high32 (high32-bits digit))
+ (low32 (low32-bits digit)))
(assert (typep high32 'fixnum))
(assert (typep low32 'fixnum))
(assert (typep high32 '(unsigned-byte 32)))
@@ -541,30 +631,36 @@
;; good enough to let SBCL's compiler realize that it doesn't need to create
;; a bignum for the digit.
- (declaim (inline write-nth-hex-bignum-digit-with-leading-zeroes))
- (defun write-nth-hex-bignum-digit-with-leading-zeroes (n val stream)
- (let ((high32 (sb-bignum::%digit-logical-shift-right (sb-bignum::%bignum-ref val n) 32))
- (low32 (logand (sb-bignum::%bignum-ref val n) #xFFFFFFFF)))
- (declare (type (unsigned-byte 32) high32 low32))
- (write-hex-u32-with-leading-zeroes high32 stream)
- (write-hex-u32-with-leading-zeroes low32 stream)))
-
- (declaim (inline write-nth-hex-bignum-digit-without-leading-zeroes))
- (defun write-nth-hex-bignum-digit-without-leading-zeroes (n val stream)
- ;; If digit is nonzero, we print it and return T.
- ;; If digit is zero, we do not print anything and return NIL.
- (let* ((high32 (sb-bignum::%digit-logical-shift-right (sb-bignum::%bignum-ref val n) 32))
- (low32 (logand (sb-bignum::%bignum-ref val n) #xFFFFFFFF)))
- (declare (type (unsigned-byte 32) high32 low32))
- (if (eql high32 0)
- (if (eql low32 0)
- nil
- (progn (write-hex-u32-without-leading-zeroes low32 stream)
- t))
- (progn
- (write-hex-u32-without-leading-zeroes high32 stream)
- (write-hex-u32-with-leading-zeroes low32 stream)
- t))))
+ ;; sjw: I obviated the need for these by introducing write-hex-u64-without-leading-zeroes
+ ;; and write-hex-u64-with-leading-zeroes which allow the extra step of splitting into high
+ ;; and low to be avoided. Declaring these be inline avoids the creation of ephemeral bignums.
+
+
+ ;; (declaim (inline write-nth-hex-bignum-digit-with-leading-zeroes))
+ ;; (defun write-nth-hex-bignum-digit-with-leading-zeroes (n val stream)
+ ;; (let ((high32 (high32-bits (sb-bignum::%bignum-ref val n)))
+ ;; (low32 (low32-bits (sb-bignum::%bignum-ref val n))))
+ ;; (declare (type (unsigned-byte 32) high32 low32))
+ ;; (write-hex-u32-with-leading-zeroes high32 stream)
+ ;; (write-hex-u32-with-leading-zeroes low32 stream)))
+
+ ;; (declaim (inline write-nth-hex-bignum-digit-without-leading-zeroes))
+ ;; (defun write-nth-hex-bignum-digit-without-leading-zeroes (n val stream)
+ ;; ;; If digit is nonzero, we print it and return T.
+ ;; ;; If digit is zero, we do not print anything and return NIL.
+ ;; (let* ((high32 (high32-bits (sb-bignum::%bignum-ref val n)))
+ ;; (low32 (low32-bits (sb-bignum::%bignum-ref val n))))
+ ;; (declare (type (unsigned-byte 32)
+ ;; high32 low32))
+ ;; (if (eql high32 0)
+ ;; (if (eql low32 0)
+ ;; nil
+ ;; (progn (write-hex-u32-without-leading-zeroes low32 stream)
+ ;; t))
+ ;; (progn
+ ;; (write-hex-u32-without-leading-zeroes high32 stream)
+ ;; (write-hex-u32-with-leading-zeroes low32 stream)
+ ;; t))))
;; Main bignum printing loop...
@@ -582,10 +678,12 @@
;; chunks and don't print them.
(loop do
(decf pos)
- (when (write-nth-hex-bignum-digit-without-leading-zeroes pos val stream)
- ;; Printed something, so subsequent chunks must be printed with
- ;; zeroes enabled.
- (loop-finish)))
+ (if (eql (sb-bignum::%bignum-ref val pos) 0)
+ nil
+ (progn (write-hex-u64-without-leading-zeroes (sb-bignum::%bignum-ref val pos) stream)
+ ;; Printed something, so subsequent chunks must be printed with
+ ;; zeroes enabled.
+ (loop-finish))))
;; We have printed at least one chunk, skipping leading zeroes, so we
;; need to print the remaining chunks in full.
@@ -593,7 +691,7 @@
(decf pos)
(when (< pos 0)
(loop-finish))
- (write-nth-hex-bignum-digit-with-leading-zeroes pos val stream)))))
+ (write-hex-u64-with-leading-zeroes (sb-bignum::%bignum-ref val pos) stream)))))
; Wrap up: |
|
Thanks for the update, @tani. Before I respond to your entire message, I'll quickly mention that I've also been testing the same patch on my own machine (8 threads, 64 GB RAM) and it seems to work, though I found another issue with the Nix expression which I've also fixed. I'll push the branch in a minute and then we can work on getting it merged to fix the immediate failure. |
|
Thank you very much. I’m glad to hear that we have confirmation from the maintainers, and it looks like we’ll have a working solution. Thank you also for fixing the Nix bugs. |
|
Did the build take quite a long time in your environment as well? If you have a rough estimate of the build time, could you let me know? |
|
A more general lesson to be learned from this is that Hydra should build unfree packages, but just not distribute hem in order to catch build failures before users encounter them. |
Steps To Reproduce
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,
allis an alias forregression-everything, and is a non-standard option as described below:Therefore, I suggest building with the
basictarget, which is the standard build option.Build log
https://gist.github.com/tani/1895f5fbe5e490ba27c0b14649a247e7
Additional context
I would like to ask you the followings:
acl2-basic?Notify maintainers
@kini @raskin
Metadata
Please run
nix-shell -p nix-info --run "nix-info -m"and paste the result.Add a 👍 reaction to issues you find important.
The text was updated successfully, but these errors were encountered: