Denis Buzdalov
36132f6539
[ fix, re #3063 ] Fix forgotten reflection values
2023-12-21 17:30:57 +01:00
Steve Dunham
59e00c5210
[ test ] clean_names to make test outputs neater ( #3156 )
2023-12-08 14:10:37 +00:00
Alex1005a
999c404552
[ fix #3083 ] Fix record update with implicit args ( #3092 )
2023-11-30 10:13:09 +00:00
Justus Matthiesen
873b3edd29
[ fix #3143 ] traverse as-patterns when constructing terms matching an impossible LHS ( #3146 )
...
* [ fix #3143 ] traverse as-patterns in `getImpossibleTerm`
* [ test ] impossible as-pattern
2023-11-23 08:29:15 +00:00
Steve Dunham
af10fbaf94
[ error ] Improve parse errors in ipkg files
2023-11-12 10:09:50 +00:00
Denis Buzdalov
1aff26e94c
[ test ] Reduce the need of frequent golden vals updates in one test
2023-11-09 22:05:36 +00:00
Denis Buzdalov
2c328a51c0
[ elab ] Support more applicative traversals of TTImp
2023-11-09 22:05:36 +00:00
Justus Matthiesen
bc386dab4e
[ cleanup ] bring formatting of sc-graphs in tests back in sync
2023-11-06 20:10:21 +00:00
Justus Matthiesen
e5788a3e86
[ test ] tracking size-change across applications
2023-11-06 20:10:21 +00:00
Justus Matthiesen
f435256812
[ test ] tracking size-change in dot patterns
2023-11-06 20:10:21 +00:00
Justus Matthiesen
2798d8f226
[ cleanup ] update expected test outputs
...
Changes to the termination checker brought along some otherwise
insignificant changes to debug and error messages.
2023-11-06 20:10:21 +00:00
G. Allais
bee59d5fde
[ fix ] missing modules in .ipkg files ( #3124 )
...
Additionally, we now have bash options to make sure we will fail hard were
this situation to arise once again.
2023-10-27 20:37:00 +01:00
Denis Buzdalov
5f29b0b9c5
[ elab ] Add an ability to inspect in which function we currently are
2023-10-26 15:42:26 +01:00
Denis Buzdalov
50a579fa18
[ elab ] Implement an operation of returning referred defs of a def
2023-10-26 15:42:26 +01:00
Adowrath
ea093ffaed
[ warning ] for incompatible visibilities on forward decls and definitions. ( #3063 )
2023-10-25 11:24:43 +01:00
Aleksei Volkov
3e5d8a54d4
[ fix ] Prevent relative path traversal in elaborator scripts
2023-10-16 09:43:22 +01:00
Steve Dunham
c04404a95b
[ fix #3097 ] Fix issues parsing %logging followed by named impls ( #3098 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2023-10-13 19:02:58 +01:00
Denis Buzdalov
419a440dad
[ impl ] Support default implicits in named implementations ( #3100 )
2023-10-13 15:26:42 +01:00
Denis Buzdalov
6815aefbe0
[ elab ] Implement file operations, e.g. applicable for type providers
2023-10-13 13:26:46 +01:00
Denis Buzdalov
cbbd0c8caa
[ elab ] Make %macro-function be callable without the extension
2023-10-11 13:20:12 +01:00
Denis Buzdalov
a5b02747b6
[ re #3066 ] Make the rest of tests to use the same form as the others
2023-10-04 14:34:03 +01:00
Denis Buzdalov
567f019230
[ test ] Set IDRIS2_PREFIX to a local dir when testing
2023-10-04 14:34:03 +01:00
Steve Dunham
46483fd120
[ fix ] support .lidr.md and .lidr.tex extensions ( #3071 )
2023-09-25 22:25:26 +01:00
Denis Buzdalov
3886200d29
[ fix ] Make traverse and friends lazy for LazyList
2023-09-25 19:51:17 +01:00
Denis Buzdalov
a643e3af62
[ elab ] Print script's FC in the bad elaboration script error
2023-09-22 11:55:34 +01:00
Steve Dunham
0029257eec
[ fix ] consider nest when guessing scrutinee ( #3070 )
2023-09-14 14:29:41 +01:00
Steve Dunham
8c14e9527b
[ test ] move test to correct location
2023-09-07 20:26:18 -07:00
Steve Dunham
e4fe90e1a3
Merge branch 'main' into foo
2023-09-07 20:19:26 -07:00
Robert Wright
424bc20c27
Group tests by directory
2023-09-07 14:57:22 +01:00
Robert Wright
2bde9104e0
Add filter_test_dir test utility
2023-09-07 14:57:22 +01:00
Robert Wright
61878ef1b6
Remove trivial testing input files
2023-09-07 14:57:22 +01:00
Robert Wright
09466a96bb
Add testing utilities script
2023-09-07 14:57:22 +01:00
G. Allais
c52b029986
[ new ] function options for case blocks ( #3062 )
2023-09-01 11:35:52 +01:00
Aleksei Volkov
af7ba2fa67
[ ttc ] Compare modification time with nanosecond precision ( #3046 )
2023-08-31 11:55:57 +01:00
Guillaume Allais
e3214586a5
[ fix #3057 ] properly handle char literals in comments
2023-08-31 11:52:32 +01:00
Denis Buzdalov
cf9a73f86c
[ prelude ] Add some lacking %tcinlines
2023-08-23 11:04:53 +01:00
Aleksei Volkov
115c9e0889
[ unelab ] Properly unelaborate metavariables originating from %search ( #3055 )
...
* [ unelab ] Properly unelaborate `%search`
* [ test ] Added regression test that checks quotation of `%search`
2023-08-23 08:02:11 +01:00
Steve Dunham
0b3e04aef0
update tests for DCon in size change
2023-08-12 13:55:07 -07:00
Steve Dunham
878187d7f7
[ fix ] Totality checker misses indirect references to partial data
2023-08-12 12:57:28 -07:00
Steve Dunham
bde1a66075
[ fix ] Fix pattern match issue with function application in Refl ( #3027 )
2023-08-04 13:46:04 +01:00
Steve Dunham
f0f776c288
[ error ] Improve error messages for Delay &co
2023-08-04 13:39:39 +01:00
André Videla
1fa638494d
[ new ] Fixity access modifier ( #3011 )
2023-07-31 08:35:16 +01:00
Robert Wright
cbbe761c51
Add fromTTImp, fromName, and fromDecls for custom TTImp, Name, and Decls literals
2023-07-31 08:17:55 +01:00
Steve Dunham
5165c79b67
[ fix ] Ensure local defs with no claim are local
2023-07-15 18:18:48 -07:00
Robert Wright
af3c5fd454
Generalize Prelude proof helpers
2023-07-05 16:36:09 +01:00
Denis Buzdalov
5dcf62499d
[ elab ] Make elab scripts be able to record warnings ( #2999 )
2023-06-19 16:34:19 +01:00
Andre Videla
9797a79b53
[ new ] Allow fixities to be hidden with %hide
...
* Change the printing of namespaced operator to show
parenthesis around operators
* Update warning when conflicting fixities are found
* Do not warn about redundant but compatible fixities
2023-06-14 11:19:59 +01:00
Alexander
63fa070efa
add test for parse error let-in in do block
2023-06-13 11:01:42 +03:00
Justus Matthiesen
6c6867490c
[ test ] lazy functions
2023-06-12 11:04:59 +01:00
Aleksei Volkov
e594669210
[ fix #1878 ] Programmer-provided terms should be alwaysReduce ( #2977 )
...
* [ fix ] Programmer-provided terms should be alwaysReduce
This ports Edwin's commit that fixes the original issue back to Idris
Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
* [ tests ] Added regression test for #1878
* Updated CHANGELOG.md and CONTRIBUTORS
---------
Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
2023-06-01 17:08:02 +01:00
