Skip to content

Commit 8bdb5b4

Browse files
committed
Preface: edit System Requirements for Idris
1 parent 1fbf7ff commit 8bdb5b4

File tree

1 file changed

+21
-13
lines changed

1 file changed

+21
-13
lines changed

src/Preface.lidr

Lines changed: 21 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -314,24 +314,32 @@ paths through the material can be found in the file `deps.html`.
314314
315315
=== System Requirements
316316
317-
\todo[inline]{Rewrite this for Idris}
317+
Idris runs on Windows, Linux, and macOS. You will need:
318318
319-
Coq runs on Windows, Linux, and OS X. You will need:
319+
- A current installation of Idris, available from
320+
\href{https://www.idris-lang.org/}{the Idris home page}. Everything should
321+
work with version 1.0. (Version 1.1.0 should work, but hasn't been tested by
322+
the Idris translation maintainers.)
320323
321-
- A current installation of Coq, available from the Coq home page. Everything
322-
should work with version 8.4. (Version 8.5 will _not_ work, due to a few
323-
incompatible changes in Coq between 8.4 and 8.5.)
324+
- A supported editor for interacting with Idris. Currently, there are (at
325+
least) five choices:
324326
325-
- An IDE for interacting with Coq. Currently, there are two choices:
327+
- \href{https://github.com/idris-hackers/atom-language-idris}{atom-language-idris}:
328+
An Idris Mode for Atom.io
326329
327-
- Proof General is an Emacs-based IDE. It tends to be preferred by users who
328-
are already comfortable with Emacs. It requires a separate installation
329-
(google "Proof General").
330+
- \href{https://github.com/idris-hackers/idris-mode}{idris-mode}:
331+
Idris syntax highlighting, compiler-supported editing, interactive REPL
332+
and more things for Emacs
330333
331-
- CoqIDE is a simpler stand-alone IDE. It is distributed with Coq, so it
332-
should "just work" once you have Coq installed. It can also be compiled
333-
from scratch, but on some platforms this may involve installing additional
334-
packages for GUI libraries and such.
334+
- \href{https://github.com/idris-hackers/idris-sublime}{idris-sublime}:
335+
A Plugin to use Idris with Sublime
336+
337+
- \href{https://github.com/idris-hackers/idris-vim}{idris-vim}:
338+
Idris mode for vim
339+
340+
- \href{https://github.com/zjhmale/vscode-idris}{idris-vscode}:
341+
Idris for Visual Studio Code
342+
\url{https://marketplace.visualstudio.com/items?itemName=zjhmale.Idris}
335343
336344
=== Exercises
337345

0 commit comments

Comments
 (0)