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
Zoe Stafford
8658351b94
Merge pull request #2583 from dunhamsteve/dumpanf
...
Fix the --dumpanf command line switch.
2022-07-10 10:17:46 +01:00
Steve Dunham
32a877c3d4
Fix the --dumpanf command line switch.
2022-07-09 13:18:29 -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
Guillaume Allais
19bc798952
[ re #2526 ] Update golden value
2022-07-07 20:34:54 +01:00
Locria Cyber
05737b25fb
Allow to specify --inc when building package
2022-07-07 17:34:41 +01:00
stefan-hoeck
ea6f9975cf
[ cleanup ] add proper depends field to network.ipkg
2022-07-07 17:24:54 +01:00
Guillaume Allais
d19dbfffff
[ fix #2229 ] better warning
2022-07-07 16:42:34 +01:00
Guillaume Allais
8b20da7e39
[ cleanup ] remove TT from base
...
As discussed with edwin, let's get rid of the external TT type.
There is no way to get your hands on a TT value anyway so this
should not change anything.
2022-07-07 16:42:19 +01:00
Denis Buzdalov
c03a39789f
[ breaking ] Make arguments of runRWST like in other transformers
...
Put the `RWST` argument to be the last one. This makes such functions
to be easier used in point-free compositions and to be easily
interchangeable with existing `runStateT`-like functions.
2022-07-07 15:19:41 +01:00
G. Allais
4874bf2114
[ fix ] handle implicit arguments in Deriving.Functor ( #2572 )
2022-07-07 09:55:13 +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
Guillaume Allais
7db20d38a3
[ cleanup ] Fewer assert_total in deriving Functor
2022-07-04 12:03:49 +01:00
G. Allais
aeeb338e6c
[ new ] deriving Functor ( #2568 )
2022-07-04 08:58:18 +01:00
Jeroen de Haas
ea7e43ad74
[doc] Remove implicit argument in documentation for parseDouble
2022-07-03 22:00:31 +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
Denis Buzdalov
38caff23b8
[ fix ] Make the result Show of case .. of compilable
...
1. The arrow was fixed
2. Put explicit type ascription into a comment
3. Don't print type when it was not present in the expression
2022-06-27 15:32:02 +01:00
Denis Buzdalov
afaa80a5ae
[ re #2533 ] Fix printing of lazy values in Show TTImp
2022-06-27 15:32:02 +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
G. Allais
4024857d20
[ base ] Various Language.Reflection improvements ( #2554 )
2022-06-22 13:07:27 +01:00
Denis Buzdalov
e856569d16
[ doc ] Clarify the doc comment of find* functions of SnocList
2022-06-20 12:13:37 +01:00
Denis Buzdalov
113085d0c3
[ base ] Add a function for changing the topmost FC of a TTImp
2022-06-17 19:53:07 +01:00
Denis Buzdalov
bc838467a3
[ base ] Add a function returning Dec for So
2022-06-17 19:52:35 +01:00
Justus Matthiesen
1ae4fdd605
Fix error message for LinearMisuse
2022-06-17 11:48:51 +01:00
Guillaume Allais
e5802204b6
[ fix ] holes in record types
2022-06-17 10:17:40 +01:00
Guillaume Allais
bf3272c344
[ minor ] more magic for name generation
2022-06-17 10:17:40 +01:00
Guillaume Allais
f111838e52
[ cleanup ] move TTC implementations to separate files
2022-06-17 10:17:40 +01:00
Denis Buzdalov
a7fb6722a0
[ re #2533 ] Fix recently added reflection's Show ( #2543 )
2022-06-16 11:08:51 +01:00
Denis Buzdalov
45579795bc
[ elab ] Make any error in elab script to produce a special error type
2022-06-16 09:49:56 +01:00
Denis Buzdalov
742d41f696
[ elab ] Make actual bad script errors be reported so
2022-06-16 09:49:56 +01:00
Denis Buzdalov
df6f4f69cd
[ doc ] Add clarification to the doc of a function of Elaboration
2022-06-16 09:49:56 +01:00
Denis Buzdalov
e590014fb7
[ cleanup ] Remove unused expression
2022-06-16 09:49:56 +01:00
G. Allais
bdf3833df5
[ new ] Auto in Agda (+ bonus) ( #2541 )
...
* [ new ] Auto in Agda (+ bonus)
* [ minor ] use DN for more readable terms
2022-06-16 09:35:45 +01:00
Guillaume Allais
cd324f9ff3
[ base ] Name convenience functions
2022-06-14 16:07:37 +01:00
