Commit Graph

15 Commits

Author SHA1 Message Date
Arnaud Bailly
eb760fe20c
fix correct version to 1.3.2 2019-07-26 20:10:22 +02:00
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