Commit Graph

2133 Commits

Author SHA1 Message Date
Edwin Brady
452b0fc3f9 Fiddle with linter
We want duplicate headings in the CHANGELOG
2021-06-27 17:30:37 +01:00
Edwin Brady
74f0c3bf33 Add some documentation on incremental builds 2021-06-27 17:03:16 +01:00
Edwin Brady
84c2a497bc Add incremental compilation note to INSTALL.md 2021-06-27 16:35:43 +01:00
Edwin Brady
5a84623629 Update CHANGELOG 2021-06-27 16:33:04 +01:00
Edwin Brady
627bce068e Better errors/warnings for --inc
If the code generator doesn't support incremental builds, report an
error.
2021-06-27 16:28:17 +01:00
Edwin Brady
fc0e0f19d3 Use IDRIS2_CG for incremental library builds
This way there's no problem if chez isn't installed
2021-06-27 16:09:02 +01:00
Edwin Brady
6c319dbcaf Update API test for new Codegen fields 2021-06-27 16:00:03 +01:00
Edwin Brady
94088bea80 Support for incremental compilation with Chez
This adds a new flag '--inc <backend>' which, if set, compiles all
modules incrementally, and for executables, links the incrementally
compiled modules rather than building the whole program.

Also, adds an environment variable IDRIS2_INC_CGS for providing a comma
separated list of backends to use for incremental builds.

Also, adds '--whole-program', which overrides incremental builds for an
executable.

Incremental builds are much faster if there's nothing to recompile, but
for the Chez backend, generate code which runs at about half the speed.

Currently only works for Chez - other backends ignore the flag.

Also, incremental building of an executable will only work if *all*
required modules have been built incrementally for the backend in use.
2021-06-27 15:40:23 +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