Commit Graph

513 Commits

Author SHA1 Message Date
Edwin Brady
0a985a2815
Merge pull request #278 from edwinb/buffer-prims
Make buffers more primitive
2020-06-11 16:03:45 +01:00
Niklas Larsson
0a4667c589
Merge pull request #277 from melted/fix_autocrlf
Disable autocrlf on WIndows CI
2020-06-11 16:37:59 +02:00
Niklas Larsson
5858365f18 Disable autocrlf on WIndows CI 2020-06-11 16:25:48 +02:00
Edwin Brady
07ae16123c Only open in binary mode on windows 2020-06-11 14:53:54 +01:00
Jinwoo Lee
5eb86af435 Add some comments about TakeN in chapter 10.
The `rest` argument must be made explicit. Related to
https://github.com/idris-lang/Idris2/issues/253.
2020-06-11 14:51:06 +01:00
Edwin Brady
4b1667fdcf Open files in binary mode
Needed for windows, and harmless on Unix (Idris 1 did it this way).
2020-06-11 14:35:26 +01:00
Niklas Larsson
7194ad11af
Merge pull request #273 from melted/full_bootstrap
Add a bootstrap from Idris 1 CI script
2020-06-11 15:13:57 +02:00
Niklas Larsson
015f195b87
Merge pull request #272 from melted/fix_primitive_bootstrap
Use 2^64 constant instead of calculation
2020-06-11 15:13:40 +02:00
Edwin Brady
0a246af449 Make Buffer more primitive
Meaning that the FFI is aware of it, so you can send arbitrary byte data
to foreign calls. Fixes #209

This means that we no longer need the hacky way of reading and writing
binary data via scheme, so can have a more general interface for reading
and writing buffer data in files.

It will also enable more interesting high level interfaces to binary
data, with C calls being used where necessary.

Note that the Buffer primitive are unsafe! They always have been, of
course... so perhaps (later) they should have 'unsafe' as part of their
name and better high level safe interfaces on top.

This requires updating the scheme to support Buffer as an FFI primitive,
but shouldn't affect Idris2-boot which loads buffers its own way.
2020-06-11 14:05:52 +01:00
Niklas Larsson
b5f67b94ae Use constants instead of calculation for upper bounds
Add wrapping to 8-bit adding.

This is a workaround to fix the bootstrap
Fixes #268
2020-06-11 14:23:41 +02:00
Jan de Muijnck-Hughes
49b4f97c5d Added some modest improvements to code. 2020-06-11 12:51:47 +01:00
Jan de Muijnck-Hughes
ef85348de8 Update src/Text/Literate.idr
Improve efficiency of lexer for code lines.

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2020-06-11 12:51:47 +01:00
Jan de Muijnck-Hughes
63e127094e Improved parsing for literate modes.
The tokenizer for literate modes was incorretly detecting code lines in text.
This PR fixes that, and allows for empty code lines.
2020-06-11 12:51:47 +01:00
Niklas Larsson
fc322bd699 Add a bootstrap from Idris 1 CI script 2020-06-11 12:20:50 +02:00
Edwin Brady
d71bfef73f
Merge pull request #266 from edwinb/vis-case-with
Propagate visibility appropriately to case/with
2020-06-10 13:53:17 +01:00
Edwin Brady
df3449f44b Fix the other clashing test output
I don't understand the difference here - there's probably a commit I
hadn't merged earlier that affected the name generation.
2020-06-10 13:08:50 +01:00
Edwin Brady
c07876d1a3 Fix clashing test output 2020-06-10 12:53:18 +01:00
Edwin Brady
004b41a3d8 Merge https://github.com/idris-lang/Idris2 into vis-case-with 2020-06-10 12:50:30 +01:00
Edwin Brady
42676d2504
Merge pull request #265 from edwinb/find-ipkg-ide
In IDE mode, look for a ipkg file before loading
2020-06-10 12:42:59 +01:00
Edwin Brady
0cc54ff145 Propagate visibility appropriately to case/with
If a function is public export, the local definitions also need to be
public export for it to reduce properly. But if they're not, we don't
want them exported or they might affect the module hash and cause
unnecessary rebuilds.
2020-06-10 12:41:02 +01:00
Jan de Muijnck-Hughes
90fb901c8f Fix test reporting when in interactive mode.
When runing in interactive mode, the diff between expected and output is not being show,
Supposedly, Git-diff returns 0 on successful run and a non-zero for error.
However, this is not being picked up by the test suite.

We change git-diff's error reporting to be more diff like in which:

+ +ve indicates that there is a diff.
+ 0 indicates the files are the same.
+ -ve program error.

