Commit Graph

1998 Commits

Author SHA1 Message Date
Guillaume ALLAIS
b5cbf9274d [ test ] cosmetic improvements
Put the dependency checks in the banner, e.g.:

------------------------------------------------------------------------
Base library
✓ Found Chez at /usr/bin/chezscheme9.5
✓ Found node at /usr/bin/node
------------------------------------------------------------------------
2021-05-26 19:50:50 +01:00
Edwin Brady
1329e69b5d
Merge pull request #1469 from edwinb/issue1365
Cache intermediate results in totality checking
2021-05-26 16:29:57 +01:00
Edwin Brady
a9b754e9fa Remove whitespace again
Didn't I just do this? Grr.
2021-05-26 15:54:57 +01:00
Edwin Brady
9cce0e1340 Remove whitespace in test file 2021-05-26 15:52:21 +01:00
Edwin Brady
68f6f4dbd5 Cache intermediate results in totality checking
This saves a lot of unnecessary exploring of size change graphs, which
can get over the top quite quickly if there's complex mutual
definitions, or even just a single function with an interesting variety
of recursive calls.

Fixes #1365
Fixes #1277
Fixes #645
2021-05-26 15:48:09 +01:00
Jan de Muijnck-Hughes
692054516e
A rough dump of how to debug idris2's workings. (#1464) 2021-05-26 10:19:40 +01:00
Ben Hormann
1aefab3af0 [ fix ] nproc missing for non-GNU systems 2021-05-26 09:05:13 +01:00
G. Allais
4b0f171d7d
[ help ] display logging topics and accompanying blurbs (if any) (#1467) 2021-05-26 08:16:33 +01:00
G. Allais
1fd5ccf080
[ fix #1453 ] rename cast -> coerce (#1468) 2021-05-26 08:12:58 +01:00
Fabián Heredia Montiel
f1085b98a5 [ test #18 ] Add passing tests from issue to avoid regressions 2021-05-25 23:07:59 +01:00
Fabián Heredia Montiel
704a2525f1 [ fix #55 ] Propagate linear context from Definition to Clauses 2021-05-25 19:27:02 +01:00
Fabián Heredia Montiel
d9318a260a [ Fixup #1437 ] Correct cases in cftySpec 2021-05-25 16:46:10 +01:00
Mathew Polzin
a0a417240e
Simple signal handling (#1458) 2021-05-25 16:45:46 +01:00
Stefan Höck
961683ab81
[ FFI ] Support new IntX types in foreign function types (#1437) 2021-05-25 13:57:25 +01:00
stefan-hoeck
6f90e5d2e2 [ test ] node test for System.getArgs 2021-05-25 13:26:42 +01:00
stefan-hoeck
e293d82577 [ fix ] System.getArgs on node backend 2021-05-25 13:26:42 +01:00
Kamiλ Shakirov
ad656a8d47
Remove realpath (#1457) 2021-05-25 11:01:28 +01:00
Ohad Kammar
699de70301
[contrib] More properties of vectors (#1449) 2021-05-24 08:48:00 +01:00
archlinuxxx
7ca526ee05 fix typo 2021-05-24 08:42:49 +01:00
Ben Hormann
b457d15701 [ fix #221 ] realpath alternative for macOS
Zsh is available by default on macOS
readlink -f is commonly supported on Linux and BSD
2021-05-21 18:23:50 +01:00
Guillaume ALLAIS
6904cf5db6 [ :doc ] Adding projections to the record doc 2021-05-21 18:23:13 +01:00
Guillaume ALLAIS
ee7956b318 [ cleanup ] move DocString to Doc.String 2021-05-21 18:23:13 +01:00
G. Allais
e9f5038cb7
[ fix ] Version encoding should be stable (#1443) 2021-05-21 10:04:27 +01:00
Zoe Stafford
50d75cc3a4
[ cleanup ] logging (#1442)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-05-20 20:00:13 +01:00
Robert Wright
5aef7a2dff fixup! 04dfba03 2021-05-20 14:25:16 +01:00
Robert Wright
1e15ff31d3 Disable C file linting 2021-05-20 14:25:16 +01:00
Robert Wright
c57bb5a65f Add RefC StringIterator support 2021-05-20 14:25:16 +01:00
Robert Wright
58a321ca9c Add RefC foreign closure support 2021-05-20 14:25:16 +01:00
Robert Wright
cd3906645b Add RefC getArgs support 2021-05-20 14:25:16 +01:00
Robert Wright
f3aae06b28 Add RefC Clock support 2021-05-20 14:25:16 +01:00
Robert Wright
cf2b05ce02 Add RefC Buffer support 2021-05-20 14:25:16 +01:00
Robert Wright
ecde887d7a Add RefC external type support
The external type must be a Value object for garbage collection reasons.

For completely custom types, use a GCPointer, with appropriate GC function for clearing up your data type.
2021-05-20 14:25:16 +01:00
Robert Wright
204b96fe6c Add RefC math library linking 2021-05-20 14:25:16 +01:00
Robert Wright
c34c6e0959 Complete RefC standard String support
- Fix off-by-one error in String reverse
- Correct order of arguments in strSubstr
- Actually use start index of strSubstr
- Reduce memory usage of strSubstr in case of overrunning string end
- Add fastPack/fastUnpack/fastConcat
- Use unsigned chars for character comparisons
- Fix generated C character encodings
2021-05-20 14:25:16 +01:00
Robert Wright
978d86f28d Fix RefC identity functions memory management 2021-05-20 14:25:16 +01:00
Robert Wright
2a957a38d9 Add RefC FFI header file support 2021-05-20 14:25:16 +01:00
Robert Wright
51ddcad3b8 Improve RefC foreign function support 2021-05-20 14:25:16 +01:00
Robert Wright
d961c0488c Make RefC fail noisily 2021-05-20 14:25:16 +01:00
Robert Wright
06ca4bed5d Refactor C codegen
- Remove commented out code
- Remove unused showEitherStringInt and toIntEitherStringInt functions
- Make cTypeOfCFType pure
- Merge identical case branches of createCFunctions
- Remove unused C support functions
2021-05-20 14:25:16 +01:00
Ohad Kammar
618c71477e
[ close #1384 ] built-in Snoc-lists [< 1, 2, 3 ] (#1383) 2021-05-20 12:56:25 +01:00
Ohad Kammar
823230b77c
Vect reasoning library (#1439)
When working on Frex I needed a whole bunch of lemmata to do with Data.Vect. I hope it will be useful for others.
2021-05-20 11:55:22 +01:00
Guillaume ALLAIS
31a5175a02 [ re #1031 ] Disallow ? patterns on the LHS
We do this during desugaring because elaboration may insert valid
`?` values on the LHS (e.g. when elaborating things that cannot be
pattern-matched on and should be checked to be forced).
2021-05-20 10:23:00 +01:00
Michael Messer
890810e9b6
Remove unsecure commands (#1433) 2021-05-20 10:21:39 +01:00
Edwin Brady
daf30ee4f6
Merge pull request #1438 from edwinb/more-ttc-wrangling
Substantial reduction in TTC size
2021-05-19 18:06:09 +01:00
Edwin Brady
f6919afef1 Increment TTC version 2021-05-19 17:13:51 +01:00
Edwin Brady
5ab91cafc8 Substantial reduction in TTC size
Write small integers out as 1 byte, not 8, at the cost of writing larger
integers out in 9 bytes. Most integers fit in 1 byte, since it's string
and list lengths from user-written code.
2021-05-19 16:48:06 +01:00
Edwin Brady
b901b2e5ad
Merge pull request #1434 from edwinb/ttc-wrangling
Some TTC loading improvements
2021-05-19 13:34:53 +01:00
Edwin Brady
72e0245e06 Remove trailing space 2021-05-19 01:08:04 +01:00
Edwin Brady
b94f7e96ae Strip current namespace when writing out defs
This saves writing the same strings over and over again in the body of a
definition. At the cost of a traversal on reading and writing the ttcs,
there is a good bit less to write out.
2021-05-19 00:23:19 +01:00
stefan-hoeck
eca25776c3 [ doc ] updated changelog 2021-05-18 20:25:26 +01:00