Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
e509f6f
commit 48a49fc
Showing
2 changed files
with
60 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
}; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters