idris-lang · andrevidela · Nov 15, 2023 · Sep 19, 2022 · Nov 9, 2023 · Nov 9, 2023
diff --git a/INSTALL.md b/INSTALL.md
@@ -1,12 +1,34 @@
-# Installing
+# Installation
 
+- [Installing with a package manager](#installing-with-a-package-manager)
 - [Installing from source](#installing-from-source)
-- [Installing from a package manager](#installing-from-a-package-manager)
+- [Installing Chez Scheme on Apple Silicon](#installing-chez-scheme-on-apple-silicon)
+
+## Installing with a package manager
+
+You can install Idris 2 with any one of a number of package managers.
+
+### Installing with [Pack](https://github.com/stefan-hoeck/idris2-pack)
+Pack comes with an installation of Idris 2, so you just need to install Pack.
+See [the installation instructions](https://github.com/stefan-hoeck/idris2-pack/blob/main/INSTALL.md)
+on GitHub.
+### Installing with [Homebrew](https://brew.sh/)
+```sh
+brew install idris2
+```
+### Installing with [Nix](https://nixos.org/features.html)
+```sh
+nix-env -i idris2
+```
+### Installing with [Nix Flakes](https://nixos.wiki/wiki/Flakes)
+```sh
+nix profile install github:idris-lang/Idris2
+```
 
 ## Installing from source
 
-The easiest way to install is via the existing generated Scheme code.
-The requirements are:
+The easiest way to install from source is via the existing generated Scheme
+code. The requirements are:
 
 - A Scheme compiler; either Chez Scheme (default), or Racket.
 - `bash`, `GNU make`, `gcc` or `clang`, `sha256sum` and `GMP`.  On Linux, you probably already
@@ -15,12 +37,12 @@ The requirements are:
   `brew install coreutils gmp` and on OpenBSD, with the `pkg_add coreutils
   bash gmake gmp` command. You specifically need the dev GMP library, which
   means on some systems the package you need to install will be named
-  something more like `libgmp3-dev`. macOS ships with `clang` whereas `gcc` is more
-  common for other \*nix distributions.
+  something more like `libgmp3-dev`. macOS ships with `clang` whereas `gcc` is
+  more common for other \*nix distributions.
 
 On Windows, it has been reported that installing via `MSYS2` works
-[MSYS2](https://www.msys2.org/). On Windows older than Windows 8, you may need to
-set an environment variable `OLD_WIN=1` or modify it in `config.mk`.
+[MSYS2](https://www.msys2.org/). On Windows older than Windows 8, you may need
+to set an environment variable `OLD_WIN=1` or modify it in `config.mk`.
 
 On Raspberry Pi, you can bootstrap via Racket.
 
@@ -151,35 +173,6 @@ bootstrapping via Chez Scheme, or while running the tests when bootstrapping via
 Racket, then your copy of Chez Scheme was built without thread support. Pass
 `--threads` to `./configure` while building Chez Scheme to correct the issue.
 
-## Installing from a package manager
-
-### Installing using Homebrew
-
-If you are Homebrew user you can install Idris 2 together with all the requirements
-by running the following command:
-
-```sh
-brew install idris2
-```
-
-### Installing from nix
-
-If you are a [nix](https://nixos.org/features.html) user you can install Idris
-2 together with all the requirements by running the following command:
-
-```sh
-nix-env -i idris2
-```
-
-### Install from nix flakes
-
-If you are a [nix flakes](https://nixos.wiki/wiki/Flakes) user you can install
-Idris 2 together with all the requirements by running the following command:
-
-```sh
-nix profile install github:idris-lang/Idris2
-```
-
 ## Running in text editor
 
 ### Run on emacs using nix flakes
@@ -191,7 +184,7 @@ Idris 2 in emacs by running the following command:
 nix run github:idris-lang/Idris2#emacs-with-idris idrisCode.idr
 ```
 
-### Installing Chez Scheme on Apple Silicon
+## Installing Chez Scheme on Apple Silicon
 
 The official version of chez scheme does not yet support Apple Silicon. So, on
 macOS with Apple Silicon (e.g. M1 and M2 macs), you will need to build and install
@@ -209,4 +202,3 @@ make ${arch}.bootquick
 make
 sudo make install
 ```
-
diff --git a/README.md b/README.md
@@ -1,119 +1,38 @@
-Idris 2
-=======
+# Idris 2
 
 [![Documentation Status](https://readthedocs.org/projects/idris2/badge/?version=latest)](https://idris2.readthedocs.io/en/latest/?badge=latest)
 [![Build Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-idris2-and-libs.yml/badge.svg?branch=main)](https://github.com/idris-lang/Idris2/actions/workflows/ci-idris2-and-libs.yml?query=branch%3Amain)
 
 [Idris 2](https://idris-lang.org/) is a purely functional programming language
 with first class types.
 
-For full installation instructions, see [INSTALL.md](INSTALL.md).  Briefly, if
-you have Chez Scheme installed, with the executable name `chez`, type:
+For installation instructions, see [INSTALL.md](INSTALL.md).
 
-* `make bootstrap SCHEME=chez`
-* `make install`
+The [wiki](https://github.com/idris-lang/Idris2/wiki) lists a number of useful
+resources, in particular
 
-You may need to change `chez` to be the local name of your Chez Scheme. This
-is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the
-version). On a modern desktop machine, this process (including tests)
-should take less than 5 minutes.
++ [What's changed since Idris 1](https://idris2.readthedocs.io/en/latest/updates/updates.html)
++ [Resources for learning Idris](https://github.com/idris-lang/Idris2/wiki/Resources),
+  including [official talks](https://github.com/idris-lang/Idris2/wiki/Resources#official-talks)
+  that showcase its capabilities
++ [Editor support](https://github.com/idris-lang/Idris2/wiki/Editor-Support)
 
-Idris 2 is mostly backward compatible with Idris 1, with some minor exceptions.
-The most notable user visible differences, which might cause Idris 1 programs
-to fail to type check, are:
+## Things still missing
 
-+ Unbound implicit arguments are always erased, so it is a type error to
-  attempt to pattern match on one.
-+ Simplified resolution of ambiguous names, which might mean you need to
-  explicitly disambiguate more often. As a general rule, Idris 2 will be able
-  to disambiguate between names which have different concrete return types
-  (such as data constructors), or which have different concrete argument
-  types (such as record projections). It may struggle to resolve ambiguities
-  if one name requires an interface to be resolved.
-+ The `cong` function now takes its congruence explicitly as its first argument.
-+ Minor differences in the meaning of export modifiers `private`, `export`,
-  and `public export`, which now refer to visibility of names from other
-  *namespaces* rather than visibility from other *files*.
-+ Module names must match the filename in which they are defined (unless
-  the module's name is "Main").
-+ Anything which uses a `%language` pragma in Idris 1 is likely to be different.
-  Notably, elaborator reflection will exist, but most likely in a slightly
-  different form because the internal details of the elaborator are different.
-+ The `Prelude` is much smaller (and easier to replace with an alternative).
-  Command-line option `--no-prelude` can be used to not implicitly import `Prelude`.
-+ `let x = val in e` no longer computes with `x` in `e`, instead being
-  essentially equivalent to `(\x => e) val`. This is to make the
-  behaviour of `let` consistent in the presence of `case` and `with` (where
-  it is hard to push the computation inside the `case`/`with` efficiently).
-  Instead, you can define functions locally with `let`, which do have
-  computational force, as follows:
++ Cumulativity (currently `Type : Type`. Bear that in mind when you think
+  you've proved something)
++ `rewrite` doesn't yet work on dependent types
 
-      let x : ?
-          x = val in
-          e
+## Contributions wanted
 
-Watch this space for more details and the rationale for the changes, as I
-get around to writing it...
+If you want to learn more about Idris, contributing to the compiler could be
+one way to do so. The [contribution guidelines](CONTRIBUTING.md) outline
+the process. Having read that, choose a [good first issue][1] or have a look at
+the [contributions wanted][2] for something more involved. This [map][3] should
+help you find your way around the source code. See [the wiki page][4]
+for more details.
 
-Summary of new features:
-
-+ A core language based on "Quantitative Type Theory" which allows explicit
-  annotation of erased types, and linear types.
-+ `let` bindings are now more expressive, and can be used to define pattern
-  matching functions locally.
-+ Names which are in scope in a type are also always in scope in the body of
-  the corresponding definition.
-+ Better inference. Holes are global to a source file, rather than local to
-  a definition, meaning that some holes can be left in function types to be
-  inferred by the type checker. This also gives better inference for the types
-  of `case` expressions, and means fewer annotations are needed in interface
-  declarations.
-+ Better type checker implementation which minimises the need for compile
-  time evaluation.
-+ New Chez Scheme based backend which both compiles and runs faster than the
-  default Idris 1 backend. (Also, optionally, Racket and Gambit can be used
-  as targets).
-+ Everything works faster :).
-
-A significant change in the implementation is that there is an intermediate
-language `TTImp`, which is essentially a desugared Idris, and is cleanly
-separated from the high level language which means it is potentially usable
-as a core language for other high level syntaxes.
-
-JavaScript
-----------
-The JavaScript codegen uses the new BigInt, hence Node.js 10.4 or higher is required.
-
-Editor Plugins
---------------
-The [wiki lists the current plugins available for common text editors](
-https://github.com/idris-lang/Idris2/wiki/Editor-Support)
-and their features.
-
-Things still missing
---------------------
-
-+ Cumulativity (so we currently have Type : Type! Bear that in mind when you
-  think you've proved something :))
-+ 'rewrite' doesn't yet work on dependent types
-
-Contributions wanted
--------------------
-
-+ [Contribution guidelines](CONTRIBUTING.md)
-+ [Good first issues](https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22)
-+ [Contributors wanted](https://github.com/idris-lang/Idris2/wiki/What-Contributions-are-Needed)
-
-If you want to learn about Idris more, contributing to the compiler could be one
-way to do so. Just select one good first issue and ask about it on the [Discord](https://discord.gg/UX68fDs2jc) channel.
-
-Talks
------
-
-[![Edwin Brady Tells Us What's New in Idris 2 (Berlin Functional Programming Group)](https://img.youtube.com/vi/nbClauMCeds/0.jpg)](https://www.youtube.com/watch?v=nbClauMCeds "Edwin Brady Tells Us What's New in Idris 2 (Berlin Functional Programming Group)")
-
-[![Scheme Workshop Keynote (ACM SIGPLAN)](https://img.youtube.com/vi/h9YAOaBWuIk/0.jpg)](https://www.youtube.com/watch?v=h9YAOaBWuIk "Scheme Workshop Keynote (ACM SIGPLAN)")
-
-[![Idris 2 - Type-driven Development of Idris (Curry On - London 2019)](https://img.youtube.com/vi/DRq2NgeFcO0/0.jpg)](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")
-
-[![Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)](https://img.youtube.com/vi/mOtKD7ml0NU/0.jpg)](https://www.youtube.com/watch?v=mOtKD7ml0NU "Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)")
+[1]: <https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22>
+[2]: <https://github.com/idris-lang/Idris2/wiki/What-Contributions-are-Needed>
+[3]: <https://github.com/idris-lang/Idris2/wiki/Map-of-the-Source-Code>
+[4]: <https://github.com/idris-lang/Idris2/wiki/Getting-Started-with-Compiler-Development>
diff --git a/docs/source/backends/javascript.rst b/docs/source/backends/javascript.rst
@@ -8,6 +8,7 @@ output an HTML file will also generate a basic HTML document with the
 generated code inside a ``<script>`` tag; the other distinction is on the ffi
 that will be explained below.
 
+**Note**: The JavaScript codegen uses the new BigInt, hence Node.js 10.4 or higher is required.
 
 Javascript FFI Specifiers
 =========================