From 0094ca20cc224085d9479c614bfed52172c93b4b Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Sat, 4 Nov 2017 10:45:34 -0700 Subject: [PATCH 1/2] acl2: 6.5 -> 7.4, refactor The `make regression` line was failing because the expression was downloading a core-system-only, no-libraries source tarball. I switched to using fetchFromGitHub, which downloads the full source code -- the core system as well as the "community books", i.e. libraries -- but the libraries unfortunately do not build yet because they have more dependencies than the core system, and they also run into some impurity problems during the build process. This commit changes the ACL2 package so that at least the user will obtain the latest version of the core system, even though they won't get the community books. In a later commit I hope to fix this; it will require either changes to ACL2 itself, or a patch to be applied to ACL2 in nixpkgs. ACL2 7.4 has no trouble building on the current version of SBCL in nixpkgs, so I let it do so instead of using the ancient SBCL version 1.2.0 from 2014. I also added myself as a maintainer to this package, since I'm an active contributor to the ACL2 project and am interested in seeing it working on Nix. --- lib/maintainers.nix | 1 + .../development/interpreters/acl2/default.nix | 63 +++++++++++++++---- pkgs/top-level/all-packages.nix | 4 +- 3 files changed, 52 insertions(+), 16 deletions(-) diff --git a/lib/maintainers.nix b/lib/maintainers.nix index 451cb4867a5c..e2d3c73301b4 100644 --- a/lib/maintainers.nix +++ b/lib/maintainers.nix @@ -328,6 +328,7 @@ KibaFox = "Kiba Fox "; kierdavis = "Kier Davis "; kiloreux = "Kiloreux Emperex "; + kini = "Keshav Kini "; kkallio = "Karn Kallio "; knedlsepp = "Josef Kemetmüller "; konimex = "Muhammad Herdiansyah "; diff --git a/pkgs/development/interpreters/acl2/default.nix b/pkgs/development/interpreters/acl2/default.nix index f1e2315d7941..16734c184eb8 100644 --- a/pkgs/development/interpreters/acl2/default.nix +++ b/pkgs/development/interpreters/acl2/default.nix @@ -1,16 +1,26 @@ -{ stdenv, fetchurl, sbcl }: +{ stdenv, fetchFromGitHub, + # perl, which, nettools, + sbcl }: -stdenv.mkDerivation rec { +let hashes = { + "7.4" = "04jb789nks9llwysxz1zw9pq1dh0j39b5fcmivcc4bq9v9cga2l1"; +}; +in stdenv.mkDerivation rec { name = "acl2-${version}"; - version = "v6-5"; + version = "7.4"; - src = fetchurl { - url = "http://www.cs.utexas.edu/users/moore/acl2/${version}/distrib/acl2.tar.gz"; - sha256 = "19kfclgpdyms016s06pjf3icj3mx9jlcj8vfgpbx2ac4ls0ir36g"; - name = "acl2-${version}.tar.gz"; + src = fetchFromGitHub { + owner = "acl2-devel"; + repo = "acl2-devel"; + rev = "${version}"; + sha256 = hashes."${version}"; }; - buildInputs = [ sbcl ]; + buildInputs = [ sbcl + # which perl nettools + ]; + + enableParallelBuilding = true; phases = "unpackPhase installPhase"; @@ -18,18 +28,45 @@ stdenv.mkDerivation rec { installPhase = '' mkdir -p $out/share/${installSuffix} + mkdir -p $out/bin cp -R . $out/share/${installSuffix} cd $out/share/${installSuffix} - make 'LISP=${sbcl}/bin/sbcl --dynamic-space-size 2000' - make 'LISP=${sbcl}/bin/sbcl --dynamic-space-size 2000' regression - make LISP=${sbcl}/bin/sbcl TAGS - mkdir -p $out/bin + + # make ACL2 image + make LISP=${sbcl}/bin/sbcl + + # The community books don't build properly under Nix yet. + rm -rf books + #make ACL2=$out/share/saved_acl2 USE_QUICKLISP=1 regression-everything + cp saved_acl2 $out/bin/acl2 ''; meta = { description = "An interpreter and a prover for a Lisp dialect"; - maintainers = with stdenv.lib.maintainers; [ raskin ]; + longDescription = '' + ACL2 is a logic and programming language in which you can model + computer systems, together with a tool to help you prove + properties of those models. "ACL2" denotes "A Computational + Logic for Applicative Common Lisp". + + ACL2 is part of the Boyer-Moore family of provers, for which its + authors have received the 2005 ACM Software System Award. + + NOTE: In nixpkgs, the community books that usually ship with + ACL2 have been removed because it is not currently possible to + build them with Nix. + ''; + homepage = http://www.cs.utexas.edu/users/moore/acl2/; + downloadPage = https://github.com/acl2-devel/acl2-devel/releases; + # There are a bunch of licenses in the community books, but since + # they currently get deleted during the build, we don't mention + # their licenses here. ACL2 proper is released under a BSD + # 3-clause license. + #license = with stdenv.lib.licenses; + #[ free bsd3 mit gpl2 llgpl21 cc0 publicDomain ]; + license = stdenv.lib.licenses.bsd3; + maintainers = with stdenv.lib.maintainers; [ kini raskin ]; platforms = stdenv.lib.platforms.linux; }; } diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 92974dd3d5db..bb573341d732 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -6362,9 +6362,7 @@ with pkgs; ### DEVELOPMENT / INTERPRETERS - acl2 = callPackage ../development/interpreters/acl2 { - sbcl = sbcl_1_2_0; - }; + acl2 = callPackage ../development/interpreters/acl2 { }; angelscript = callPackage ../development/interpreters/angelscript {}; From 21db63d66956aef37f372809877f17c747df66ca Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Sat, 4 Nov 2017 10:45:51 -0700 Subject: [PATCH 2/2] sbcl: remove old versions 1.2.0, 1.3.12 SBCL 1.2.0 was being retained for the acl2 package, which no longer needs it. SBCL 1.3.12 was being retained for the maxima package, which appears to no longer need it. --- pkgs/development/compilers/sbcl/1.2.0.nix | 84 ----------------- pkgs/development/compilers/sbcl/1.3.12.nix | 104 --------------------- pkgs/top-level/all-packages.nix | 6 -- 3 files changed, 194 deletions(-) delete mode 100644 pkgs/development/compilers/sbcl/1.2.0.nix delete mode 100644 pkgs/development/compilers/sbcl/1.3.12.nix diff --git a/pkgs/development/compilers/sbcl/1.2.0.nix b/pkgs/development/compilers/sbcl/1.2.0.nix deleted file mode 100644 index 975cb7db1bbf..000000000000 --- a/pkgs/development/compilers/sbcl/1.2.0.nix +++ /dev/null @@ -1,84 +0,0 @@ -{ stdenv, fetchurl, sbclBootstrap, clisp}: - -stdenv.mkDerivation rec { - name = "sbcl-${version}"; - version = "1.2.0"; - - src = fetchurl { - url = "mirror://sourceforge/project/sbcl/sbcl/${version}/${name}-source.tar.bz2"; - sha256 = "13k20sys1v4lvgis8cnbczww6zs93rw176vz07g4jx06418k53x2"; - }; - - buildInputs = [ ] - ++ (stdenv.lib.optional stdenv.isDarwin sbclBootstrap) - ++ (stdenv.lib.optional stdenv.isLinux clisp) - ; - - patchPhase = '' - echo '"${version}.nixos"' > version.lisp-expr - echo " - (lambda (features) - (flet ((enable (x) - (pushnew x features)) - (disable (x) - (setf features (remove x features)))) - (enable :sb-thread))) " > customize-target-features.lisp - - pwd - - # SBCL checks whether files are up-to-date in many places.. - # Unfortunately, same timestamp is not good enough - sed -e 's@> x y@>= x y@' -i contrib/sb-aclrepl/repl.lisp - sed -e '/(date)/i((= date 2208988801) 2208988800)' -i contrib/asdf/asdf.lisp - sed -i src/cold/slam.lisp -e \ - '/file-write-date input/a)' - sed -i src/cold/slam.lisp -e \ - '/file-write-date output/i(or (and (= 2208988801 (file-write-date output)) (= 2208988801 (file-write-date input)))' - sed -i src/code/target-load.lisp -e \ - '/date defaulted-fasl/a)' - sed -i src/code/target-load.lisp -e \ - '/date defaulted-source/i(or (and (= 2208988801 (file-write-date defaulted-source-truename)) (= 2208988801 (file-write-date defaulted-fasl-truename)))' - - # Fix the tests - sed -e '/deftest pwent/inil' -i contrib/sb-posix/posix-tests.lisp - sed -e '/deftest grent/inil' -i contrib/sb-posix/posix-tests.lisp - sed -e '/deftest .*ent.non-existing/,+5d' -i contrib/sb-posix/posix-tests.lisp - sed -e '/deftest \(pw\|gr\)ent/,+3d' -i contrib/sb-posix/posix-tests.lisp - - sed -e '5,$d' -i contrib/sb-bsd-sockets/tests.lisp - sed -e '5,$d' -i contrib/sb-simple-streams/*test*.lisp - - # Use whatever `cc` the stdenv provides - substituteInPlace src/runtime/Config.x86-64-darwin --replace gcc cc - - substituteInPlace src/runtime/Config.x86-64-darwin \ - --replace mmacosx-version-min=10.4 mmacosx-version-min=10.5 - ''; - - preBuild = '' - export INSTALL_ROOT=$out - mkdir -p test-home - export HOME=$PWD/test-home - ''; - - buildPhase = if stdenv.isLinux - then '' - sh make.sh clisp --prefix=$out - '' - else '' - sh make.sh --prefix=$out --xc-host='${sbclBootstrap}/bin/sbcl --disable-debugger --no-userinit --no-sysinit' - ''; - - installPhase = '' - INSTALL_ROOT=$out sh install.sh - ''; - - meta = { - description = "Lisp compiler"; - homepage = http://www.sbcl.org; - license = stdenv.lib.licenses.bsd3; - maintainers = [stdenv.lib.maintainers.raskin]; - platforms = stdenv.lib.platforms.all; - inherit version; - }; -} diff --git a/pkgs/development/compilers/sbcl/1.3.12.nix b/pkgs/development/compilers/sbcl/1.3.12.nix deleted file mode 100644 index 8fa4741a4a14..000000000000 --- a/pkgs/development/compilers/sbcl/1.3.12.nix +++ /dev/null @@ -1,104 +0,0 @@ -{ stdenv, fetchurl, writeText, sbclBootstrap -, sbclBootstrapHost ? "${sbclBootstrap}/bin/sbcl --disable-debugger --no-userinit --no-sysinit" -, threadSupport ? (stdenv.isi686 || stdenv.isx86_64) - # Meant for sbcl used for creating binaries portable to non-NixOS via save-lisp-and-die. - # Note that the created binaries still need `patchelf --set-interpreter ...` - # to get rid of ${glibc} dependency. -, purgeNixReferences ? false -}: - -stdenv.mkDerivation rec { - name = "sbcl-${version}"; - version = "1.3.12"; - - src = fetchurl { - url = "mirror://sourceforge/project/sbcl/sbcl/${version}/${name}-source.tar.bz2"; - sha256 = "1hjr2xqazy4j0m58y4na6fz8ii3xflqairxy7vpd7ajbs00yqfc0"; - }; - - patchPhase = '' - echo '"${version}.nixos"' > version.lisp-expr - echo " - (lambda (features) - (flet ((enable (x) - (pushnew x features)) - (disable (x) - (setf features (remove x features)))) - '' - + (if threadSupport then "(enable :sb-thread)" else "(disable :sb-thread)") - + stdenv.lib.optionalString stdenv.isArm "(enable :arm)" - + '' - )) " > customize-target-features.lisp - - pwd - - # SBCL checks whether files are up-to-date in many places.. - # Unfortunately, same timestamp is not good enough - sed -e 's@> x y@>= x y@' -i contrib/sb-aclrepl/repl.lisp - sed -e '/(date)/i((= date 2208988801) 2208988800)' -i contrib/asdf/asdf.lisp - sed -i src/cold/slam.lisp -e \ - '/file-write-date input/a)' - sed -i src/cold/slam.lisp -e \ - '/file-write-date output/i(or (and (= 2208988801 (file-write-date output)) (= 2208988801 (file-write-date input)))' - sed -i src/code/target-load.lisp -e \ - '/date defaulted-fasl/a)' - sed -i src/code/target-load.lisp -e \ - '/date defaulted-source/i(or (and (= 2208988801 (file-write-date defaulted-source-truename)) (= 2208988801 (file-write-date defaulted-fasl-truename)))' - - # Fix the tests - sed -e '/deftest pwent/inil' -i contrib/sb-posix/posix-tests.lisp - sed -e '/deftest grent/inil' -i contrib/sb-posix/posix-tests.lisp - sed -e '/deftest .*ent.non-existing/,+5d' -i contrib/sb-posix/posix-tests.lisp - sed -e '/deftest \(pw\|gr\)ent/,+3d' -i contrib/sb-posix/posix-tests.lisp - - sed -e '5,$d' -i contrib/sb-bsd-sockets/tests.lisp - sed -e '5,$d' -i contrib/sb-simple-streams/*test*.lisp - - # Use whatever `cc` the stdenv provides - substituteInPlace src/runtime/Config.x86-64-darwin --replace gcc cc - - substituteInPlace src/runtime/Config.x86-64-darwin \ - --replace mmacosx-version-min=10.4 mmacosx-version-min=10.5 - '' - + (if purgeNixReferences - then - # This is the default location to look for the core; by default in $out/lib/sbcl - '' - sed 's@^\(#define SBCL_HOME\) .*$@\1 "/no-such-path"@' \ - -i src/runtime/runtime.c - '' - else - # Fix software version retrieval - '' - sed -e "s@/bin/uname@$(command -v uname)@g" -i src/code/*-os.lisp - '' - ); - - - preBuild = '' - export INSTALL_ROOT=$out - mkdir -p test-home - export HOME=$PWD/test-home - ''; - - buildPhase = '' - sh make.sh --prefix=$out --xc-host="${sbclBootstrapHost}" - ''; - - installPhase = '' - INSTALL_ROOT=$out sh install.sh - ''; - - # Specifying $SBCL_HOME is only truly needed with `purgeNixReferences = true`. - setupHook = writeText "setupHook.sh" '' - envHooks+=(_setSbclHome) - _setSbclHome() { - export SBCL_HOME='@out@/lib/sbcl/' - } - ''; - - meta = sbclBootstrap.meta // { - inherit version; - updateWalker = true; - }; -} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index bb573341d732..b47d817d3722 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -6234,12 +6234,6 @@ with pkgs; sbclBootstrap = callPackage ../development/compilers/sbcl/bootstrap.nix {}; sbcl = callPackage ../development/compilers/sbcl {}; - # For Maxima - sbcl_1_3_12 = callPackage ../development/compilers/sbcl/1.3.12.nix { }; - # For ACL2 - sbcl_1_2_0 = callPackage ../development/compilers/sbcl/1.2.0.nix { - clisp = clisp; - }; scala_2_9 = callPackage ../development/compilers/scala/2.9.nix { }; scala_2_10 = callPackage ../development/compilers/scala/2.10.nix { };