Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #280
Closed
Open
Issue created Dec 16, 2019 by Jules Jacobs@julesContributor

Documentation for installation on OS X

Perhaps there could be an Install.md that describes the installation process to install Coq, Iris, and an IDE for Coq on OS X (and other platforms). Not everything works well on OS X. CoqIDE is extremely slow, for instance, and the main Coq extension for VS code does not work well, and OS X has an old version of Make that fails sometimes. VS Code + the maximedenes.vscoq for Coq + oijaz.unicode-latex for unicode input works reasonably well. What I eventually did was something like:

/usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
brew update
brew install make
brew install opam
opam init
eval $(opam env)
opam install coq
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-iris
brew install visual-studio-code
code --install-extension maximedenes.vscoq
code --install-extension oijaz.unicode-latex

A complete recipe like that might save new people a lot of time.

Edited Dec 16, 2019 by Jules Jacobs
Assignee
Assign to
Time tracking