idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-30 15:13:37 +03:00
Code Issues Projects Releases Wiki Activity
2,703 Commits 6 Branches 9 Tags 116 MiB
1ba0008486
Commit Graph

2703 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
050abe663e
Merge pull request #1638 from stepancheg/idris2-time 
Use C idris2_time for all C-based backends
 2021-07-16 09:40:08 +01:00
Edwin Brady
69663735f4
Merge pull request #1680 from stepancheg/buffer-buffer 
Remove Value_Buffer.len field
 2021-07-16 09:22:48 +01:00
Edwin Brady
59387fc87b
Merge pull request #1679 from stepancheg/new-value 
In RefC, allocate the exact size of value subtype
 2021-07-16 09:22:10 +01:00
Edwin Brady
6143508f7b
Merge pull request #1659 from stepancheg/verify 
IDRIS2_VERIFY macro
 2021-07-16 09:01:31 +01:00
Thomas E. Hansen
7e904ecdef
Update %hide help to show it takes a 'name'. 2021-07-16 09:58:33 +02:00
Edwin Brady
a20aba63ee
Merge pull request #1448 from mattpolzin/case-tree-experiments-merge-upstream 
Case tree heuristics
 2021-07-16 08:47:19 +01:00
Edwin Brady
37475d722a
Merge pull request #1720 from ShinKage/reflection-fix 
Fixed wrong reflection of records and parameters
 2021-07-16 08:40:58 +01:00
Giuseppe Lomurno
37c700907e Removed leak of internal names from test reflection010 2021-07-16 04:28:58 +02:00
Giuseppe Lomurno
07c62e9eef Fixed wrong reflection of records and parameters 2021-07-16 04:28:52 +02:00
Mathew Polzin
6c24b9ea7d fix bad merge conflict resolution. 2021-07-15 17:27:35 -07:00
Mathew Polzin
ec3b868cb6 rename experimental command line flag and group with the other experimental feature. 2021-07-15 17:24:12 -07:00
Mathew Polzin
89125e96dd merge w/ upstream 2021-07-15 17:21:08 -07:00
Edwin Brady
a880b9884c
Merge pull request #1670 from stepancheg/buffer-names 
Add parameter names to Buffer builtins parameter names
 2021-07-16 00:53:42 +01:00
Edwin Brady
f0df67a2fe
Merge pull request #1656 from stepancheg/bootstrap-build 
Write files into bootstrap-build directory during bootstrap
 2021-07-16 00:22:23 +01:00
Edwin Brady
3c88c33f15
Merge pull request #1452 from nickdrozd/emacs-doc 
Update Emacs idris-mode doc
 2021-07-15 23:38:26 +01:00
Edwin Brady
f4cc2f1ea8
Merge pull request #1721 from edwinb/AliasQli-master 
Updated: add doublePow to primitives
 2021-07-15 23:17:53 +01:00
Stiopa Koltsov
c80a502627 Return Bool from IOArray.writeArray 
As suggested in #1677.

Crashing on out-of-bounds might be more practical, but we can
reconsider it later.
 2021-07-15 22:16:22 +01:00
Edwin Brady
f51aa22046 Bring #1719 up to date with latest changes 2021-07-15 22:04:49 +01:00
Edwin Brady
4079ae0e25 Merge branch 'master' of https://github.com/AliasQli/Idris2 into AliasQli-master 2021-07-15 21:44:26 +01:00
Edwin Brady
50c0116780
Merge pull request #1718 from edwinb/Russoul-unification 
Postpone when instantiating if type is unknown
 2021-07-15 21:16:00 +01:00
André Videla
e45d792283
Merge pull request #1701 from mattpolzin/alternative-errors 
Show error output from multiple alternative parsing branches.
 2021-07-15 20:06:25 +00:00
Edwin Brady
a709f6d369 Fix/reorganise tests 2021-07-15 20:24:40 +01:00
Edwin Brady
d9a56c5fd1 Merge branch 'unification' of https://github.com/Russoul/Idris2 into Russoul-unification 2021-07-15 20:24:27 +01:00
Mathew Polzin
883097e907 whitespace lint fix 2021-07-15 12:09:15 -07:00
Mathew Polzin
948a5ba9df noticed I was not _quite_ retaining existing behavior around Alt error processing so fixed that. updated tests. 2021-07-15 12:05:23 -07:00
Edwin Brady
fbb277f8e9
Merge pull request #1715 from edwinb/buzden-name-quote-single-brace 
Name quotes are suggested to use single brace instead of double
 2021-07-15 19:15:19 +01:00
