coq-HoTT won't compile on OS X

[GallagherCommaJack]

Whenever I try to install coq-HoTT, I get this error:

File "parsing/compat.ml", line 130, characters 48-54:
Error: This expression has type 'a Ploc.vala
       but an expression was expected of type MLast.str_item list

Since there isn't some massive issue filled with urgent commits about it not compiling, I'm guessing it's some flaw on my system, but I'm not sure so I figured I'd post to see if anyone else has had this issue.

[JasonGross]

As a work-around, you can install Coq 8.5 beta 1 from the official website, or install coq-hott from opam.

[GallagherCommaJack]

Installing coq-hott from opam is its own issue, as it comes bundled with coqide and opam can't seem to detect the installation of lablgtk, though I'll give the binary a try.

[mikeshulman]

Can this be closed now that we work with the released Coq 8.5?