idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-22 11:13:36 +03:00
Code Issues Projects Releases Wiki Activity
2,126 Commits 6 Branches 9 Tags 115 MiB
f77670814e
Commit Graph

2126 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Jan de Muijnck-Hughes
f77670814e
[ fix ] test Test.Golden with non-idris2 projects. (#1613) 2021-06-25 14:04:46 +01:00
Jan de Muijnck-Hughes
939bc8d8ff
Merge pull request #1610 from gallais/fix-golden 
[ fix ] Various Test.Golden fixes
 2021-06-24 20:27:20 +01:00
Guillaume ALLAIS
516b1b18f5 [ fix ] padding shouldn't be affected by ANSI escape codes 2021-06-24 16:38:27 +01:00
Guillaume ALLAIS
c217911573 [ fix ] Only pass --cg to test exec if requested 
Do not pass a codegen choice when the test pool specifies it does
not require a codegen to be specified.
 2021-06-24 16:36:03 +01:00
Edwin Brady
ea1ad1688f
Merge pull request #1599 from edwinb/prepare-040 
Changes for next release, 0.4.0
 2021-06-23 19:37:12 +01:00
Edwin Brady
00107730ae More version number updates 2021-06-23 18:46:38 +01:00
Edwin Brady
980b6174ec Added --mkdoc to CHANGELOG too 2021-06-23 18:31:31 +01:00
Edwin Brady
80aeecaac0 Add note on --mkdocs 2021-06-23 18:29:49 +01:00
Edwin Brady
6511412518 Change heading in CHANGELOG 2021-06-23 18:25:35 +01:00
Edwin Brady
a93def90a9 Merge github.com:idris-lang/Idris2 into prepare-040 2021-06-23 18:16:36 +01:00
Edwin Brady
991a4e8196 Update bootstrap scheme 2021-06-23 18:16:13 +01:00
Edwin Brady
5689786b26
Merge pull request #1598 from gallais/show-void 
[ fix ] missing Show implementations in libs
 2021-06-23 18:11:40 +01:00
Edwin Brady
7d3e3e0719 Check sizes of buffers and strings in TTCs 
They need to be positive or we can't make the buffer, which causes a
segfault. This happened when loading old TTCs with a different format.
Fixes #1503
 2021-06-23 18:08:27 +01:00
Edwin Brady
56a9a5866d Update version number in pkg010 test 2021-06-23 17:52:00 +01:00
Guillaume ALLAIS
afd55951c2 [ fix ] missing Show (Fin n) in base 2021-06-23 16:46:25 +01:00
Edwin Brady
0a0c41d79b
Merge pull request #1574 from I-B-3/patch-1 
Add clarifying note re: PREFIX in config.mk
 2021-06-23 16:19:04 +01:00
Edwin Brady
ae73c39609 Merge github.com:idris-lang/Idris2 into prepare-040 2021-06-23 16:17:40 +01:00
Edwin Brady
c1057a19af
Merge pull request #1489 from buzden/some-uninhabiteds 
[ base ] Some lacking implementations for `Uninhabited`
 2021-06-23 16:17:32 +01:00
Guillaume ALLAIS
4d12766886 [ fix ] expected test output 2021-06-23 16:15:35 +01:00
Edwin Brady
a0cfa28621 Update version numbers 2021-06-23 16:15:21 +01:00
Edwin Brady
af1cbbf913 Update CHANGELOG 
Missing timeout command and a note on performance
 2021-06-23 16:13:02 +01:00
Edwin Brady
f1b2828be7
Merge pull request #1593 from zseri/fix-theorem-docs 
fix #1514 (Broken doc in the theorem proving part of Idris2)
 2021-06-23 15:56:40 +01:00
Edwin Brady
bea175c09c
Merge pull request #1531 from Russoul/fc-name-at 
Reconcile FC and IDE mode
 2021-06-23 15:48:04 +01:00
Guillaume ALLAIS
21cca08df1 [ fix ] missing Show Void in prelude 2021-06-23 15:33:12 +01:00
Edwin Brady
514a9d79c7
Merge pull request #1597 from edwinb/expr-search 
A couple of expression search improvements
 2021-06-23 12:02:03 +01:00
Edwin Brady
7802b72dd5 Refine timeout mechanism 
Set the maximum time when initialising the timer, which means we can
check in the middle of potentially expensive operations like
normalisation, rather than just at occasional points in expression
search.
 2021-06-23 01:23:20 +01:00
Edwin Brady
4ef29da87e Fix expression search on already solved holes 
If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
 2021-06-23 00:59:26 +01:00
Edwin Brady
92066c24fe Add timeout for definition/expression search 
This is set to 1 second by default. Usually if it hasn't found a result
by then, it never will, but given that we find the first batch of
results then sort them, the timeout also stops us fruitlessly searching
for more solutions.

Hopefully 1s is more than enough for CI too. There is a mechanism to
change the timeout (%search_timeout) so if it turns out that CI needs
longer in some cases, we can increase it there.

I haven't documented this yet, but proof/definition search needs
documenting in general. I'll get to that.

The timer mechanism may also be useful elsewhere - I'm considering it
for ambiguity warnings, because the ambiguity depth limit isn't working
very well for that.
 2021-06-23 00:42:51 +01:00
zseri
c760812b59 fix #1514 (Broken doc in the theorem proving part of Idris2) 2021-06-22 14:42:54 +02:00
zseri
82cf4092b7 Nix: verbatim URLs are deprecated 
References:
- https://nix.dev/anti-patterns/language#unquoted-urls
- https://github.com/NixOS/rfcs/pull/45
- https://github.com/NixOS/rfcs/blob/master/rfcs/0045-deprecate-url-syntax.md
 2021-06-22 12:52:53 +01:00
G. Allais
d2986e5fea
[ refactor ] to allow testpools to specify a backend (#1591) 2021-06-21 22:12:17 +01:00
G. Allais
49f8cefeff
[ cleanup ] Test.Golden (#1526) 2021-06-21 17:30:11 +01:00
Edwin Brady
a15136b3b2
Merge pull request #1590 from edwinb/eval-updates-take2 
Some evaluator tidying, CBV evaluation (second attempt)
 2021-06-21 14:10:43 +01:00
Edwin Brady
ab2012a7dc Small change in output of reg042 
No idea what happened there. Maybe a minor change in the input? Anyway,
this updates it as it should be.
 2021-06-21 13:07:26 +01:00
Edwin Brady
e35930a2aa Change reg042 to look at compiler output 2021-06-21 12:41:55 +01:00
Matt Smith
95710c3a29 Add chezscheme binary to search path 
The Gentoo Chez package and some versions of the Ubuntu package
install Chez scheme as `/usr/bin/chezscheme' which requires manually
setting the CHEZ environment variable.  Adding it to the search path
makes it easier for these users.

Closes: https://github.com/idris-lang/Idris2/issues/666
 2021-06-21 11:20:12 +01:00
Edwin Brady
37f8c2c58f Merge github.com:idris-lang/Idris2 into eval-updates 2021-06-20 21:35:56 +01:00
Robert Wright
a8264f8f05 Add ability to extend RefC backend to create further backends 2021-06-18 16:59:35 +01:00
Fabián Heredia Montiel
657699a866
[doc] Add missing entries and refactor CHANGELOG.md (#1566) 2021-06-18 16:45:00 +01:00
Tim Engler
68c6fe222c
[ Fix #1577 ] Actually use natMinus hack (#1578) 
And also make sure that the output is truncated to 0.

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-06-18 11:50:54 +01:00
I B 3
da21f0477a Add note to INSTALL.md re: PREFIX being an absolute path 2021-06-18 11:07:53 +01:00
I B 3
722bab8110 Stop pointing at the Void 2021-06-18 11:06:45 +01:00
I B 3
fb14b57eb0
Add clarifying note re: PREFIX in config.mk 2021-06-18 01:36:24 +01:00
G. Allais
f3177e0cc1
[ fix ] print postfix projections... postfix (#1557) 2021-06-18 00:00:51 +01:00
CodingCellist
55f8bc3b90
Improve case-splitting formatting to not introduce new whitespace; add a bit of comments+docs. (#1553) 2021-06-17 16:48:59 +01:00
Nick Drozd
3e3a4e1b78
Use truncated case notation (#1562) 2021-06-17 15:52:19 +01:00
Stefan Höck
c04835c436
[ cleanup ] Reuse Tarjan's algorithm in JS backend and some other cleanups (#1504) 2021-06-17 12:43:10 +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
Fabián Heredia Montiel
e0e8403317
[ new ] detect changes using sha256 rather than timestamps (#1535) 
The option is hidden being a flag (`-Xcheck-hashes`) so that by default `touch`ing
a file is enough to get it recompiled.

Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
 2021-06-16 16:16:58 +01:00
Nick Drozd
0db136d168
Hoist some pures (#1556) 2021-06-16 15:22:52 +01:00