Commit Graph

10 Commits

Author SHA1 Message Date
André Videla
274954998b
Implement generic interpolation (#1967)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-13 17:26:54 +01:00
Edwin Brady
1e90182311
Version increment to 0.5.1 (#1939)
This is to remove the requirement on Chez >9.5
2021-09-19 20:53:32 +01:00
Edwin Brady
ada3eb4449
Version 0.5.0 (#1931)
* Update version numbers and bootstrap scheme

* Use wall clock time for search timeouts

That was always the intention in any case, rather than the process time.
2021-09-18 16:07:34 +01:00
Edwin Brady
a0cfa28621 Update version numbers 2021-06-23 16:15:21 +01:00
Edwin Brady
4726c32d94 Add --ignore-missing-ipkg flag
When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.

We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!
2021-02-27 19:39:47 +00:00
Edwin Brady
1052c41a3c Use version number field in ipkg
Packages are now installed in a directory with their version number.
On adding a package directory, we now look in a local 'depends'
directory first (to allow packages to be installed locally to another
project) before the global install directory.
Dependencies can have version bounds (details yet to be implemented) and
we pick the package with the highest version number that matches.
2021-02-27 14:15:19 +00:00
Stiopa Koltsov
901a15e8f8 Move Cast interface to Prelude.Cast
Extract 200 lines file from 1000 lines `Prelude/Types.idr`.  To
make code more discoverable.
2021-01-27 18:31:43 +00:00
Edwin Brady
6a53e0177c Reorganise prelude into multiple files
This is partly to tidy things up, but also a good test for 'import as'.
Requires some internal changes since there are parts of reflection,
unelaboration and a compiler hack that rely on where things are in the
Prelude.
2020-07-12 16:55:48 +01:00
Stiopa Koltsov
c140605a0f Extract Prelude.Basics, Prelude.Uninhabited from Prelude 2020-06-22 18:10:06 +01:00
Edwin Brady
dec7dff622 Add libraries 2020-05-18 14:00:08 +01:00