homebrew install instructions don't work any more?

[sourcefrog]

I'm trying to follow instructions from https://github.com/FStarLang/FStar/blob/master/INSTALL.md#homebrew-formula-for-mac-os-x

> brew update
> brew --version
Homebrew 2.2.10
Homebrew/homebrew-core (git revision 516c4; last commit 2020-03-12)
Homebrew/homebrew-cask (git revision 84a32; last commit 2020-03-12)
> brew install fstar
Error: No available formula with the name "fstar"
==> Searching for a previously deleted formula (in the last month)...
Warning: homebrew/core is shallow clone. To get complete history run:
  git -C "$(brew --repo homebrew/core)" fetch --unshallow

Error: No previously deleted formula found.
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching taps...
==> Searching taps on GitHub...
Error: No formulae found in taps.

[YumaVlaicu]

It happened to me, too.
I installed instead by opam

$ brew install fstar
Error: No available formula with the name "fstar"
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching taps...
==> Searching taps on GitHub...
Error: No formulae found in taps.

$ opam switch create 4.07.1 # fstar needs ocaml whose version is less than 4.08.0
$ opam pin add fstar --dev-repo # Automatically installed

[momohatt]

I ran into the same problem. Seems that they deleted the formula recently:
Homebrew/homebrew-core#49745

[catalin-hritcu]

I've removed the broken reference to the Homebrew formula from the documentation. This is not the perfect fix for this issue, but a better fix would require a brave volunteer to bring the Homebrew formula back to life and keep maintaining it.

[catalin-hritcu]

FWIW London Fuller (@landonf) has been keeping the MacPorts for F*/KreMLin up-to-date:
https://ports.macports.org/port/fstar-devel/summary
https://ports.macports.org/port/kremlin-devel/summary

[catalin-hritcu]

Looking at the link that @momohatt sent above (Homebrew/homebrew-core#49745), the reason they deleted our Homebrew formula is our dependency on camlp4/ulex (#1792), which is not easy to fix, but we'll eventually have to do it or be stuck with OCaml 4.09 forever.

[catalin-hritcu]

Don't expect any miracles, but still pinging @beurdouche who's been the original maintainer of the Homebrew formula.

[beurdouche]

I wasn’t aware of this problem prior deletion unfortunately. The homebrew formula was quite useful for many users... What I see as a potential alternative to the F* formula in the core homebrew repo is to have our own tap for it. Which makes installing F* a two liners on OSX. brew tap FStarLang/brew brew install fstar Or something like this. I have to look if we can do this easily and if we are interested in doing so... Will get back when possible.

[catalin-hritcu]

"Having our own tap" would indeed be cool, if possible :)

[jasonhemann]

@beurdouche Did you at one point have a separate tap for fstar ? What happened to it / why did you move away from that model before?