61 lines
2.2 KiB
Ruby
61 lines
2.2 KiB
Ruby
class ElanInit < Formula
|
||
desc "Lean Theorem Prover installer and version manager"
|
||
homepage "https://github.com/leanprover/elan"
|
||
url "https://github.com/leanprover/elan/archive/v1.3.1.tar.gz"
|
||
sha256 "8e1380a1cb20cec54f07e30519ad7bc0179d9e3d68d33c02d0476248322b5015"
|
||
license any_of: ["Apache-2.0", "MIT"]
|
||
head "https://github.com/leanprover/elan.git", branch: "master"
|
||
|
||
bottle do
|
||
sha256 cellar: :any_skip_relocation, monterey: "b3fe1b75cae3f28df2396ed8135c81cce9aba4983818c23cc512e9f5bf7fad1d"
|
||
sha256 cellar: :any_skip_relocation, big_sur: "4f5f7dc532d5336c0cdb6842d24e47f141baaaa421234231c018606c9e640aca"
|
||
sha256 cellar: :any_skip_relocation, catalina: "da690e90eb12525fb959d870768efc6aafc52bf89079b55dab286aba933cbf47"
|
||
sha256 cellar: :any_skip_relocation, x86_64_linux: "b911325b4e04255311dda1dab5ab19516f3196ba63b11170d782149d2a5f36c7"
|
||
end
|
||
|
||
depends_on "rust" => :build
|
||
# elan-init will run on arm64 Macs, but will fetch Leans that are x86_64.
|
||
depends_on arch: :x86_64
|
||
depends_on "coreutils"
|
||
depends_on "gmp"
|
||
|
||
uses_from_macos "zlib"
|
||
|
||
conflicts_with "lean", because: "`lean` and `elan-init` install the same binaries"
|
||
|
||
def install
|
||
ENV["RELEASE_TARGET_NAME"] = "homebrew-build"
|
||
|
||
system "cargo", "install", "--features", "no-self-update", *std_cargo_args
|
||
|
||
%w[lean leanpkg leanchecker leanc leanmake lake elan].each do |link|
|
||
bin.install_symlink "elan-init" => link
|
||
end
|
||
|
||
bash_output = Utils.safe_popen_read(bin/"elan", "completions", "bash")
|
||
(bash_completion/"elan").write bash_output
|
||
zsh_output = Utils.safe_popen_read(bin/"elan", "completions", "zsh")
|
||
(zsh_completion/"_elan").write zsh_output
|
||
fish_output = Utils.safe_popen_read(bin/"elan", "completions", "fish")
|
||
(fish_completion/"elan.fish").write fish_output
|
||
end
|
||
|
||
test do
|
||
system bin/"elan-init", "-y"
|
||
(testpath/"hello.lean").write <<~EOS
|
||
def id' {α : Type} (x : α) : α := x
|
||
|
||
inductive tree (α : Type) : Type
|
||
| node : α → list tree → tree
|
||
|
||
example (a b : Prop) : a ∧ b -> b ∧ a :=
|
||
begin
|
||
intro h, cases h,
|
||
split, repeat { assumption }
|
||
end
|
||
EOS
|
||
system bin/"lean", testpath/"hello.lean"
|
||
system bin/"leanpkg", "help"
|
||
end
|
||
end
|