Commit Graph

69 Commits

Author SHA1 Message Date
Edwin Brady
da4885c4fa Fix formatting 2020-07-10 16:01:17 +01:00
Edwin Brady
874587906f A few more internal details in the docs 2020-07-10 15:59:47 +01:00
Edwin Brady
3312961b54 Fix reference id 2020-07-10 15:23:44 +01:00
Edwin Brady
56e21fa27a Add some implementation notes to the docs 2020-07-10 15:21:24 +01:00
Edwin Brady
2ab2adec0b Update JS code generator to remove RF
This name was removed in a recent patch, leading to a small conflict.
Also added a note to the CHANGELOG and a placeholder in the docs.
2020-07-08 22:40:47 +01:00
Matus Tejiscak
168e5d8a21 Update postfix projection doc. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
98e94f956e Rename record projections to postfix projections. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
4af4ae01ae Update the postfix projection doc. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
a4c59204c5 Add postfix projection sections. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
bfb56ae71a Update the doc. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
3b6d7a22e3 Remove forgotten .field from docs. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
b46064f688 Update docs and tests. 2020-07-07 21:06:35 +01:00
Tim Engler
14725dac67 Describe what is meant by "use"
I hit a roadblock trying to understand linear types, because I couldn't figure out what is meant to "use" a variable. I eventually think I figured it out, by reading "Linear types can change the world!", but it was not easy to do so. I think a better description of what "use" means would be very helpful for those unfamiliar with linear types, so I took a stab at it. Hope it helps.
2020-07-06 12:38:03 +01:00
Denis Buzdalov
066b37feb4 Tiny doc fix about combination of import public and import .. as. 2020-07-06 11:23:56 +01:00
Edwin Brady
4c5d26f050 Add note on import...as to tutorial 2020-07-04 23:30:13 +01:00
Edwin Brady
950431a9ce Note in tutorial on qualified do 2020-07-04 23:12:03 +01:00
Alex Gryzlov
afde930e7a
Vect updates (#335) 2020-07-04 11:02:04 +01:00
Christian Rasmussen
b4ba476c8a
Merge branch 'master' into add-docs-about-dirs 2020-07-01 23:51:40 +02:00
Kamil Shakirov
f094a52ba9 Update docs 2020-06-30 18:44:36 +06:00
Christian Rasmussen
3bf384860a Add documentation for sourcedir/builddir/outputdir 2020-06-28 19:56:02 +02:00
Alex Humphreys
565ede2406 Update linear.rst
Fix typo
2020-06-22 21:23:45 +01:00
Dario Vladovic
9cc1215f6c Format Homebrew install code block 2020-06-22 17:17:11 +01:00
Edwin Brady
1e6314c4cc
Merge pull request #345 from edwinb/hasio
HasIO interface for IO actions
2020-06-21 20:24:29 +01:00
TomasPuverle
833a24cb45
Updated documentation for export (#344)
Co-authored-by: Thomas Herzog <thomas-github@poto.cafe>
2020-06-21 20:17:34 +01:00
Edwin Brady
413e75b6a3 Fix documentaton error 2020-06-21 19:56:23 +01:00
Edwin Brady
dbdf7dab3d Back to HasIO, remove MonadIO
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:

- it's easier for backend authors if the type of IO operations is
  slightly less restrictive. For example, if it's in HasIO, that limits
  alternative implementations, which might be awkward for some
  alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
  be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
  instance (I have personally never encountered one - if they turns out
  to exist, again, we can revisit!)
2020-06-21 19:21:22 +01:00
Edwin Brady
1b15463746 Update libraries and docs with HasIO/MonadIO 2020-06-21 15:25:40 +01:00
Dario Vladovic
cc61d4d3d8
Add Homebrew installation instructions 2020-06-21 13:37:36 +02:00
Niklas Larsson
1780bd2aba
Add note about the default codegen 2020-06-20 22:56:35 +02:00
Christian Rasmussen
1f0ca85678 Allow overriding the build directory and the output directory
The output directory was previously called the executable directory, but I changed it because the output is not always an executable (depending on the code generator).

The code generators can now distinguish between where to place the (temporary) build files and the resulting output files.
2020-06-20 17:23:51 +02:00
Mark Barbone
59dceb857f Make reference and source agree about literate markdown 2020-06-19 10:08:47 +01:00
Kamil Shakirov
9e42eb1be1 Fix 'install-api' makefile target
When building from a clean state `src/IdrisPaths.idr` must be generated first
before installing `idris2api.ipkg`.
2020-06-18 17:19:48 +06:00
Niklas Larsson
2ec923d4f3 Add documentation 2020-06-15 16:11:08 +02:00
Edwin Brady
c9b20911e1 Add linear pair/dependent pair to the prelude
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
2020-06-12 11:18:12 +01:00
Jinwoo Lee
5eb86af435 Add some comments about TakeN in chapter 10.
The `rest` argument must be made explicit. Related to
https://github.com/idris-lang/Idris2/issues/253.
2020-06-11 14:51:06 +01:00
Edwin Brady
ca28dab1d7 Add finalisers for Racket back end
Like Chez, we also need an explicit call to the garbage collector at the
end to ensure that all the finalisers get run on exit.
2020-06-08 22:13:24 +01:00
Edwin Brady
d60feaace0 Add finalisers to Chez back end
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.

In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...

This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
2020-06-08 20:34:23 +01:00
Keller, Bryn
a5449d926e Update docs to reflect changes to ipkg format 2020-06-05 22:14:16 -07:00
Edwin Brady
3f914889b8 Add visibility rules on types
Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.
2020-05-30 17:03:15 +01:00
Niklas Larsson
4ef0cb2c15
Merge pull request #176 from MilanKral/https
replace HTTP links with HTTPS
2020-05-27 23:23:29 +02:00
Edwin Brady
c3ed22c82f
Merge pull request #165 from stephen-smith/docs-updates
Documentation Updates based on my first experiences with Idris 2
2020-05-27 22:06:53 +01:00
Boyd Stephen Smith Jr
38876800ca Mention %access specifically
(The first failure I got when trying to compile Idris 1.3.1 code with
Idris2.)
2020-05-27 12:51:41 -05:00
Milan Kral
9f78f1cddc
replace HTTP links with HTTPS 2020-05-27 14:50:05 +02:00
asdfjasdf
6d36b04c72 Possible copy-paste mistake in typesfuns.rst
In the intial code listing we currently have "x = 42" but in following listing "x == 9 * 9 + 13" returns true.
2020-05-26 10:21:58 +01:00
Boyd Stephen Smith Jr
7e23c844a8 Mention make install
README.md has that step, but this section of the documentation was
missing it.
2020-05-25 21:32:33 -05:00
Boyd Stephen Smith Jr
7816c6c5e9 Fix formatting
Someone had LaTeX on the brain instead of RST
2020-05-25 21:31:58 -05:00
Marek Labos
f691469aa9 Reword a sentence in multiplicities.rst to improve readability. 2020-05-25 14:34:04 +01:00
Marek Labos
9160d2772a Fix typo in backends/index.rst and racket/support.rkt 2020-05-25 14:02:49 +01:00
Marek Labos
fc08b361f3 Fix typo in multiplicities.rst 2020-05-25 13:58:45 +01:00
Edwin Brady
3120fcb84a Allow _ for names in pi binders
This is mostly to make it easier to write linear function types without
having to invent names for everything, which might be noisy. Also it
improves the display of linear function types when the name isn't used
in the scope.
2020-05-25 13:14:51 +01:00