Commit Graph

1686 Commits

Author SHA1 Message Date
Raoul Hidalgo Charman
3e85e23638
Namespace checks for resugaring (#1161)
This avoids resugaring to the wrong type when there are user defined
symbols which conflicts with builtins such as Pair.

Changed the test linear002 which was relying on this behaviour for a
user defined Unit.

Fixes #634.
2021-03-15 13:34:54 +00:00
Michael Messer
d08c0c78b3
Change :doc to use PTerm instead of Name (#1178) 2021-03-12 09:46:46 +00:00
Kamil Shakirov
ca071a96c3 [ docs ] Update Control.App docs 2021-03-10 23:30:46 +00:00
Edwin Brady
17cdc7fa88
Merge pull request #1171 from edwinb/fix1163
Correct multiplicities when checking Pi binders
2021-03-09 18:36:08 +00:00
Mathew Polzin
06586d401a
Add a test package to the Idris 2 project (#1162) 2021-03-09 18:27:05 +00:00
Edwin Brady
04a0f5001f Correct multiplicities when checking Pi binders
We've always just used 0, which isn't correct if the function is going
to be used in a runtime pattern match. Now calculate correctly so that
we're explicit about which type level variables are used at runtime.

This might cause some programs to fail to compile, if they use functions
that calculate Pi types. The solution is to make those functions
explicitly 0 multiplicity. If that doesn't work, you may have been
accidentally trying to use compile-time only data at run time!

Fixes #1163
2021-03-09 17:23:05 +00:00
Ruslan Feizerahmanov
50c60185a7
[ auto ] Ignore hidden names in Core.Context.getSearchData (#1143)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-03-09 14:13:29 +00:00
John Mager
a8952faebc Fix package paths in for Nix 2021-03-09 11:31:25 +00:00
Ruslan Feizerakhmanov
0ef8f08594 Revert #878 (the test stays put) 2021-03-09 11:26:56 +00:00
stefan-hoeck
0fd9ed0555 [ new ] Interface implementations for Subset 2021-03-09 11:25:03 +00:00
Andy Lok
2ed2f93004
Fix multiline string literals not properly merged (#1158) 2021-03-08 11:28:19 +00:00
Donovan Crichton
8d4e7cc581
List elem extra move/rename (#1165) 2021-03-07 18:00:03 +00:00
Donovan Crichton
06c4daa9bc [ fix ] added Data.Elem.Extra to contrib.ipkg
Added the missing module path in contrib.ipkg.
2021-03-07 11:56:23 +00:00
G. Allais
1d96dd2bd7
[ refactor ] generalise open union machinery (#1157) 2021-03-05 09:28:23 +00:00
Stefan Höck
8d4321eb9a
Add Data.Bits to base (#1033) 2021-03-04 20:59:56 +00:00
Stefan Höck
4c7d0db4bc
[ fix #1148 ] Support hyphenated package names (#1151) 2021-03-04 19:09:15 +00:00
stefan-hoeck
d952741563 [new] instances for SortedMap and Set 2021-03-04 14:54:27 +00:00
Denis Buzdalov
a74d8e6c2d [ doc ] Documentation of package lookup was clarified a bit. 2021-03-04 14:51:57 +00:00
Donovan Crichton
2de2ac2e2c
[ new ] Lemmas: append preserves List membership. (#1152) 2021-03-04 14:50:10 +00:00
Edwin Brady
72b68fd813
Merge pull request #1153 from edwinb/delay-localhints
Record local hints in delayed elaborators
2021-03-03 15:57:36 +00:00
Edwin Brady
c9de4d9f9f Remove more trailing whitespace 2021-03-03 14:36:33 +00:00
Edwin Brady
6a29fab245 Remove trailing whitespace in tests
Keep the linter happy
2021-03-03 13:55:30 +00:00
Edwin Brady
6887a5f95f Record local hints in delayed elaborators
We might not have set up search problems yet when delaying an
elaborator, so we need to know what the local hints were at the point of
delay.
2021-03-03 13:49:32 +00:00
Edwin Brady
a00fc25109
Merge pull request #1146 from edwinb/fix1140
Check current holes only at end of elaboration
2021-03-01 20:51:46 +00:00
Edwin Brady
b782f82667 A bit of tidying
`when` is better than if ... else pure ()
2021-03-01 19:55:16 +00:00
Edwin Brady
58fe629d13 Add missing case in ProcessIdr 2021-03-01 19:29:14 +00:00
Edwin Brady
1d965627c9 Check current holes only at end of elaboration
Fixes #1140 - when checking holes were solved, we checked all of them,
but there may still be some open if there's a local definition.
2021-03-01 19:11:15 +00:00
Denis Buzdalov
ae43ff688c [ doc ] Orphaned todo block was removed 2021-03-01 14:50:31 +00:00
Denis Buzdalov
2bb8ff90e2 [contrib] Existing natToFinLTE was reimplemented to have 0 LT argument 2021-03-01 08:31:09 +00:00
G. Allais
cee7e38894
[ new ] Proof search from 'Applications of Applicative Proof Search' (#1093) 2021-03-01 08:29:43 +00:00
Denis Buzdalov
7a8c12771b
[ base ] A property of interaction between zipWith and index (#1128) 2021-03-01 08:29:17 +00:00
Niklas Larsson
da2ad89252
Merge pull request #910 from cypheon/createdir-permissions
Better default permissions for created directories
2021-02-28 17:04:53 +01:00
Edwin Brady
b74e1dc472
Merge pull request #1137 from edwinb/packagepath
Add IDRIS2_PACKAGE_PATH environment variable
2021-02-28 15:38:32 +00:00
Edwin Brady
46f994e4c6 Update CHANGELOG 2021-02-28 14:48:37 +00:00
Edwin Brady
03b8198560 Add environment variables to documentation 2021-02-28 14:18:19 +00:00
Edwin Brady
ebbc123b85 Add IDRIS2_PACKAGE_PATH environment variable
This tells Idris where to look for packages in addition to the default
places (under $PREFIX and ./depends/). This should allow package
managers a bit more flexibility.
2021-02-28 14:06:10 +00:00
Edwin Brady
5912c1a1df
Merge pull request #1134 from edwinb/versions
Version numbers in .ipkg files
2021-02-28 13:45:45 +00:00
Edwin Brady
3a6aa27ba4
Fix package parser error message
Thanks to @andylokandy for spotting!

Co-authored-by: Andy Lok <andylokandy@hotmail.com>
2021-02-28 12:56:11 +00:00
Edwin Brady
4726c32d94 Add --ignore-missing-ipkg flag
When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.

We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!
2021-02-27 19:39:47 +00:00
Edwin Brady
d617290dd5 Update packaging documentation 2021-02-27 18:20:55 +00:00
Edwin Brady
37cc095f7a Merge github.com:idris-lang/Idris2 into versions 2021-02-27 18:00:18 +00:00
Edwin Brady
1d8166b1b2 Version number constraints in 'depends' field
Now reporting an error if we can't find a package that satisfies the
constraints. The version number field can still be a string (as it used
to be) but will give a deprecation warning - and the old style version
string wasn't used anyway.

Version constraints can have an upper and/or lower bound, which can be
inclusive or not.
2021-02-27 17:58:52 +00:00
Edwin Brady
1052c41a3c Use version number field in ipkg
Packages are now installed in a directory with their version number.
On adding a package directory, we now look in a local 'depends'
directory first (to allow packages to be installed locally to another
project) before the global install directory.
Dependencies can have version bounds (details yet to be implemented) and
we pick the package with the highest version number that matches.
2021-02-27 14:15:19 +00:00
André Videla
aa27ccbdb6
Merge pull request #1097 from andylokandy/multiline
Implement multi-line string
2021-02-26 21:50:54 +00:00
Andy Lok
75b41bc8b7 Remove FIXME
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-27 02:42:42 +08:00
Denis Buzdalov
9b5a773376 Double fixity/priority definition of >> in a single file was removed 2021-02-26 14:20:49 +00:00
Kamil Shakirov
3ec64a7cfc [docs] Mention external code generators 2021-02-26 13:18:45 +00:00
G. Allais
59de5f1326
[ fix #762 ] Different case tree building strategy (#1125) 2021-02-26 09:33:07 +00:00
claymager
33e336ad27
Give App1 implementation of (>>) (#1122) 2021-02-25 17:09:24 +00:00
Andy Lok
7630aaea5b address comment 2021-02-25 22:12:21 +08:00