tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 stdenv,
3 lib,
4 runCommand,
5 patchelf,
6 makeWrapper,
7 pkg-config,
8 curl,
9 runtimeShell,
10 openssl,
11 zlib,
12 fetchFromGitHub,
13 rustPlatform,
14 libiconv,
15}:
16
17rustPlatform.buildRustPackage rec {
18 pname = "elan";
19 version = "4.1.2";
20
21 src = fetchFromGitHub {
22 owner = "leanprover";
23 repo = "elan";
24 rev = "v${version}";
25 hash = "sha256-1pEa3uFO1lncCjOHEDM84A0p6xoOfZnU+OCS2j8cCK8=";
26 };
27
28 cargoHash = "sha256-CLeFXpCfaTTgbr6jmUmewArKfkOquNhjlIlwtoaJfZw=";
29
30 nativeBuildInputs = [
31 pkg-config
32 makeWrapper
33 ];
34
35 OPENSSL_NO_VENDOR = 1;
36 buildInputs = [
37 curl
38 zlib
39 openssl
40 ]
41 ++ lib.optional stdenv.hostPlatform.isDarwin libiconv;
42
43 buildFeatures = [ "no-self-update" ];
44
45 patches = lib.optionals stdenv.hostPlatform.isLinux [
46 # Run patchelf on the downloaded binaries.
47 # This is necessary because Lean 4 is now dynamically linked.
48 (runCommand "0001-dynamically-patchelf-binaries.patch"
49 {
50 CC = stdenv.cc;
51 cc = "${stdenv.cc}/bin/cc";
52 ar = "${stdenv.cc}/bin/ar";
53 patchelf = patchelf;
54 shell = runtimeShell;
55 }
56 ''
57 export dynamicLinker=$(cat $CC/nix-support/dynamic-linker)
58 substitute ${./0001-dynamically-patchelf-binaries.patch} $out \
59 --subst-var patchelf \
60 --subst-var dynamicLinker \
61 --subst-var cc \
62 --subst-var ar \
63 --subst-var shell
64 ''
65 )
66 ];
67
68 postInstall = ''
69 pushd $out/bin
70 mv elan-init elan
71 for link in lean leanpkg leanchecker leanc leanmake lake; do
72 ln -s elan $link
73 done
74 popd
75
76 # tries to create .elan
77 export HOME=$(mktemp -d)
78 mkdir -p "$out/share/"{bash-completion/completions,fish/vendor_completions.d,zsh/site-functions}
79 $out/bin/elan completions bash > "$out/share/bash-completion/completions/elan"
80 $out/bin/elan completions fish > "$out/share/fish/vendor_completions.d/elan.fish"
81 $out/bin/elan completions zsh > "$out/share/zsh/site-functions/_elan"
82 '';
83
84 meta = {
85 description = "Small tool to manage your installations of the Lean theorem prover";
86 homepage = "https://github.com/leanprover/elan";
87 changelog = "https://github.com/leanprover/elan/blob/v${version}/CHANGELOG.md";
88 license = with lib.licenses; [
89 asl20 # or
90 mit
91 ];
92 maintainers = with lib.maintainers; [ ];
93 mainProgram = "elan";
94 };
95}