14 Commits

Author	SHA1	Message	Date
Arnaud Bailly	cb6ce92cbb	use regexp to validate idris version	2019-07-26 16:44:27 +02:00
Arnaud Bailly	6c1c865587	check idris version before building	2019-07-26 09:52:45 +02:00
Kamil Shakirov	85a1f9becc	Fix makefile's 'install-exec' target	2019-07-15 12:42:54 +06:00
Edwin Brady	0d5dc8cc26	Check delay is allowed before delaying ... We can't nest delayed elaborators (this is an efficiency constraint, to prevent excessive searching for ambiguous names) to run elaborator immediately if delays aren't allowed in delayElab	2019-07-14 11:23:58 +01:00
Matthew Wilson	8167197a4b	idk	2019-07-12 07:06:25 -04:00
Matthew Wilson	b7a11bd22c	enable install-libs workflow and the typical install behavior	2019-07-12 07:04:36 -04:00
Matthew Wilson	8f4c35a7b5	install target depend on all target	2019-07-11 22:44:21 -04:00
Niklas Larsson	28438650d0	windows support	2019-07-10 01:51:41 +02:00
Edwin Brady	38443e23a3	Need to build 'libs' before running tests	2019-07-09 09:31:35 +02:00
Edwin Brady	c121910298	Add 'base' libraries	2019-06-15 11:54:22 +01:00
Edwin Brady	2c1c86639a	Update makefiles and paths ... We can now build and install the prelude, and hello world has successfully compiled to chez	2019-06-13 16:53:16 +01:00
Edwin Brady	146c301f6c	Change main program to be Idris2 ... With the --yaffle flag, you get the old behaviour which is to invoke the checker for the core theory (and all the tests are updated appropriately for this).	2019-06-09 11:58:29 +01:00
Edwin Brady	411b8ccc07	Support eta in unification ... Also added (necessarily) a rule for lambdas	2019-05-07 15:06:00 +01:00
Edwin Brady	77bf4c7c44	Added test framework (copied from Blodwen)	2019-05-07 10:43:02 +01:00