Commit Graph

51 Commits

Author SHA1 Message Date
G. Allais
f72f91c67a
[ fix ] build by installing support before tests (#369) 2020-05-12 15:23:42 +01:00
Edwin Brady
6681131957 Make a start on C support code
It would be nice to have some common routines that all back ends that
can talk to C can use, rather than relying on Scheme for standard
library code.
2020-05-11 18:10:08 +01:00
Edwin Brady
15c6a0d137 Remove chicken back end
(Which was commented out anyway)
Three scheme back ends is enough to maintain, and Gambit does the same
job as chicken (fast startup of the interpreter, generating via C) but
seems to deal with the code Idris generates better.
2020-05-09 13:57:27 +01:00
Abdelhakim Qbaich
1bbf662609 Preparation for the Gambit Scheme backend 2020-05-01 23:27:36 -04:00
Ben Davies
93871c5fb9 Fix builds on *BSD
This makes it so gmake gets used instead of make on *BSD, refactors how
platforms are handled in general.
2020-04-22 11:09:05 -03:00
Edwin Brady
7f4659814c Set version number to 0.1.0 2020-03-31 22:41:15 +01:00
Edwin Brady
28f47963df
Merge pull request #215 from ska80/fix-bsd-sed
Make BSD 'sed' happy
2020-03-07 14:06:38 +00:00
Edwin Brady
2eb9a52727 Tests need to know where to find idris_net.so 2020-03-06 15:38:47 +00:00
Kamil Shakirov
2d1f35ab21 Fix indentation 2020-03-06 12:36:43 +06:00
Kamil Shakirov
0e01c2aa0b Make BSD 'sed' happy 2020-03-06 12:32:16 +06:00
Edwin Brady
edc3e2a4cd Need the network libs in the path for tests 2020-03-05 18:46:26 +00:00
Edwin Brady
2c2acdcfac Reorganise build system to go via generating C
This has two main advantages: firstly, it actually makes the build slightly
faster and less memory intensive, because Idris doesn't fork a new
process and eat all the memory! Secondly, it means we can build a
distribution with the C file, for building on machines which don't have
Idris 1 available.

Also includes a script for building such a distribution.

I expect someone who is better a writing Makefiles than me can tidy this
up. There are almost certainly problems on Windows too - please help if
you can!

There are new Make targets 'all-fromc' and 'install-fromc' which don't
require building from Idris source, so that we can build with no Idris 1
available.

A small consequence: make install-exec no longer builds the idris2
executable, just installs it.
2020-03-05 17:16:20 +00:00
Kamil Shakirov
b38f6f98c6 Improve 'idris2c' makefile target 2020-02-26 13:00:25 +06:00
Edwin Brady
da675b38a0 Add some machinery to generate C
This is towards making a distribution that allows building from C,
rather than having to build from the Idris source, to make it easier to
install.
2020-02-25 14:09:08 +00:00
Edwin Brady
0cb446dd31 Only use version tag in display
Not in generating install directories, otherwise we end up with loads of
new directories for every patch and the purpose is to make it easy to
see which version you're working with.
2020-01-30 18:25:18 +00:00
Ohad Kammar
be90749e22 Create a contrib directory in the standard library
Move the TailRec.idr and current poor-man's syntax for:
  equational reasoning (`Syntax.PreorderReasoning`)
  with proof           (`Syntax.WithProof`)
2020-01-09 12:54:55 +00:00
lodi
76ff99d370 allow overriding racket/chicken paths through environment variables
This is to help Idris2 codegen the correct scripts on NixOS where
Racket and Chicken aren't installed in the standard locations, and
the /usr/bin/env trampoline is disabled at package build time.
This now matches the existing Chez behavior.

Also, fixed the test runner to restore the correct working directory
after a failed test, and fixed the top-level Makefile to allow the
IDRIS2_VERSION variable to be queried without building the project.
2019-10-28 22:44:16 -04:00
Kamil Shakirov
b87fd0beb3 Add optional version tag when build in between releases
Also add REPL :version command to show the current version
2019-10-14 12:01:29 +06:00
Edwin Brady
bf69b89b0d Support for buffers and file erros in Racket CG 2019-09-28 18:10:14 +01:00
Arnaud Bailly
c80bfc0ed7 fix incorrect variable in makefile preventing install 2019-09-22 22:43:08 +02:00
Arnaud Bailly
2f8daa7cf2 Merge branch 'master' of https://github.com/edwinb/Idris2 into add-version-command 2019-09-22 22:39:36 +02:00
Arnaud Bailly
9c1f8b6f02
Merge branch 'master' into add-version-command 2019-09-22 15:50:13 +02:00
Edwin Brady
65b3ddb81b Add --libdir option
This makes it easier for more complicated packages (e.g. network, which
needs to install a C shared library) to know where to put things without
having to work out the prefix themselves.
2019-09-19 13:04:39 +01:00
Arnaud Bailly
295058130e
Merge branch 'master' into add-version-command 2019-09-13 17:33:14 +02:00
Edwin Brady
412930522e Put idris version number in package install path
Since they'll be incompatible between different Idris2 versions, this
helps protect against importing the wrong thing by mistake. Also, it
means the canonical place for the version number is now the top level
Makefile.

You'll need to delete src/YafflePaths.idr before rebuilding, since it's
now generated slightly differently.
2019-09-04 16:20:26 +01:00
Edwin Brady
65db4fbf96 Put built ttcs in build/ttc, rather than build
This is so that we can put other build artefacts (e.g. executables) in
properly organised subdirectories of build, e.g. build/bin/chez,
build/bin/js, etc.
2019-09-04 12:41:16 +01:00
Arnaud Bailly
09f71182b5
expose version components in Makefile 2019-08-29 14:37:38 +02:00
Arnaud Bailly
643fc9c4c7
provide Version command in ide-mode 2019-08-29 14:37:38 +02:00
Arnaud Bailly
4646bb0d1c
expose current Idris2 version as a proper type 2019-08-29 14:37:04 +02:00
Arnaud Bailly
4d3e190e90
Merge branch 'master' of https://github.com/edwinb/Idris2 into network-lib 2019-07-28 23:00:07 +02:00
Christian Rasmussen
e82a0c6acb Add instructions on how to run a subset of the tests 2019-07-28 20:21:34 +02:00
Christian Rasmussen
54f00e9247 Run individual tests (Fixes #23) 2019-07-28 18:54:23 +02:00
Edwin Brady
d5409ac2d0 Add 'libs' directory to paths
This is for finding support libraries for code generators, e.g. the
shared objects that chez will load for glue code for foreign libraries.
It'll be used more shortly...
2019-07-28 11:48:00 +01:00
Arnaud Bailly
02978c81fc
Merge branch 'master' of https://github.com/edwinb/Idris2 into network-lib 2019-07-27 17:27:49 +02:00
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
Arnaud Bailly
a87639d53a
refactor code to be more compact
uses alternative branches for failed pattern matches in do-notation
2019-07-26 09:51:49 +02:00
Arnaud Bailly
18d83420da
initial import of idris 1 network lib 2019-07-22 17:24:55 +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