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
Joel Berkeley
c0153e72cd
[ base ] implement decEq for SnocList ( #2630 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-09-20 15:46:15 +01:00
G. Allais
d1ae9d9fd5
[ papers ] Computing with Generic Trees ( #2661 )
2022-09-16 11:40:09 +01:00
Steve Dunham
669f49e23e
[ parser ] Make commitKeyword fail fatally
2022-09-16 11:39:53 +01:00
G. Allais
55926f30c5
[ fix #2655 ] Add support for DataOpts in records ( #2658 )
2022-09-14 14:57:04 +01:00
stefan-hoeck
188de8b4cc
[ fix ] issue 2616
2022-09-12 02:10:13 -07: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
Nil Geisweiller
e8b1e34f1c
Add missing space after …
2022-09-08 09:22:47 +01:00
Hattori, Hiroki
4ba651bb8e
[RefC] Add sysCodegen primitive to avoid compiler error. ( #2613 )
2022-09-08 00:44:14 +01:00
Zoe Stafford
a001333947
Warning for shadowed local bindings ( #2623 )
...
* Warning for shadowed local bindings
* [ lint ]
* Remove name shadowing in compiler src
* [ fix ] spelling & test cases
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-09-07 20:59:28 +01:00
Steve Dunham
9646b31f2b
[ test ] Fix timing issue in interactive045 test
2022-09-06 10:05:34 +01:00
Steve Dunham
90e46ef340
Add test case for lexer issue and fix other instance.
2022-09-05 13:47:41 -07:00
Yupanqui
93b0f9c7b8
Fix for lexer colums
2022-09-05 13:47:41 -07:00
G. Allais
ece1198074
[ fix #1742 ] Do not use uppercase names as pattern variables ( #2642 )
2022-09-05 12:45:51 +01:00
0xd34df00d
b3c80e0765
[ base ] Add finToNatEqualityAsPointwise, an inverse of finToNatQuotient
2022-09-05 12:45:28 +01:00
Steve Dunham
351b5ba720
[ parser ] Fix issue where Alt drops incoming commit tag
2022-09-05 12:44:02 +01:00
Steve Dunham
2e45902048
[ parser ] Better error messages inside if statements.
2022-09-05 12:44:02 +01:00
Steve Dunham
150673622b
[ test ] Add a sleep 1 to the interactive044 test to work around a race condition
2022-09-04 09:17:22 +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
Hattori, Hiroki
c2be1677da
[RefC] add missing symbols of showcCleanStringChar ( #2610 )
2022-09-01 14:34:40 +01:00
Adowrath
1914606d40
Fix connect in linear module and add bytes-specific functions
2022-09-01 12:23:29 +01:00
Steve Dunham
1f4508390f
[ doc ] Add instructions for installing chez scheme and bootstrapping on M1 / M2 macs.
2022-09-01 10:52:45 +01:00
Denis Buzdalov
5266a2bc22
[ base ] Implement MonadError () for MaybeT
2022-09-01 10:48:15 +01:00
Guillaume Allais
6891490ed2
[ fix ] support for implicits in Deriving.Functor
...
A lot of refactoring to bring these. That's hopefully the last
feature that was needed...
2022-08-29 18:35:24 +01:00
Mathew Polzin
23e3695d74
Add test for auto implicit case splitting.
2022-08-16 09:23:19 +02:00
Mathew Polzin
50ae5f9484
fix syntax errors produced by case splitting
2022-08-16 09:23:19 +02:00
Zoe Stafford
86c060ef13
Reimplement %nomangle in terms of %export ( #2604 )
...
* Reimplement %nomangle in terms of %export
Also deprecate %nomangle
* [ lint ] fix linter errors
2022-08-15 13:26:06 +01:00
Guillaume Allais
4672305fc3
[ fix ] more filtering of invalid datatypes
2022-08-13 11:29:19 +01:00
Eric Corson
8684ca4d3d
[ fix ] Add missing reserved words to JS backend
2022-08-13 11:29:02 +01:00
Steve Dunham
e29e2289e7
[ fix ] Fixes memory leaks in currentDir, fGetLine, and fGetChars ( #2606 )
2022-08-10 21:23:53 +01:00
Nil Geisweiller
719b5ad17f
[ cleanup ] Remove extraneous show and simplify printLn ( #2618 )
2022-08-10 21:22:58 +01:00
Justus Matthiesen
a30209d492
[ fix ] Remove stray ")" in Show instance for Term ( #2611 )
2022-08-08 15:24:07 +01:00
Zoe Stafford
5c4b2e81cd
Merge pull request #2560 from dunhamsteve/issue-2557
...
Address issue #2557 Incremental compilation produces bad executables
2022-08-07 12:13:42 +01:00
Steve Dunham
f4dc7f4221
Merge branch 'main' into issue-2557
2022-08-03 07:13:04 -07:00
Steve Dunham
4088dd863b
Rebuild TTC if they don't contain needed incremental data (related to #2560 )
2022-08-03 07:12:46 -07:00
Guillaume Allais
2aaad190fb
[ ci ] drop hirsute, stick to latest (now 22.04)
2022-07-30 00:34:21 +01:00
Guillaume Allais
4a465ac21e
[ fix ] custom backend doc
...
The type Codegen was changed in #2594 .
2022-07-26 15:33:46 +01:00
nrnrk
572a4c74d6
Fix typo
2022-07-24 13:50:45 +01:00
Guillaume Allais
a4b99bd81c
[ refactor ] introduce allSemanticHighlighting
...
Side effect: all the aspects are now sorted by ranges as we are
merging the PosMaps instead of appending the lists.
2022-07-19 15:01:20 +01:00
G. Allais
84a504738c
[ doc ] add comments to generated javascript ( #2594 )
2022-07-18 17:30:56 +01:00
Guillaume Allais
8ecb1aaf95
Revert "Fix issue with case inside a type."
...
This reverts commit 50ca28c068
2022-07-18 15:58:29 +01:00
Steve Dunham
50ca28c068
Fix issue with case inside a type.
2022-07-18 14:17:14 +01:00
G. Allais
0cbbf97b79
[ new ] extend Deriving.Functor to (non-strictly) positive functors ( #2591 )
2022-07-18 14:10:46 +01:00
Mathew Polzin
4a348c1f95
Public export remaining function to allow for proofs involving parsing numbers.
2022-07-18 14:10:05 +01:00
Steve Dunham
c69af04f46
[ fix ] Support multiple ide server instances ( #2586 )
...
* Print the bound ide mode socket instead of the configuration variable.
* Change --ide-mode-socket to choose an open socket instead of using 38398
* [ doc ] Documentation for starting ide-mode
2022-07-18 14:08:56 +01:00
Steve Dunham
a0d9e2bbba
Update tests using base64 utility to also work on macos ( #2536 )
...
* Update tests using base64 utility to also work on macos
* Fix invocation of base64 in refc/buffer test.
2022-07-13 06:46:31 -07:00
Nil Geisweiller
da3239bdf5
Update packages.rst ( #2588 )
2022-07-13 06:25:37 -07:00
ProofOfKeags
68a144bf18
Support System.Signal for node backend ( #2556 )
...
* first pass at signal support for node backend
* change signal values to int's
* implements defaultSignal
* return -1 as expected by calling API if any error is raised by nodejs runtime
* finishes signal support for nodejs
* extract repetitive foreign import identifiers
* fix comments
2022-07-10 10:18:58 +01:00
