Commit Graph

163 Commits

Author SHA1 Message Date
Niklas Larsson
9662ab5e4a Disable travis for GHC 8.8 (libffi still broken)
Update changelog

Use GHC 8.8 in Appveyor

Run legacy test commands
2020-01-25 18:48:50 +01:00
Edwin Brady
9549d9cb9a Update version numbers ready for release 2019-07-22 12:09:06 +01:00
Jan de Muijnck-Hughes
dbf060cf17 Updated changelog and add GitHub issue reference: Fixes #4702 2019-05-16 11:14:21 +01:00
Matus Tejiscak
11b4fb16ff Rename to --optimise-nat-like-types. 2019-04-05 11:09:41 +02:00
Niklas Larsson
9d03084a33
Merge pull request #4658 from martinbaker/mydoc
add to proof documentation
2019-03-21 15:09:24 +01:00
Niklas Larsson
56c20587e8 Make binary files the default when opening.
The reason is that most things on windows handles unix line endings just
fine and this leads to terrible bugs when writing binary files.

fopen still allows opening of files without the "b".

This only has effect on Windows, but POSIX systems allows the "b" as a
noop.
2019-03-12 00:46:38 +01:00
Martin Baker
80636c0f24 add to proof documentation 2019-02-23 08:32:21 +00:00
Edwin Brady
8362faae46 Slightly better hashing function for interfaces
The previous one would have given the same result if swapping a name and
a type... oops!
2018-10-24 13:47:45 +01:00
Edwin Brady
2699ce128b Update CHANGELOG 2018-10-23 10:16:15 +01:00
Niklas Larsson
faf1d6727c
Add fixes to changelog 2018-09-29 12:18:21 +02:00
Edwin Brady
61cf812e97 Update version number 2018-05-26 17:55:45 +01:00
Niklas Larsson
40a58fe55d
Update CHANGELOG with the closure work. 2018-04-02 19:17:12 +02:00
Niklas Larsson
069f34469e
Add GHC 8.4 fixes to CHANGELOG 2018-03-31 15:44:50 +02:00
Ahmad Salim Al-Sibahi
eb41a1d67c Allow capitalized pattern variables via switch 2018-03-03 12:49:44 +01:00
Ahmad Salim Al-Sibahi
cc7ef9adaf
Remove old eliminator generation and induction tactic (#4351)
* Remove old eliminator generation and induction tactic

* Run stylize
2018-02-25 20:26:29 +01:00
Patrick Hilhorst
2be6e6a7d9 Various additions to contrib (#4343)
* Wrote Data.{SortedBag,ArrowChain,PosNat}

* Added some more docs to Data.SortedBag

* Renamed ArrowChain to Chain

* Added `null` to Data.SortedMap

* Edited CHANGELOG

* Edited contrib.ipkg

* Fixed tiny typo
2018-02-23 09:36:36 +01:00
martinbaker
fab2841112 fix for odd-even bug in random (#4339)
* fix for odd-even bug in random

* edit CHANGELOG and remove TODO

* modify tests to conform to new random values

* fix effects003
2018-02-22 10:37:46 +01:00
Ilya Yanok
8e2aff5c83 Print error message if :exec'ed program exits with failure
Check the result code of the compiled program and print an error message if it
didn't return success.
2018-02-06 17:56:33 +01:00
Edwin Brady
d77513b966 Update version number properly this time (sorry!) 2018-01-07 18:10:44 +00:00
Edwin Brady
ab806e9dde Update version number 2018-01-07 18:07:51 +00:00
Edwin Brady
a9b30adea2
Merge pull request #4280 from asandroq/set-build-env-flags
Set environment with Idris flags while running `make`
2018-01-07 18:04:02 +00:00
Melvar Chen
d1fae54cd2
Merge pull request #4260 from Melvar/let-alternatives
Add alternatives syntax to `let` in `do` blocks
2018-01-04 23:31:09 +01:00
Alex Queiroz
946c9e10d9 Set environment with Idris flags while running make
When building a package with foreign code and a makefile, the makefile
itself must find the compilation flags that Idris already knows
about. Moreover, the `idris` executable found by the makefile may not
be the same used to build the package. This change passes the build
flags to the makefile though environment variables.
2018-01-04 12:55:29 +01:00
Jason Felice
a037d4cb62 Fix up CHANGELOG.md 2017-12-23 19:32:03 -05:00
Melvar Chen
b3ee2df5ca Update the changelog 2017-12-22 07:26:27 +01:00
Jason Felice
117a8ecb54 Merge remote-tracking branch 'upstream/master' into pretty-warnings 2017-12-21 08:33:41 -05:00
Jason Felice
c20e139882 Merge remote-tracking branch 'upstream/master' into deprecated-parser-features 2017-12-18 10:11:12 -05:00
Ahmad Salim Al-Sibahi
54049341df
Merge pull request #4226 from XeFias/contrib_ST_File
First attempt at implementing ST alternative for File.idr in Effects.
2017-12-14 16:39:20 +01:00
Jason Felice
0bb18f1111 Add CHANGELOG entry 2017-12-07 10:18:03 -05:00
Ahmad Salim Al-Sibahi
5218727b2f
Merge pull request #4245 from msmorgan/data-fuel
Data.Fuel: move `Fuel` data type from Control.ST to its own module
2017-12-06 09:33:53 +01:00
Jason Felice
4f19553b61 Merge remote-tracking branch 'upstream/master' into deprecated-parser-features 2017-12-05 20:36:37 -05:00
Xefias
b4b4641315 Updated comments according to review comments:
- Updated CHANGELOG
- Improved description of `Control.ST.File` interface and `FileHandle` type.
- Removed commented code.
2017-12-05 21:33:42 +01:00
Michael Morgan
99f0d60a4d add CHANGELOG entry for Data.Fuel 2017-12-05 14:31:03 -06:00
Michael Morgan
27bf213895 add CHANGELOG entry for Language.JSON 2017-12-05 12:51:44 -06:00
Jason Felice
57b64a7f69 Remove deprecated 'public' without 'export' 2017-12-04 15:14:41 -05:00
Jason Felice
e35d64377c Remove deprecated [static] keyword 2017-12-04 15:13:41 -05:00
Jason Felice
4c40a7260b Remove deprecated %assert_total 2017-12-04 15:13:05 -05:00
Jason Felice
0cfc98cf79 Remove long-deprecated abstract 2017-12-04 13:31:58 -05:00
Jason Felice
b1a4264f7c Improve error message locations (#4210)
This contribution uses the strict WriterT transformer over our parser stack with a
monoid over FC and what used to be spanFC to compute the span of
non-terminal parsers from the spans of trackExtent-wrapped parsers.

The net result is that the locations reported for errors and warnings is
much improved. Most errors now report the extent of the error, rather than a
point roughly preceeding it (or after it, sometimes). There are still cases
where FCs are recomputed as a point after parsing--I didn't fix these, to cut
the scope of this PR--though all file locations produced during parsing use
the new, spanning parsing combinators.

I would start reading at Idris.Parser.Stack, then Idris.Parser.Helpers.

Overview:    
- *FC and non-*FC parsers (e.g. tokenFC and token, charLiteralFC and
    charLiteral, etc.) have been elided and the FC suffix removed. Any
    parser can be asked to report it's FC using the extent or withExtent
    combinators.
    
- Extents reported for errors end at the last character of the token, rather
    than on the following character.
 
- Now that all parsers can be queried for their spans, highlighting is
    done with the highlight parser combinator, e.g.
    highlight AnnQuasiquote (symbol "`{{" ...). These can be nested.
   
- Totality checking, in its current design, reports the extent of the first
    equation. This is a bit more misleading now that the span is computed
    correctly, since it could look like it's trying to indicate which clause is
    non-total. We should fix this (hopefully as a separate PR.)
   
- The span of clauses is actually the span of the right-hand side, and so this
    is reported when there is an error on the right-hand side or the left-hand
    side. We should also fix this (hopefully as a separate PR.)
    
- There's probably cases where, owning to the improved granularity, we will now
    notice errors were reported with FCs from the wrong object.
    I haven't tested an IDE-mode client yet. They may need to be patched if they
    are manually excluding the last character of tokens. Highlighting appears to
    work fine without changes, though.
2017-11-30 12:18:36 +01:00
Niklas Larsson
f452b923b0 Add changelog item for C FFI #-prefix 2017-11-25 12:52:52 +01:00
Michael Morgan
612f918afd update CHANGELOG.md with new verbatim string behavior 2017-11-16 17:54:03 -06:00
Niriel
cc1c4ed0ec Sync issue_3500 with upstream/master. 2017-11-12 12:47:27 +01:00
Jan de Muijnck-Hughes
d2f638235f Updated the CHANGELOG. 2017-11-13 11:24:24 +00:00
Niriel
2a6dce9190 Moved abs from the Neg interface into its own Abs interface. (Issue 3500) 2017-11-10 19:44:06 +01:00
Jan de Muijnck-Hughes
28fc3908ff Updated the changelog. 2017-11-09 10:12:50 +00:00
Ahmad Salim Al-Sibahi
249ff98d7b
Fix indentation of CHANGELOG
[noci]
2017-11-08 21:21:40 +01:00
Ahmad Salim Al-Sibahi
8da55c2505 Add CHANGELOG entry and test 2017-11-08 21:10:01 +01:00
Alex Queiroz
e61c630166 Update changelog with changes for atan2 2017-11-04 00:26:41 +01:00
Jason Felice
edfc5e373e Add CHANGELOG message 2017-11-02 21:16:33 -04:00
Michael Morgan
5856a77cb7 update CHANGELOG for recent updates 2017-11-01 09:48:38 -05:00