This should make diff reporting more robust.
2020-06-10 09:30:02 +01:00
Edwin Brady
cf23bae7d6 In IDE mode, look for a ipkg file before loading
This takes the responsibilty of finding the ipkg away from IDE mode,
which seems sensible given that we can do it ourselves. If there isn't
one, it'll load from the local directory as always.
2020-06-09 23:31:30 +01:00
Edwin Brady
b88f425a57
Merge pull request #257 from edwinb/finalisers
Add finalisers to Chez and Racket back ends
2020-06-08 22:59:48 +01:00
Edwin Brady
ca28dab1d7 Add finalisers for Racket back end
Like Chez, we also need an explicit call to the garbage collector at the
end to ensure that all the finalisers get run on exit.
2020-06-08 22:13:24 +01:00
Edwin Brady
e32f039227 Fix includes in chez022 test 2020-06-08 20:46:25 +01:00
Edwin Brady
d60feaace0 Add finalisers to Chez back end
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.

In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...

This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
2020-06-08 20:34:23 +01:00
Edwin Brady
2c77c38f1f Merge branch 'nickdrozd-nats' 2020-06-08 13:22:46 +01:00
Edwin Brady
85bd751283 Update reflection test again 2020-06-08 13:22:18 +01:00
Edwin Brady
4cc4099ace
Merge branch 'master' into nats 2020-06-08 12:11:10 +01:00
Edwin Brady
d6e3f1f746
Merge pull request #100 from ska80/use-contrib
Use Control.Delayed from the 'contrib' package
2020-06-08 12:07:09 +01:00
Edwin Brady
abcb1b417f
Merge pull request #248 from vilunov/repl-let
":let" command for REPL
2020-06-08 12:00:15 +01:00
Edwin Brady
ff56062a5e
Merge pull request #244 from xoltar/ipkg-format-docs
Update docs to reflect changes to ipkg format
2020-06-08 11:55:46 +01:00
Edwin Brady
73de552776
Merge pull request #239 from MarcelineVQ/elab-changes
add parens for some TTImp Shows
2020-06-08 11:54:19 +01:00
Edwin Brady
6b0118d7ca
Merge pull request #227 from clayrat/master
add Data.Fuel
2020-06-08 11:46:48 +01:00
Edwin Brady
3a0a907c0b
Merge pull request #226 from ShinKage/auto-implicit-depth
Added auto_implicit_depth pragma
2020-06-08 11:45:33 +01:00
Edwin Brady
59025b0a85
Merge pull request #183 from keram/remove-clang
Remove clang from config.mk
2020-06-08 11:42:37 +01:00
Edwin Brady
47c0675e49
Merge pull request #254 from edwinb/test-fix
Update test output
2020-06-08 11:01:27 +01:00
Edwin Brady
4834f2f78c Update test output
Clash in a reflection test due to conflicting merges. I'd like to find a
way to make the internally generated numbers not matter here (and
elsewhere) but I don't see an obvious way.
2020-06-08 10:39:58 +01:00
Edwin Brady
e033609310
Merge pull request #207 from mb64/assert_smaller-linear
Make assert_smaller and assert_total linear
2020-06-08 10:19:33 +01:00
Edwin Brady
0b20fe2412
Merge branch 'master' into remove-clang 2020-06-08 10:18:31 +01:00
Edwin Brady
8f80e77678
Merge pull request #122 from keram/install-impro-v2
Add additional information on requirements in INSTALL.md
2020-06-08 10:16:40 +01:00
Edwin Brady
7455a7c9f3
Merge pull request #232 from mb64/no-thin
Remove redundant thin functions and replace with insertNames
2020-06-08 10:15:17 +01:00
Edwin Brady
f9fc61ad4c
Merge pull request #252 from edwinb/totality-case
Case block improvements
2020-06-08 01:35:53 +01:00
Edwin Brady
0f27042b32 Fix build given new case elaboration rule
Actually this was an error in Core.Directory, so the change has caught
it! Always nice to see that happen on making an improvement...
2020-06-08 01:14:06 +01:00
Edwin Brady
1057cb9314 Go into case branches when productivity checking
We were only looking inside the branches for termination checking, so
this might have missed some non-productive things.
2020-06-08 01:10:07 +01:00
Alex Gryzlov
14002213a1 Merge remote-tracking branch 'upstream/master' 2020-06-08 00:27:58 +02:00
Edwin Brady
d47d495744 Free standing case blocks return ()
Fixes #116. This is the solution Idris 1 took, and while it is a special
case, the syntax does make it explicit (in a way) that the result of the
case is unused - if you mean something other than (), you must now say
so!
2020-06-07 22:49:19 +01:00
Nick Drozd
85c1e62587 Update test 2020-06-07 14:17:17 -05:00
Nick Drozd
5665cfab21 Copy over more Nat proofs 2020-06-07 12:19:32 -05:00
Nick Drozd
4292d735eb Simplify Nat proofs
These changes are strictly nonfunctional.
2020-06-07 12:19:32 -05:00