Commit Graph

442 Commits

Author SHA1 Message Date
Stefan Höck
9c9ffe4a31
[ fix ] isue 2745 (#2747)
* [ fix ] .ipkg install dir

* [ test ] .ipkg install dir

* [ doc ] update CHECKLIST

* [ doc ] add explanation to pkg016 test

* [ cleanup ] no need to clutter CHECKLIST
2022-11-02 12:01:19 +00:00
Zoe Stafford
078445b178
Merge pull request #2744 from dunhamsteve/bang-fc
[ parser ] Better error messages for type mismatch on bang expressions
2022-11-02 07:06:11 +00:00
Steve Dunham
3c0eadee07 [ parser ] Better error messages for type mismatch on bang expressions 2022-11-01 20:18:33 -07:00
G. Allais
19d0cbcd37
[ new ] put TTC files in a version-tagged directory (#2684) 2022-11-01 18:11:18 +00:00
Guillaume Allais
542ebeae97 [ fix 2726 ] more peeling of Erased 2022-10-22 10:07:39 +01:00
CodingCellist
47c2de3148
[ repl ] Add the ability to get detailed help, e.g. :help :help (#2722)
A common issue for users is that the behaviour of the various repl
commands are not documented anywhere despite some of them having complex
behaviour (e.g. `:set` which accepts a specific set of options). This
implements the ability to call `:?|:h|:help` on repl commands to request
detailed help for a specific repl command, while preserving the
behaviour that calling the help command without any arguments prints the
general help text.

Generic help is defined as the first line of the help text.
Detailed help is defined as the entire help text.

This means that `:help :t`, for example, does not error (there is no
detailed help) but instead just prints the single line of help text.

* [ repl ] Use unlines for detailed help (see #2087)

  Ideally, the lines affected should be multiline strings. But for some
  arcane reason, newlines in those get swallowed in Nix and Windows
  **CI** only Ô.o
  This was already documented in issue #2087.

* [ new ] --except for golden testing lib

  To allow CI to pass despite #2087

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-21 14:35:33 +02:00
G. Allais
30866fa892
[ new ] do not split on dotted patterns (#2706) 2022-10-14 16:21:06 +01:00
Steve Dunham
b15be4a70a [ new ] Allow forward declarations of records 2022-10-14 14:58:29 +01:00
CodingCellist
bb602643b1
[ fix #2712 ] Don't consider CyclicMeta recoverable (#2713) 2022-10-14 14:57:55 +01:00
Thomas E. Hansen
6823915dd0 [ tests ] Check REPL help text and module import cmds
The help text check is for making sure we update it when modifying
things, more than anything else.
2022-10-13 11:31:05 +02:00
Denis Buzdalov
3ca065b85d [ fix #2088 ] Make %runElab expression propagate its rig to check 2022-10-07 10:55:22 +02:00
CodingCellist
23eea52c50
[ fix ] also usleep in the producer of channels006 to guarantee correct output (#2702)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-05 12:03:20 +01:00
Sam Phillips
54a426356a Move channel tests to allschemes 2022-10-04 10:24:27 +02:00
Sam Phillips
abe2e94b5b Add channel tests from Chez to Racket 2022-10-04 10:24:27 +02:00
Sam Phillips
795eeb23c5 Make Racket backend channels behave same as Chez.
Add tests for both that demonstrate equivalent behavior.
2022-10-04 10:24:27 +02:00
Stefan Höck
7eebeff905
[ fix ] natToFinLt is O(n) (#2689) 2022-09-29 14:36:32 +01:00
Steve Dunham
f03f184af9 [ parse ] Add fc to IPragma for better error messages 2022-09-25 16:09:53 +01:00
Guillaume Allais
5631608782 [ base ] deriving Foldable 2022-09-24 10:20:25 +01:00
Guillaume Allais
2adc3319f6 [ parse ] better error messages for records 2022-09-22 12:25:20 +01:00
Stefan Höck
08f24e79fd
[ performance ] constant folding for all integral expressions (#2662) 2022-09-21 10:05:02 +01:00
Steve Dunham
1142f73e05 Add indentation checks when parsing args in implDecl 2022-09-20 23:57:54 +01:00
Steve Dunham
03d6c5f637
[ new ] Handle forward declarations of implementations (#2668)
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2022-09-20 21:08:50 +01:00
G. Allais
55926f30c5
[ fix #2655 ] Add support for DataOpts in records (#2658) 2022-09-14 14:57:04 +01:00
Zoe Stafford
02dfd6ff6c
Trans deps v3 (#2584)
* make `depends` collect all transitive dependencies

This happens by installing the (modified) ipkg file along with ttc files

* [ fix ] parsing a package shouldn't always set sourceDir

* linter *sigh*

* Fix test, add changelog

`asDepends` has been changed to `setSrc` as that is for me more intuitive

in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder

idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info

* (hopefully) fix idris2/pkg13 test on windows

* Actually install the version
This should make things start working

* [ fix ] use backtracking to resolve transitive dependencies

* [ fix ] use backtracking to resolve dependencies

* [ fix ] test pkg006

* Fix missing import

Co-authored-by: stefan-hoeck <hock@zhaw.ch>
2022-09-09 07:08:39 +01:00
G. Allais
ece1198074
[ fix #1742 ] Do not use uppercase names as pattern variables (#2642) 2022-09-05 12:45:51 +01:00
Steve Dunham
2e45902048 [ parser ] Better error messages inside if statements. 2022-09-05 12:44:02 +01:00
Guillaume Allais
f678043854 [ test ] add tricky test case ported from Agda 2022-09-02 16:06:40 +01:00
Guillaume Allais
552f27f813 [ fix #2640 ] Do not shadow function name during case split 2022-09-02 11:55:15 +01:00
Mathew Polzin
23e3695d74 Add test for auto implicit case splitting. 2022-08-16 09:23:19 +02:00
Steve Dunham
f4dc7f4221 Merge branch 'main' into issue-2557 2022-08-03 07:13:04 -07:00
G. Allais
1f41c8b44d
[ close #647 ] Already fixed (#2581) 2022-07-08 14:16:25 +01:00
Guillaume Allais
ac2ef882f6 [ fix #2573 ] Solve constraints before looking at eq type 2022-07-07 20:36:05 +01:00
Stefan Höck
5a962929e7
[ fix ] issue 2537 (#2538)
Co-authored-by: Zoe Stafford <zoepolarsax@gmail.com>
2022-07-07 09:54:52 +01:00
G. Allais
aeeb338e6c
[ new ] deriving Functor (#2568) 2022-07-04 08:58:18 +01:00
Ruslan
dbba32ea09
Fix an eta issue in elaborator-reflection (#2449)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Denis Buzdalov <public@buzden.ru>
2022-06-30 22:01:31 +01:00
Steve Dunham
0454dfd66a Address issue #2557 Incremental compilation is used when .so files are missing. 2022-06-25 19:56:56 -07:00
Guillaume Allais
e5802204b6 [ fix ] holes in record types 2022-06-17 10:17:40 +01:00
György Kurucz
79a2f677d4 [ re #1282 ] Improve unelaboration of case expressions 2022-06-08 17:01:36 +01:00
Zoe Stafford
b9001439b3 Revert "Transitive dependencies v2 (#2496)"
This reverts commit 51f952714d.
2022-06-08 06:35:39 +01:00
Zoe Stafford
51f952714d
Transitive dependencies v2 (#2496)
* make `depends` collect all transitive dependencies

This happens by installing the (modified) ipkg file along with ttc files

* [ fix ] parsing a package shouldn't always set sourceDir

* linter *sigh*

* Fix test, add changelog

`asDepends` has been changed to `setSrc` as that is for me more intuitive

in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder

idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info

* (hopefully) fix idris2/pkg13 test on windows

* Actually install the version
This should make things start working
2022-06-07 14:31:14 +01:00
Denis Buzdalov
599027a893 [ fix ] Make able to interpret result of a macro as a function 2022-05-27 09:36:44 +01:00
Zoe Stafford
932a24baa1 Revert "make depends collect all transitive dependencies (#2469)"
This reverts commit fde6269c7e.
2022-05-21 06:49:07 +01:00
Zoe Stafford
fde6269c7e
make depends collect all transitive dependencies (#2469)
* make `depends` collect all transitive dependencies

This happens by installing the (modified) ipkg file along with ttc files

* [ fix ] parsing a package shouldn't always set sourceDir

* linter *sigh*

* Fix test, add changelog

`asDepends` has been changed to `setSrc` as that is for me more intuitive

in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder

idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info

* (hopefully) fix idris2/pkg13 test on windows
2022-05-20 16:20:54 +01:00
G. Allais
f80fc184e3
[ new ] :exec for RefC (#2466) 2022-05-10 15:09:53 +01:00
Jesse Nava
db13a35bf5 [ fix ] Ensure casting from String to Double results in floating numbers on scheme backends 2022-05-09 18:36:17 +01:00
G. Allais
4256cd15fd
[ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
Steve Dunham
04e65529f6 Better parse error for missing paren after with 2022-04-29 08:59:40 +01:00
Guillaume Allais
81ba322a4b Revert "[ fix ] search should solve auto implicits before implicits"
This reverts commit 6dd68e8924.
because of issue #2437
2022-04-27 11:00:51 +01:00
Guillaume Allais
6dd68e8924 [ fix ] search should solve auto implicits before implicits 2022-04-26 15:07:51 +01:00
Guillaume Allais
0986cf177b [ parse ] better error message for list literals
I got fed up with being puzzled whenever edwin's trailing commas
and my leading commas clash and the error location is the opening
square bracket rather than the repeated comma.
2022-04-15 11:33:20 +01:00