Merge pull request #31264 from kini/acl2-update

acl2: 6.5 -> 7.4; sbcl: remove 1.2.0 and 1.3.12

lib/maintainers.nix

@@ -328,6 +328,7 @@
   KibaFox = "Kiba Fox <kiba.fox@foxypossibilities.com>";
   kierdavis = "Kier Davis <kierdavis@gmail.com>";
   kiloreux = "Kiloreux Emperex <kiloreux@gmail.com>";
+  kini = "Keshav Kini <keshav.kini@gmail.com>";
   kkallio = "Karn Kallio <tierpluspluslists@gmail.com>";
   knedlsepp = "Josef Kemetmüller <josef.kemetmueller@gmail.com>";
   konimex = "Muhammad Herdiansyah <herdiansyah@netc.eu>";

pkgs/development/compilers/sbcl/1.2.0.nix

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

pkgs/development/compilers/sbcl/1.3.12.nix

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

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 {
+  src = fetchFromGitHub {
-    url = "http://www.cs.utexas.edu/users/moore/acl2/${version}/distrib/acl2.tar.gz";
+    owner = "acl2-devel";
-    sha256 = "19kfclgpdyms016s06pjf3icj3mx9jlcj8vfgpbx2ac4ls0ir36g";
+    repo = "acl2-devel";
-    name = "acl2-${version}.tar.gz";
+    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 ACL2 image
-    make LISP=${sbcl}/bin/sbcl TAGS
+    make LISP=${sbcl}/bin/sbcl
-    mkdir -p $out/bin
+
+    # 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;
   };
 }

pkgs/top-level/all-packages.nix

@@ -6238,12 +6238,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 { };
@@ -6366,9 +6360,7 @@ with pkgs;
 
   ### DEVELOPMENT / INTERPRETERS
 
-  acl2 = callPackage ../development/interpreters/acl2 {
+  acl2 = callPackage ../development/interpreters/acl2 { };
-    sbcl = sbcl_1_2_0;
-  };
 
   angelscript = callPackage ../development/interpreters/angelscript {};