idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity
3,384 Commits 6 Branches 9 Tags 115 MiB
9f93d4c1ec
Commit Graph

254 Commits

Author SHA1 Message Date
Edwin Brady
a0cfa28621 Update version numbers 2021-06-23 16:15:21 +01:00
zseri
c760812b59 fix #1514 (Broken doc in the theorem proving part of Idris2) 2021-06-22 14:42:54 +02:00
Robert Wright
a8264f8f05 Add ability to extend RefC backend to create further backends 2021-06-18 16:59:35 +01:00
Alissa Tung
41c3fd2632
[docs] ind-ind ind-rec rec-rec in style of fwddecl (#1558) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-06-16 16:20:11 +01:00
Robert Wright
1875f62248 Remove freeBuffer function 
Each backend is now responsible for freeing Buffers in the same way as other objects
 2021-06-14 15:06:44 +01:00
Robert Wright
c63f25dac2 Distinguish common C and RefC FFI calls 2021-06-14 15:06:44 +01:00
Denis Buzdalov
2a4197e909
[ doc ] Some documentation on := syntax of let bindings (#1487) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-06-03 16:49:31 +01:00
Jan de Muijnck-Hughes
692054516e
A rough dump of how to debug idris2's workings. (#1464) 2021-05-26 10:19:40 +01:00
Kamiλ Shakirov
ad656a8d47
Remove realpath (#1457) 2021-05-25 11:01:28 +01:00
Nick Drozd
dc5c3963e4 Update Emacs idris-mode doc 2021-05-22 16:19:17 -05:00
Ohad Kammar
618c71477e
[ close #1384 ] built-in Snoc-lists [< 1, 2, 3 ] (#1383) 2021-05-20 12:56:25 +01:00
Zoe Stafford
7fe8c42116
[ builtin ] O(1) integerToNat for any 'Nat'-like type (#1403) 2021-05-13 18:44:24 +01:00
Zoe Stafford
8a7aeca1b0
[ builtin ] O(1) natToInteger for any 'Nat'-like type (#1363) 2021-05-10 12:14:19 +01:00
Ohad Kammar
e58bcfc7ef
Semantic highlighting (#1335) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-05-10 09:05:43 +01:00
Ruslan Feizerakhmanov
51184c156d [doc] Interface constructors 2021-05-08 11:36:12 +03:00
Raoul Hidalgo Charman
2c8f2483de Update docs to reflect usage of >> in do syntax 2021-05-01 15:18:49 +01:00
Edwin Brady
6d37471ccc Add --profile flag 
If set, when compiling this generates an executable which generates
profiling data. Currently supported by Racket and Chez, other backends
silently ignore it.
 2021-04-29 15:18:59 +01:00
Zoe Stafford
c75b3f7f14
Add Agda-like builtins (#1253) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-22 13:08:32 +01:00
Ohad Kammar
e130ee33f4 [doc] Minor tweaks to installation instructions 2021-04-19 14:24:06 +01:00
Georgi Lyubenov
0bbc3cf42b Update section on custom code gens in updates.rst 
It is now possible to write your own code generation.
 2021-04-07 16:28:46 +01:00
Andor Penzes
b0d6793cfb
[ doc ] Custom backend cookbook (#1237) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-07 16:24:39 +01:00
Kamil Shakirov
43d0b94567 [ docs ] Update Control.App docs 2021-03-31 18:01:39 +01:00
Kamil Shakirov
ca071a96c3 [ docs ] Update Control.App docs 2021-03-10 23:30:46 +00:00
Stefan Höck
8d4321eb9a
Add Data.Bits to base (#1033) 2021-03-04 20:59:56 +00:00
Denis Buzdalov
a74d8e6c2d [ doc ] Documentation of package lookup was clarified a bit. 2021-03-04 14:51:57 +00:00
Denis Buzdalov
ae43ff688c [ doc ] Orphaned todo block was removed 2021-03-01 14:50:31 +00:00
Edwin Brady
03b8198560 Add environment variables to documentation 2021-02-28 14:18:19 +00:00
Edwin Brady
d617290dd5 Update packaging documentation 2021-02-27 18:20:55 +00:00
Kamil Shakirov
3ec64a7cfc [docs] Mention external code generators 2021-02-26 13:18:45 +00:00
Jan de Muijnck-Hughes
bf2e15699e updated protocol with versioning and version changes. 2021-02-25 10:18:47 +00:00
Jan de Muijnck-Hughes
4d36b754c6 initial dump of IDE protocol documentation from Idris1. 2021-02-25 10:18:47 +00:00
Guillaume ALLAIS
da88b80481 [ fix #794 ] missing cases in recoverable 2021-02-24 20:25:04 +00:00
Dong Tsing-hsuen
505224e9fc
[ typo ] Enum -> Range (#1099) 2021-02-22 10:05:08 +00:00
Nil Geisweiller
bb25050746 Remove redundant to 2021-02-18 09:56:42 +00:00
gemmaro
5eafe11de7 A tiny doc fix: the program name was idris 2021-02-17 09:30:52 +00:00
Nil Geisweiller
f390fba766 Rename Sotrable to Storable 2021-02-16 09:51:44 +00:00
Guillaume ALLAIS
5aa4262792 [ fix ] some of the docs 2021-02-10 00:37:06 +00:00
Denis Buzdalov
052e3f0908 A tiny doc fix: heading line was not long enough. 2021-02-04 16:48:19 +00:00
Stiopa Koltsov
e6447e7515 Check docs in CI 2021-02-04 14:59:14 +00:00
Nil Geisweiller
0a24821429 Fix documentation link in typesfuns tutorial 2021-02-02 11:04:44 +00:00
stefan-hoeck
29a6aa45e0 fixed whitespace for *.md and .rst files 2021-01-22 15:08:49 +00:00
stefan-hoeck
1218abfa18 fixed whitespace for *.py files 2021-01-22 15:08:49 +00:00
Edwin Brady
79a89a046f FAQ addition 2021-01-13 16:31:20 +00:00
Edwin Brady
b35268b774 Update version numbers and bootstrap code 2021-01-13 12:46:06 +00:00
Michael Messer
a1f3424ab8 Remove lamdaRequire 2021-01-05 16:30:11 +00:00
Jonathan Lorimer
4bc1d17506 add command history faq 2020-12-29 16:52:04 -05:00
Jonathan Lorimer
47df67af16 add rlwrap docs 2020-12-29 14:55:00 -05:00
raptazure
043faf8baf docs: fix grammar 2020-12-16 10:02:34 +00:00
G. Allais
3f6b99e979
[ fix #657 ] RigCount for interface parameters (#808) 2020-12-11 11:58:26 +00:00
Denis Buzdalov
a1b624a3bc Tiny fix of the formatting in the recently added documentation. 2020-12-08 08:56:38 +00:00
Ruslan Feizerahmanov
1dba32a0c4
[ doc ] new application syntax (#820) 2020-12-07 18:59:49 +00:00
Jan de Muijnck-Hughes
3a6e779acf Extended Literate support to include LaTeX. 2020-12-07 14:54:35 +00:00
Jan de Muijnck-Hughes
9c5198cde3 Fixed docs and improved Literate mode. 
+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
 2020-12-07 14:54:35 +00:00
Andor Penzes
aeab632c7e [doc] JS FFI examples. 2020-12-06 19:07:34 +00:00
Edwin Brady
bfea7d785a
Merge pull request #766 from mokshasoft/gambit-cg 
Gambit cg
 2020-12-04 15:51:22 +00:00
Jonas Claesson
924166a911 Add GAMBIT_GSC_BACKEND and C directive to Gambit docs 2020-12-03 18:02:54 +01:00
Cotton Hou
52ba8b00a6 Fix broken url to JS code gen page in faq 2020-11-01 11:07:06 +00:00
DavidTheBugWriter
b4b800e967 Update starting.rst 
Hellow world execute fails on Macos as it doesn't have realpath by default & one needs to install it with coreutils first.
 2020-10-24 12:35:13 +01:00
Edwin Brady
3007b5a99d Generate an executable via CC 
This builds a .o from the generated C, and statically links with the
libidris2_support library. It doesn't yet dynamically link with any
additional libraries.
 2020-10-11 18:35:51 +01:00
Matus Tejiscak
668762e693 Merge branch 'revert-projections' into master 2020-10-11 08:12:00 +02:00
Brandon Elam Barker
28cf2a3083 Making "functional dependencies" easier to find 2020-09-30 19:33:02 +01:00
Brandon Elam Barker
9aefc9f60c Updating info about backends in FAQ 2020-09-23 18:32:46 +01:00
MarcelineVQ
19bad79847 change runState's to take state first to allow easier use 2020-09-15 09:23:41 +01:00
MarcelineVQ
5acb306bf9 add ability to target scheme flavor in foreign specifiers 
There's some missing flexibility in how foreign specifiers can be used with
scheme that is addressed here with minimal changes to how scheme specifiers
are read. This opens up uses for users that they otherwise would have had
to modify the compiler's support files to accomplish.
 2020-09-13 10:10:53 +01:00
Matus Tejiscak
d98686d4f8 Update doc, fix tests. 2020-09-10 20:33:08 +02:00
Matus Tejiscak
e491e2969e Re-introduce %prefix_record_projections. 2020-09-10 20:18:51 +02:00
Matus Tejiscak
aebe3c19d9 Revert postfix dotted application. 2020-09-10 19:00:48 +02:00
stasoid
a70446c8ff
Clarify what 'invisible' code means in literate.rst (#615) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: stasoid <x@x.x>
 2020-08-31 18:37:48 +01:00
Donald Thompson
ec65f101fc Update typedd.rst 
Added implicit argument to exercise 5 of section 4.2
 2020-08-31 18:37:14 +01:00
lodi
3b49b10832
add extraRuntime option for Scheme backends (#578) 2020-08-21 09:34:57 +01:00
Kamil Shakirov
8544e80076 Use the same naming convention for foreign primitives 2020-08-19 14:05:28 +01:00
Fangyi Zhou
df4c454f4e Typo in updates.rst 2020-08-17 19:33:14 +01:00
Edwin Brady
0d81e3b59c Version increment 2020-08-16 12:06:38 +01:00
Thomas Dziedzic
a1739a69a0
Update app docs (#537) 2020-08-10 10:05:23 +01:00
Thomas Dziedzic
f337698608 update ffi docs with Bits* 2020-08-08 12:48:46 +01:00
Giuseppe Lomurno
627d340b62 Docs for overloaded literals 2020-08-05 11:51:27 +02:00
Rui Barreiro
736b91b118 ups 2020-07-24 20:23:34 +01:00
Rui Barreiro
7e27d03ef9
Update docs/source/backends/javascript.rst 
Co-authored-by: memoryruins <memoryruinsmusic@gmail.com>
 2020-07-24 19:10:11 +01:00
Rui Barreiro
503c513aef
Update docs/source/backends/javascript.rst 
Co-authored-by: memoryruins <memoryruinsmusic@gmail.com>
 2020-07-24 19:09:47 +01:00
Rui Barreiro
99ea8f59aa
Update docs/source/backends/javascript.rst 
Co-authored-by: memoryruins <memoryruinsmusic@gmail.com>
 2020-07-24 19:09:38 +01:00
Rui Barreiro
10be065553
Update docs/source/backends/javascript.rst 
Co-authored-by: memoryruins <memoryruinsmusic@gmail.com>
 2020-07-24 19:09:27 +01:00
Rui Barreiro
211a5e55cc javascript codegen minimal doc 2020-07-24 18:28:20 +01:00
elsanussi-s-mneina
19bced702d
fix typo: "lowercase later" to "lowercase letter" 
I think this is a spelling mistake.
 2020-07-15 09:50:19 -04:00
Christian Rasmussen
6211922960
%auto_implicit has been renamed to %unbound_implicits 2020-07-11 02:33:23 +02:00
Denis Buzdalov
0aeadbad19 Recently added implementation were slightly fixed and nicened. 2020-07-10 17:28:49 +01:00
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
Edwin Brady
3859f60d7a Merge remote-tracking branch 'upstream/master' 2020-05-25 09:11:54 +01:00
Edwin Brady
2206692533 Some documentation updates 
Remove things from CONTRIBUTING that are done, and initial App
documentation (though it could use more examples).
 2020-05-25 09:03:08 +01:00
Edwin Brady
7881dfd110
Merge pull request #146 from edwinb/docupdates 
Small documentation updates
 2020-05-25 01:22:40 +01:00
Edwin Brady
9c5594223e Small documentation updates 2020-05-25 01:02:07 +01:00
Edwin Brady
508b136866
Merge branch 'master' into add-warnings-to-rtd 2020-05-25 00:38:22 +01:00
Fabián Heredia Montiel
731a416043 Split Package Specific Lexer/Rules from Lexer/{Common,Source} and Refactor Idris/Package 
Co-authored-by: Matus Tejiscak <ziman@functor.sk>
 2020-05-24 16:01:17 -05:00
Edwin Brady
498421a236 All functions now need to be covering by default 
This has caught a couple of things in the Idris 2 code base itself. Some
tests needed partial annotations too.
 2020-05-24 19:58:20 +01:00
Edwin Brady
cff5fc2625 Workaround for byte vectors in Racket 
Racket appears to have a different notion of current directory than the
system does, so we need to tell it which directory we think we're in
when reading and writing bytevectors using the scheme file functions.
 2020-05-23 21:37:31 +01:00
Jan de Muijnck-Hughes
43c5075f6e Use reST directives to make warnings and TODOs explicit in the documentation. 2020-05-23 19:57:50 +01:00
Edwin Brady
0d5c709fc6 Add IDRIS2_CG environment variable 
This allows setting code generators globally, which makes building with
alternative back ends smoother.
 2020-05-23 19:03:56 +01:00
Edwin Brady
e3df2d59b0 Tidy up Racket CG 
Instead of dumping the required dynamic libraries in the working
directly, where the executable won't necessarily find them, take the
same approach as the Chez backend and create a subdirectory for the
required runtime files and use a shell script to start up with the right
library paths.
 2020-05-23 15:18:18 +01:00
Edwin Brady
3fa4a9768f Small addition to FAQ on scheme performance 2020-05-23 12:26:05 +01:00
Edwin Brady
aeea2b80c9
Merge pull request #109 from ziman/with-disamb 
`with` expressions for name disambiguation
 2020-05-23 12:22:35 +01:00
Edwin Brady
840e020d8c Some FAQ updates 2020-05-22 21:17:37 +01:00
Matus Tejiscak
74dd653fc5 Apply the patch from idris2-boot. 2020-05-22 20:26:10 +02:00