mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-08-17 09:10:33 +03:00
refactor README and installation instructions
This commit is contained in:
Joel Berkeley
parent
1aff26e94c
commit
c4b3069a6f
73
INSTALL.md
73
INSTALL.md
@ -1,12 +1,41 @@
|
||||
# Installing
|
||||
# Installation
|
||||
|
||||
- [Installing from source](#installing-from-source)
|
||||
- [Installing from a package manager](#installing-from-a-package-manager)
|
||||
- [Install with a package manager](#install-with-a-package-manager)
|
||||
- [Install with Pack](#install-with-pack)
|
||||
- [Install with Homebrew](#install-with-homebrew)
|
||||
- [Install with Nix](#install-with-nix)
|
||||
- [Install with Nix Flakes](#install-with-nix-flakes)
|
||||
- [Install from source](#install-from-source)
|
||||
- [Install Chez Scheme on Apple Silicon](#install-chez-scheme-on-apple-silicon)
|
||||
|
||||
## Installing from source
|
||||
## Install with a package manager
|
||||
|
||||
The easiest way to install is via the existing generated Scheme code.
|
||||
The requirements are:
|
||||
You can install Idris 2 with any one of a number of package managers.
|
||||
|
||||
### Install with [Pack](https://github.com/stefan-hoeck/idris2-pack/blob/main/INSTALL.md)
|
||||
Pack comes with an installation of Idris 2 so you just need to install Pack.
|
||||
Assuming you have already installed Chez Scheme, run
|
||||
```sh
|
||||
bash -c "$(curl -fsSL https://raw.githubusercontent.com/stefan-hoeck/idris2-pack/main/install.bash)"
|
||||
```
|
||||
then add `$HOME/.pack/bin` to your `$PATH` variable.
|
||||
### Install with [Homebrew](https://brew.sh/)
|
||||
```sh
|
||||
brew install idris2
|
||||
```
|
||||
### Install with [Nix](https://nixos.org/features.html)
|
||||
```sh
|
||||
nix-env -i idris2
|
||||
```
|
||||
### Install with [Nix Flakes](https://nixos.wiki/wiki/Flakes)
|
||||
```sh
|
||||
nix profile install github:idris-lang/Idris2
|
||||
```
|
||||
|
||||
## Install from source
|
||||
|
||||
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
|
||||
@ -151,35 +180,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 +191,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
|
||||
## Install 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 +209,3 @@ make ${arch}.bootquick
|
||||
make
|
||||
sudo make install
|
||||
```
|
||||
|
||||
|
||||
117
README.md
117
README.md
@ -1,5 +1,4 @@
|
||||
Idris 2
|
||||
=======
|
||||
# Idris 2
|
||||
|
||||
[](https://idris2.readthedocs.io/en/latest/?badge=latest)
|
||||
[](https://github.com/idris-lang/Idris2/actions/workflows/ci-idris2-and-libs.yml?query=branch%3Amain)
|
||||
@ -7,113 +6,19 @@ Idris 2
|
||||
[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)
|
||||
+ [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...
|
||||
|
||||
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
|
||||
-----
|
||||
|
||||
[](https://www.youtube.com/watch?v=nbClauMCeds "Edwin Brady Tells Us What's New in Idris 2 (Berlin Functional Programming Group)")
|
||||
|
||||
[](https://www.youtube.com/watch?v=h9YAOaBWuIk "Scheme Workshop Keynote (ACM SIGPLAN)")
|
||||
|
||||
[](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")
|
||||
|
||||
[](https://www.youtube.com/watch?v=mOtKD7ml0NU "Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)")
|
||||
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](https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22) or have a look at the [contributions wanted](https://github.com/idris-lang/Idris2/wiki/What-Contributions-are-Needed) for something more involved. See [the wiki page](https://github.com/idris-lang/Idris2/wiki/Getting-Started-with-Compiler-Development) for more details.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user