3544 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Joel Berkeley	2520f4eb7b	line length	2023-11-11 16:11:02 +00:00
Joel Berkeley	a0887401a6	line length	2023-11-11 16:10:13 +00:00
Joel Berkeley	d7d97d45ad	line length	2023-11-11 16:09:23 +00:00
Joel Berkeley	323f1d0186	line length	2023-11-11 16:02:33 +00:00
Joel Berkeley	a409f11d39	wording	2023-11-11 15:57:02 +00:00
Joel Berkeley	fec32e45f8	wording	2023-11-11 15:55:19 +00:00
Joel Berkeley	9608086669	link map of source code	2023-11-11 15:54:09 +00:00
Joel Berkeley	1e7aee47d8	typo	2023-11-11 02:11:50 +00:00
Joel Berkeley	92d36fb19c	link videos and map of source code	2023-11-11 02:10:17 +00:00
Joel Berkeley	978f956012	remove icon	2023-11-10 13:38:12 +00:00
Joel Berkeley	9b4c4d8efd	icon attempt 5	2023-11-10 13:35:57 +00:00
Joel Berkeley	54eec37572	icon attempt 4	2023-11-10 13:35:24 +00:00
Joel Berkeley	0795d9cb00	icon attempt 3	2023-11-10 13:34:57 +00:00
Joel Berkeley	4c5bfbc95c	icon attempt 2	2023-11-10 13:31:54 +00:00
Joel Berkeley	6abffe22d0	icon first attempt	2023-11-10 13:28:37 +00:00
Joel Berkeley	e66b79fc2c	mention Node version requirement	2023-11-10 13:09:27 +00:00
Joel Berkeley	3f1784a163	simplify TOC in INSTALL	2023-11-10 13:07:07 +00:00
Joel Berkeley	e048896179	Install -> Installing	2023-11-10 12:59:19 +00:00
Joel Berkeley	6a6ad983db	pack link points to homepage	2023-11-09 23:33:29 +00:00
Joel Berkeley	b26bd7d4b4	remove pack installation instructions	2023-11-09 23:16:54 +00:00
Joel Berkeley	4d0410a7d3	alternative links	2023-11-09 23:13:07 +00:00
Joel Berkeley	c4b3069a6f	refactor README and installation instructions	2023-11-09 22:58:02 +00:00
Denis Buzdalov	1aff26e94c	[ test ] Reduce the need of frequent golden vals updates in one test	2023-11-09 22:05:36 +00:00
Denis Buzdalov	2c328a51c0	[ elab ] Support more applicative traversals of TTImp	2023-11-09 22:05:36 +00:00
CodingCellist	d80bc1537d	[ base ] Add bindings for ieee Double number consts (#3116)	2023-11-09 14:01:40 +00:00
Steve Dunham	a945b5d2df	[ ffi ] Fix missing structure declarations in scheme ffi	2023-11-09 14:00:20 +00:00
Justus Matthiesen	db4c5e7fbb	Cleanup of sizeEq (#3138)	2023-11-09 13:59:53 +00:00
PHO	7c87005092	Support "make -j" (#3135) ... * Allow Idris2 to bootstrap with "make -j" "linear" should explicitly depend on "base" so that "base" is built before "linear", otherwise it can fail with: > Error: Module Data.Nat not found > > Data.Linear.Copies:5:1--5:16 > 1 | module Data.Linear.Copies > 2 | > 3 | import Data.Linear.Bifunctor > 4 | import Data.Linear.Notation > 5 | import Data.Nat > ^^^^^^^^^^^^^^^ * Allow Idris2 to build with "make -j all" "all: ${TARGET} libs" is bad because it means "${TARGET}" and "libs" can be built independently. So "make -j" attempts to build them parallelly and fail.	2023-11-08 08:18:02 +00:00
Justus Matthiesen	a26766e57a	[ doc ] bring findLoops and checkNonDesc description back in sync	2023-11-06 20:10:21 +00:00
Justus Matthiesen	8e34332c08	[ cleanup ] remove unneeded debug messages	2023-11-06 20:10:21 +00:00
Justus Matthiesen	a84ba3b1ef	[ doc ] bring description of mkChange back in sync	2023-11-06 20:10:21 +00:00
Justus Matthiesen	bc386dab4e	[ cleanup ] bring formatting of sc-graphs in tests back in sync	2023-11-06 20:10:21 +00:00
Justus Matthiesen	ba19fae07a	[ fix ] handle printing of empty matrices gracefully	2023-11-06 20:10:21 +00:00
Justus Matthiesen	39f3aeeb08	[ cleanup ] remove 1 suffix from Vector1 functions	2023-11-06 20:10:21 +00:00
Justus Matthiesen	291d60da08	[ cleanup ] move auxiliary function to where block	2023-11-06 20:10:21 +00:00
Justus Matthiesen	03484f2dfa	[ cleanup ] split Vector and Vector1 into separate namespaces	2023-11-06 20:10:21 +00:00
Justus Matthiesen	c36be9291d	[ doc ] clarification on neutrals	2023-11-06 20:10:21 +00:00
Justus Matthiesen	c36625d1db	[ cleanup ] remove duplicate and unused functions	2023-11-06 20:10:21 +00:00
Justus Matthiesen	d9cc448d3e	[ debug ] sc-graphs now have labels "l" and "r" for LHS and RHS	2023-11-06 20:10:21 +00:00
Justus Matthiesen	8c7c59a5d0	[ new ] labels for pretty-printed sparse matrices	2023-11-06 20:10:21 +00:00
Justus Matthiesen	8822040f37	[ new ] replicateChar, an analogue to spaces but for arbitrary Chars	2023-11-06 20:10:21 +00:00
Justus Matthiesen	80657feb34	[ doc ] sparse matrix invariants	2023-11-06 20:10:21 +00:00
Justus Matthiesen	e5788a3e86	[ test ] tracking size-change across applications	2023-11-06 20:10:21 +00:00
Justus Matthiesen	f435256812	[ test ] tracking size-change in dot patterns	2023-11-06 20:10:21 +00:00
Justus Matthiesen	2798d8f226	[ cleanup ] update expected test outputs ... Changes to the termination checker brought along some otherwise insignificant changes to debug and error messages.	2023-11-06 20:10:21 +00:00
Justus Matthiesen	b3c186900c	[ fix #2954 ] use matrices to represent sc-graphs ... We also update sc-graph generation to - fully traverse `As` patterns - go under `Dotted` patterns - consider `f x <= f`	2023-11-06 20:10:21 +00:00
Justus Matthiesen	c4677edc5f	[ new ] Pretty instance for SizeChange	2023-11-06 20:10:21 +00:00
Justus Matthiesen	8a9bf396ea	[ new ] semiring instance for SizeChange	2023-11-06 20:10:21 +00:00
Justus Matthiesen	aac6e8600c	[ new ] sparse matrices	2023-11-06 20:10:21 +00:00
Justus Matthiesen	4f7f5a2ed4	[ cleanup ] use information order for SizeChange	2023-11-06 20:10:21 +00:00