Arnaud Bailly
ae0e4f4893
fix returned sexp for make-lemma command result (#570) 
the returned structure is inline with what Emacs idris-mode expects, so this fix
allows using C-c C-e on a hole and get it lifted as a toplevel definition
 2021-07-15 18:41:13 +01:00
Edwin Brady
b192be32b8 Merge branch 'name-quote-single-brace' of https://github.com/buzden/Idris2 into buzden-name-quote-single-brace 2021-07-15 17:57:41 +01:00
Fabián Heredia Montiel
dd7081e2fe Use --tag (non-reversed) variant of sha256sum for NetBSD compat 
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
 2021-07-15 11:54:10 -05:00
Fabián Heredia Montiel
9b8de95a38 Detect hashFn once 
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
 2021-07-15 11:54:10 -05:00
Fabián Heredia Montiel
106487ca59 [refactor] Move pathLookup from Compiler.Common to Utils.Path 2021-07-15 11:54:10 -05:00
Stiopa Koltsov
61e04e36cf Use gsha256sum when sha256sum doesn't exist 
On my mac laptop there's no `sha256sum` command, but there's
`gsha256sum`: using `g` prefix is common when GNU utilities are
installed on macOS.

```
SCHEME=chez make bootstrap
```

no longer fails on my laptop.

The downside is that compilation now continuously prints a warning
about `sha256sum` command not found (when it is not found).  And I
don't know how to fix it cross-platform way.

```
1/5: Building Network.Socket.Data (Network/Socket/Data.idr)
sh: sha256sum: command not found
2/5: Building Network.FFI (Network/FFI.idr)
sh: sha256sum: command not found
3/5: Building Network.Socket.Raw (Network/Socket/Raw.idr)
sh: sha256sum: command not found
4/5: Building Network.Socket (Network/Socket.idr)
sh: sha256sum: command not found
5/5: Building Control.Linear.Network (Control/Linear/Network.idr)
sh: sha256sum: command not found
```
 2021-07-15 11:54:10 -05:00
Edwin Brady
b8082f4ed7
Merge pull request #1714 from edwinb/lodi-thread-data 
fix arity for blodwen-set-thread-data
 2021-07-15 16:21:31 +01:00
Edwin Brady
267b8f5406
Merge pull request #1713 from edwinb/mb64-fix-unquote-thing 
Bring PR #530 up to date
 2021-07-15 16:21:17 +01:00
Edwin Brady
dad1804509 Fix for thread data in racket/gambit too 2021-07-15 15:12:50 +01:00
Edwin Brady
62586627d8 fix arity for blodwen-set-thread-data 
This is an update of PR #540, thanks to @lodi
 2021-07-15 15:02:43 +01:00
Mathew Polzin
8d8d3ef71e woops, missed the first let when resolving merge. thank goodness we are dealing with a static type system 2021-07-15 06:40:38 -07:00
Mathew Polzin
289f1cc954 merge w/ upstream. 2021-07-15 06:29:56 -07:00
Edwin Brady
f79ff202e7 Bring quotation fix up to date 
This is an update of PR #530 (Thanks to @mb64!)
 2021-07-15 14:29:12 +01:00
Edwin Brady
86aaed5ae1
Merge branch 'master' into fix-unquote-thing 2021-07-15 14:13:25 +01:00
Edwin Brady
15bc6a3980
Merge pull request #1708 from stepancheg/fork-io-array 
Fork Data.IOArray into the compiler
 2021-07-15 14:09:58 +01:00
Edwin Brady
35f23ac1d6
Merge pull request #1712 from edwinb/MarcelineVQ-elab-name-changes 
Add more name reflections
 2021-07-15 14:08:31 +01:00
Edwin Brady
9b0ebcd08b Merge branch 'elab-name-changes' of https://github.com/MarcelineVQ/Idris2 into MarcelineVQ-elab-name-changes 2021-07-15 13:16:47 +01:00
Guillaume ALLAIS
efcf44e8ba [ cosmetic ] use the whole range when underlining the problem 2021-07-15 07:32:43 +01:00
Mathew Polzin
221dadeb20 set default alt error count to 1 and create a config option that sets it to any number. 2021-07-14 20:23:29 -07:00
Mathew Polzin
1f21e787b1 Use commit to reduce the alternative parsing space as soon as an opening paren is encountered. 2021-07-14 17:22:40 -07:00
Stiopa Koltsov
47205049cf Fork Data.IOArray into the compiler 
To be able to modify `Data.IOArray` as proposed in #1677.

Currently `Data.IOArray` cannot be modified because compiler need
to be built with previous compiler. This PR removes compiler
dependency on `Data.IOArray`.
 2021-07-15 00:38:08 +01:00
Edwin Brady
8cd265cf47
Merge pull request #1698 from stepancheg/move-rm-rf-build 
Move rm -rf to the beginning of the test
 2021-07-14 16:00:46 +01:00
Edwin Brady
5cb77ad675
Merge pull request #1704 from edwinb/with-params 
Fix 'with' under implicit parameters
 2021-07-14 15:56:58 +01:00
Thomas E. Hansen
9fc3ee79e1
Merge branch 'master' into pragma-topic. 2021-07-14 16:45:05 +02:00