Fix #6866: User Manual: Make Installation as Easy as Possible #7155
Conversation
A refactor of the installation section of the user manual. The overall approach is to make installation easy for beginners, making the happy path obvious, but still leave the more in-depth information for others. The main changes: 1. Start with a list of steps to get started with Agda: Step 1: Install Agda, Step 2: Install the Agda Standard Library (agda-stdlib), Step 3: Install and Configure a Text Editor for Agda. 2. Change the top-level of the installation page to be the above three steps, plus an Installation Reference section to put other information. 3. Under 'Step 1: Install Agda' give three options: Option 1: Install Agda as a Haskell Package (recommended), Option 2: Install the Development Version of Agda from Source (for advanced users), Option 3: Install Agda as a Prebuilt Package (not generally recommended). 4. Move 'Installation Flags', 'Installing multiple versions of Agda' and others to the 'Installation Reference' section. 5. Under step 1, option 1, simplify the instructions, link to GHCup to install GHC, other simplifications. Various other small fixes, including: * Remove obsolete dependencies, * Unclutter instructions where possible, moving extra info to the new reference section or note/hint/warning blocks, * Add a warning about how old the precompiled Windows binary is. * Remove reference to the `agda-mode` package which no longer exists on Debian/Ubuntu.
|
|
||
| .. code-block:: bash | ||
| .. hint:: Use GHCup's 'recommended' version unless you have a reason |
There was a problem hiding this comment.
Do we already have a policy in place that the latest released of Agda should always have been tested with ghcup's recommended version? We don't want to recommend something that would be incompatible.
There was a problem hiding this comment.
In practice, yes, we have the recommended GHC covered. (But we do not have a policy.)
| but if you ever want to install different versions of these you can use the | ||
| ``ghcup`` command, e.g. ``ghcup list`` to see what is available, then e.g. | ||
| ``ghcup install cabal latest`` to switch to the latest version of Cabal. | ||
|
|
||
| apt-get install zlib1g-dev libncurses5-dev | ||
| .. note:: A popular alternative to Cabal is `Stack <https://www.haskellstack.org>`_, | ||
| which can also be installed using GHCup, or using its own installer. When using | ||
| Stack it should suffice to replace ``cabal`` with ``stack`` in the following | ||
| instructions, e.g. ``stack install Agda``. |
There was a problem hiding this comment.
This is too ghcup centric IMO, and I don't think we want to start introducing even more choices for users. I would drop any mention of unnecessary ghcup commands and stack altogether.
|
|
||
| cabal v2-install --package-env agda --lib Agda ieee754 | ||
| **Warning** : Depending on the system, prebuilt packages may not be | ||
| the latest release. See https://repology.org/project/agda/versions. |
There was a problem hiding this comment.
When I click on this link (at least in the github interface), I land on the "versions." page which naturally does not exist. We should check the built docs do not actually include the final full stop as part of the URL.
| able to install these files for you. For instance, on Debian or Ubuntu | ||
| it should suffice to run | ||
| Follow the `GHCup installation instructions <https://www.haskell.org/ghcup/>`_ | ||
| to install GHC and Cabal (see also :ref:`zlib-ncurses` and :ref:`ghc-versions`). |
There was a problem hiding this comment.
The zlib ncurses install should be highlighted as a separate step. Otherwise I can guarantee we'll get people saying the build fails because the dependencies are not properly installed.
|
|
||
| .. code-block:: bash | ||
| cabal update | ||
| cabal install Agda |
There was a problem hiding this comment.
Do we not need to install alex and happy first? IME it still seemed to be flaky whether cabal would complain about their absence or not.
A refactor of the installation section of the user manual. The overall approach is to make installation easy for beginners, making the happy path obvious, but still leave the more in-depth information for others.
The main changes:
Various other small fixes, including:
agda-modepackage which no longer exists on Debian/Ubuntu.Note that I didn't fix a couple of things I intended to in the original issue: