@@ -314,24 +314,32 @@ paths through the material can be found in the file `deps.html`.
314
314
315
315
=== System Requirements
316
316
317
- \t odo[inline]{Rewrite this for Idris}
317
+ Idris runs on Windows, Linux, and macOS. You will need:
318
318
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.)
320
323
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:
324
326
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
326
329
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
330
333
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}
335
343
336
344
=== Exercises
337
345
0 commit comments