Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fstar fails to build #5123

Closed
vmrsss opened this issue Sep 22, 2016 · 9 comments
Closed

fstar fails to build #5123

vmrsss opened this issue Sep 22, 2016 · 9 comments
Labels
ocaml OCaml use is a significant feature of the PR or issue

Comments

@vmrsss
Copy link

vmrsss commented Sep 22, 2016

link to output of brew gist-logs fstar

https://gist.github.com/a8e9609be396dedffa516036005b0532

The build breaks at
opam install ocamlfind=1.5.5 batteries=2.5.2 zarith=1.3 yojson=1.1.6

it manages to download the package batteries-2.5.2, but then crashes with

"Your request can't be satisfied:

  • No package matches batteries.2.5.2.

No solution found, exiting"

@vmrsss
Copy link
Author

vmrsss commented Sep 29, 2016

anybody? thanks

@dunn
Copy link
Contributor

dunn commented Oct 11, 2016

Sorry for the late reply! I can reproduce this, but I've tried a few different things and haven't figured out a fix yet.

@dunn dunn added help wanted Task(s) needing PRs from the community or maintainers ocaml OCaml use is a significant feature of the PR or issue labels Oct 11, 2016
@vmrsss
Copy link
Author

vmrsss commented Oct 15, 2016

thanks for the reply dunn, i am happy others can reproduce the issue, hopefully there will be a fix soon. I really need FStar soon, but am very new to homebrew, i wouldn't know where to start to fix the build.

@josephlr
Copy link

josephlr commented Oct 26, 2016

It looks like there is a conflict with the dependancies of the packages being installed. base-ocamlbuild is needed to install batteries, but base-ocamlbuild will not work with ocaml version >= 4.03.

To fix this, we need to make the install sandbox use an earlier version of ocaml. The simple patch below fixes the build:

diff --git a/Formula/fstar.rb b/Formula/fstar.rb
index 15c471c..ee55892 100644
--- a/Formula/fstar.rb
+++ b/Formula/fstar.rb
@@ -56,6 +56,7 @@ class Fstar < Formula
       modules << "#{r.name}=#{r.version}"
     end

+    system "opam", "switch", "4.02.3"
     system "opam", "install", *modules
     system "opam", "config", "exec", "--",
     "make", "-C", "src/ocaml-output/"

I ran a fresh install with the patch and it worked, but someone else should test it.

However, the correct solution to this problem is to configure the sandbox to have the right version from the start, rather than switching. opam switch takes a very long time to complete.

Even better would be if we could fix this dependency hell, but I'm not very familiar with opam, so I'm not the right person to ask.

@ilovezfs
Copy link
Contributor

Note that the fstar-on-10.12 failure has already been noted here #5488.

@vmrsss
Copy link
Author

vmrsss commented Nov 5, 2016

thanks. isn't this an obvious issue for the package manager to fix? why are they not taking it up? is there an "official" way to ask? thank you

@ilovezfs
Copy link
Contributor

ilovezfs commented Nov 5, 2016

@vmrsss I'll probably tweak it further, but just for you:

diff --git a/Formula/fstar.rb b/Formula/fstar.rb
index 15c471c..0d775c2 100644
--- a/Formula/fstar.rb
+++ b/Formula/fstar.rb
@@ -15,50 +15,24 @@ class Fstar < Formula
     sha256 "611406bfa8d13b9a6af24b066e4010b8d96dd260abec933bb215fbb180856f5e" => :mavericks
   end

-  depends_on "opam" => :build
+  depends_on "findutils" => :build
   depends_on "gmp" => :build
-  depends_on "ocaml" => :recommended
-  depends_on "z3" => :recommended
-
-  resource "ocamlfind" do
-    url "http://download.camlcity.org/download/findlib-1.5.5.tar.gz"
-    sha256 "aafaba4f7453c38347ff5269c6fd4f4c243ae2bceeeb5e10b9dab89329905946"
-  end
-
-  resource "batteries" do
-    url "https://github.com/ocaml-batteries-team/batteries-included/archive/v2.5.2.tar.gz"
-    sha256 "649038b47cdc2b7d4d4331fdb54b1e726212ce904c3472687a86aaa8d6006451"
-  end
-
-  resource "zarith" do
-    url "https://forge.ocamlcore.org/frs/download.php/1471/zarith-1.3.tgz"
-    sha256 "946687d6f032b96ab9db9661d876e39437bff783e0ad473ac463c06259b7a3d7"
-  end
-
-  resource "yojson" do
-    url "http://mjambon.com/releases/yojson/yojson-1.1.6.tar.gz"
-    sha256 "d97497f4d0694f515a9c12708eda2654dddb289b2ed567a377706e62e54c480d"
-  end
+  depends_on "gnu-sed" => :build
+  depends_on "ocaml" => :build
+  depends_on "opam" => :build
+  depends_on "pkg-config" => :build
+  depends_on "z3"

   def install
     ENV.deparallelize # Not related to F* : OCaml parallelization

     opamroot = buildpath/"opamroot"
     ENV["OPAMROOT"] = opamroot
-    ENV["OPAMYES"] = "1"
+    ENV["OPAMYES"] = "true"
     system "opam", "init", "--no-setup"
-    archives = opamroot/"repo/default/archives"
-    modules = []
-    resources.each do |r|
-      r.verify_download_integrity(r.fetch)
-      original_name = File.basename(r.url)
-      cp r.cached_download, archives/original_name
-      modules << "#{r.name}=#{r.version}"
-    end
-
-    system "opam", "install", *modules
-    system "opam", "config", "exec", "--",
-    "make", "-C", "src/ocaml-output/"
+    system "opam", "install", "batteries", "sqlite3", "fileutils", "stdint", "zarith", "yojson"
+    system "opam", "config", "exec", "--", "ocamlfind", "ocamlopt", "-config"
+    system "opam", "config", "exec", "--", "make", "-C", "src/ocaml-output/"

     bin.install "src/ocaml-output/fstar.exe"

@ilovezfs ilovezfs removed the help wanted Task(s) needing PRs from the community or maintainers label Nov 5, 2016
@ilovezfs ilovezfs changed the title fstar failed to build on 10.12 fstar fails to build Nov 5, 2016
@ilovezfs
Copy link
Contributor

ilovezfs commented Nov 5, 2016

Fixed by #6635 in 0e66557

@ilovezfs ilovezfs closed this as completed Nov 5, 2016
@vmrsss
Copy link
Author

vmrsss commented Nov 6, 2016

thank you!

@Homebrew Homebrew locked and limited conversation to collaborators May 4, 2018
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
ocaml OCaml use is a significant feature of the PR or issue
Projects
None yet
Development

No branches or pull requests

4 participants