mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-08-17 09:10:33 +03:00
line length
This commit is contained in:
parent
a409f11d39
commit
323f1d0186
11
INSTALL.md
11
INSTALL.md
@ -9,7 +9,8 @@
|
||||
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.
|
||||
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
|
||||
@ -35,12 +36,12 @@ code. 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.
|
||||
|
||||
|
10
README.md
10
README.md
@ -16,12 +16,18 @@ The [wiki](https://github.com/idris-lang/Idris2/wiki) lists a number of useful r
|
||||
|
||||
## Things still missing
|
||||
|
||||
+ Cumulativity (currently `Type : Type`. Bear that in mind when you think you've proved something)
|
||||
+ Cumulativity (currently `Type : Type`. Bear that in mind when you think
|
||||
you've proved something)
|
||||
+ `rewrite` doesn't yet work on dependent types
|
||||
|
||||
## Contributions wanted
|
||||
|
||||
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.
|
||||
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.
|
||||
|
||||
[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>
|
||||
|
Loading…
Reference in New Issue
Block a user