coqPackages.HoTT: init at 20170921

This commit is contained in:
Langston Barrett 2017-09-21 23:08:34 +00:00 committed by vbgl
parent e509f6ffdf
commit 48a49fc12e
2 changed files with 60 additions and 0 deletions

View file

@ -0,0 +1,59 @@
{ stdenv, fetchFromGitHub, autoconf, automake, coq }:
if !stdenv.lib.versionAtLeast coq.coq-version "8.6"
then throw "This version of HoTT requires Coq 8.6"
else stdenv.mkDerivation rec {
name = "coq${coq.coq-version}-HoTT-${version}";
version = "20170921";
src = fetchFromGitHub {
owner = "HoTT";
repo = "HoTT";
rev = "e3557740a699167e6adb1a65855509d55a392fa1";
sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
};
buildInputs = [ autoconf automake coq ];
enableParallelBuilding = true;
preConfigure = ''
patchShebangs ./autogen.sh
./autogen.sh
mkdir -p "$out/bin"
'';
configureFlags = [
"--bindir=$(out)/bin"
];
patchPhase = ''
patchShebangs etc
patchShebangs hoqc hoqchk hoqdep hoqide hoqtop
'';
postBuild = ''
patchShebangs hoq-config
'';
# Currently, all the scripts like hoqc and hoqtop assume that the *.vo files are
# either (1) in the same directory as the scripts, or (2) in /usr/share/hott.
# We fulfill (1), which means that these files are only accessible via hoqtop,
# hoqc, etc and not via coqtop, coqc, etc.
postInstall = ''
mv $out/share/hott/* "$out/bin"
rmdir $out/share/hott
rmdir $out/share
'';
installFlags = [
"COQBIN=${coq}/bin"
];
meta = with stdenv.lib; {
homepage = http://homotopytypetheory.org/;
description = "Homotopy type theory";
maintainers = with maintainers; [ siddharthist ];
platforms = coq.meta.platforms;
};
}

View file

@ -18526,6 +18526,7 @@ with pkgs;
dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
flocq = callPackage ../development/coq-modules/flocq {};
heq = callPackage ../development/coq-modules/heq {};
HoTT = callPackage ../development/coq-modules/HoTT {};
interval = callPackage ../development/coq-modules/interval {};
mathcomp = callPackage ../development/coq-modules/mathcomp { };
paco = callPackage ../development/coq-modules/paco {};