nordic-dev.net/nixpkgs
nordic-dev.net/nixpkgs
2
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2025-02-20 11:05:14 +00:00
Code Issues Packages Projects Releases Wiki Activity

acl2: 6.5 -> 7.4, refactor

Browse Source 
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.
This commit is contained in:
Keshav Kini 2017-11-04 10:45:34 -07:00
parent af3a11b8f6
commit 0094ca20cc
3 changed files with 52 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
lib/maintainers.nix
View File

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

63
pkgs/development/interpreters/acl2/default.nix
View File

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

4
pkgs/top-level/all-packages.nix
View File

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