Commit Graph

2349 Commits

Author SHA1 Message Date
Edwin Brady
52c21c6182 Update bootstrap code
We shouldn't strictly need this, but it doesn't do any harm, and it also
means we can use --inc chez in the build if we do. Let's see if it helps
or hinders the CI problem...
2021-07-22 13:36:17 +01:00
Edwin Brady
e633a9fa6e Correct error018 test
I expect I got my local versions inconsistent while working on this...
2021-07-22 13:36:03 +01:00
Edwin Brady
edefd543f7 A bit of refactoring of argument elaboration order
In theory argument elaboration order doesn't matter, but in practice we
sometimes make choices for performance reasons, like helping with
disambiguation by knowing the target type.

This was kind of messy, now we can more clearly see what's going on.
Also, more importantly, it gives us a bit more control which we
sometimes need. For example, if we go choose to go right to left for
some performance heuristic it might turn out we don't have enough
information yet, in which case we need to delay and try again later.

Fixes #1743
2021-07-22 13:36:03 +01:00
G. Allais
9f0a70626a
[ ci ] turn ubuntu-bootstrap-racket off for now (#1772)
[ci: skip]
2021-07-22 12:27:34 +01:00
André Videla
5576d30c27
Merge pull request #1736 from stepancheg/test-discovery
Implement test discovery
2021-07-22 08:56:02 +00:00
G. Allais
34167d58bb
[ ci ] controlling builds via commit messages (#1766) 2021-07-21 16:49:32 +01:00
Ben Hormann
74db7714d4
[fix] Loading libidris2_support.dll with Racket (#1583) 2021-07-21 14:35:21 +01:00
Mathew Polzin
5f34801200 Make drop and drop' public exported from the vect module. 2021-07-20 14:27:43 +01:00
André Videla
ada33b90a1
Merge pull request #1756 from andrevidela/document-raw-strings
Document string literals
2021-07-19 19:38:47 +00:00
André Videla
440a3affd5
Update docs/source/reference/strings.rst
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-07-19 10:37:22 +00:00
Nick Drozd
ab36ad71cf Simplify a few Factor proofs
A few proofs have been rewritten, a few unnecessary cases cut, and
lots of unnecessary "explicit implicits" have been cut. Probably these
implicits were required when the code was initially written, and
inference has improved since then.
2021-07-19 08:30:47 +01:00
Stiopa Koltsov
eabab4bdea Split Windows CI build into multiple steps
It's easier to follow Windows CI output this way.
2021-07-19 08:02:06 +01:00
Edwin Brady
68db9fe0fe Add reg048 files
Odd, I thought I added these before, but it's probably because I got in
a mess with git and didn't re-add once I resolved that.
2021-07-19 00:21:28 +01:00
Edwin Brady
2068eb271b Better ordering of delayed elaborators
Instead of having an arbitrary looking priority number, record explicit
reasons for the delay, which helps order them sensibly when rerunning
them. Mostly this allows us to choose which ones to rerun, where it
helps, and helps order things to get better error messages.
2021-07-19 00:21:28 +01:00
André Videla
396ebe2023 Add documentation for new string literals 2021-07-18 22:32:26 +00:00
André Videla
9aa7a4303a Added documentation for new string literals 2021-07-18 21:37:20 +00:00
Edwin Brady
d1b1ec04cf Minor FAQ edits 2021-07-18 21:03:12 +01:00
Zoe Stafford
fe8b1d91da
Merge pull request #1737 from stepancheg/ref-assert
Assertions in RefC runtime
2021-07-18 20:49:38 +01:00
Niklas Larsson
706fb85b74
Merge pull request #1750 from melted/fix_link
Fix link to chez-exe
2021-07-18 19:45:54 +02:00
Niklas Larsson
ac595b1bb1 Fix link to chez-exe 2021-07-18 15:47:45 +02:00
Kenneth J Hughes
b663a06999 Update javascript.rst 2021-07-17 17:32:39 +01:00
Stiopa Koltsov
7325002dec Implement test discovery
`testInDir dir ...` lists all directories in `dir` which contains
`run` files, and such directories are considered tests.

This is done to make test addition/maintenance cheaper.

Convert some test directories to `testInDir`, but not all of them
because
* some directories are listed in several test groups
* other directories are have some tests disabled
2021-07-17 16:53:43 +01:00
Stiopa Koltsov
4eff6ac916 System.Directory.listDir
This function is what users want 99.9% of time.
2021-07-17 14:58:57 +01:00
Stiopa Koltsov
c7629e20fe Skip dot and dot-dot in nextDirEntry
These entries returned by `readdir` are legacy of Unix API, we don't
really need them. Most APIs do not return them (for example Java
`Files.newDirectoryStream` or Python `os.listdir`).
2021-07-17 14:58:28 +01:00
Stiopa Koltsov
0ecf74e434 System.Directory.nextDirEntry
* add `nextDirEntry` which returns `Maybe String`, so `Nothing` on
  the end of directory unlike `dirEntry` which returns unspecified error
  on the end of directory
* `dirEntry` is deprecated now, but not removed because compiler depends on it
* native implementation of `dirEntry` is patched to explicitly reset `errno`
  before the `readdir` call: without it end of directory and error were
  indistinguishable
* test added
2021-07-17 14:57:27 +01:00
Stepan Koltsov
ce44d3b50a
Change semantics of lines and unlines function to match Haskell and other languages (#1585)
* Add trailing newline on non-empty list in unlines

There are several reasons to do that:
* a line in a text file is something which ends with newline,
  and the last line is not special
* `unlines []` should be different from `unlines [""]`
* `unlines (a ++ b) = unlines a ++ unlines b`
* Haskell does it

* Change lines function behaviour
2021-07-17 14:54:23 +01:00
Ruslan Feizerakhmanov
ee063a5412
Apply "qualified do" notation to bangs and comprehensions (#1700)
* Propagate 'do qualification' to inner bangs and comprehensions

* Minor

* Remove banner in test

* Move tests from reg045 to reg047

* Move mbNS from Desugar.idr to Name.idr, renaming it to mbApplyNS
2021-07-17 14:52:22 +01:00
Stiopa Koltsov
5a351f4e7e Accept HasIO in onCollect functions
Since most functions work with `HasIO`, it is more convenient to
accept `HasIO` in `onCollect` and `onCollectAny`.
2021-07-17 14:42:34 +01:00
Niklas Larsson
f8fc131b57
Merge pull request #1734 from melted/chez_exe
Add docs for chez-exe
2021-07-17 15:33:58 +02:00
Edwin Brady
877e830133 A couple of documentation corrections
A CHANGELOG update, and a correction on data type names which has been
wrong in the crash course for some time now!
2021-07-17 14:20:32 +01:00
Alex Humphreys
f195aed2cd [ Test ] allow 'N' as an acceptable response
Situation I just ran into that I found confusing:
```
Golden value differs from actual value.
Accept actual value as new golden value? [y/N]
N
Invalid answer.
```
2021-07-17 13:29:13 +01:00
André Videla
8130b660d7
Merge pull request #1725 from andrevidela/update-proposal-template
Update issue template for proposals
2021-07-17 10:06:36 +00:00
Stiopa Koltsov
41c20ddf6a Assertions in RefC runtime
Better crash explicitly than debug memory violation.

The most important part of this is in `Buffer` implementation.
2021-07-17 03:59:32 +01:00
Niklas Larsson
d4039d962c Add docs for chez-exe 2021-07-16 22:05:28 +02:00
Zoe Stafford
0fec867583 [ fix ] Name in Language.Reflection.TT
This was different to `Name` in `Core.Name`
Specifically `CaseBlock` and `WithBlock` had an `Int` instead of a `String`
2021-07-16 20:05:49 +01:00
Mathew Polzin
2c5b9bfe85
Merge pull request #1696 from stepancheg/sig-counter
Replace per signal counter with per signal flag
2021-07-16 07:54:18 -07:00
André Videla
d1e6726f70 Update issue template for proposals 2021-07-16 12:47:57 +00:00
Edwin Brady
70b838fd07
Merge pull request #1722 from edwinb/doc-revisions
FAQ/CONTRIBUTION updates
2021-07-16 13:46:07 +01:00
Edwin Brady
c9a129bf11
Merge pull request #1723 from edwinb/throw-export
Export throw and catch again in App
2021-07-16 13:44:52 +01:00
Edwin Brady
d2af6e5027 Export throw and catch again in App
Fixes #1706
2021-07-16 11:42:24 +01:00
Stiopa Koltsov
c4ed1395d9 Replace per signal counter with per signal flag
Operating system counter stores signals as flag set without counter.
So sending two signals to a process may result to one or two signal
handler invocation. Queueing signals inside Idris could give users
false sense of signals being are queue, while they are not.

In particular, test for signal could not work reliably for that
reason.

Also, practically we usually don't need have more than once signal
event.

This is follow-up to #1660. CC @mattpolzin
2021-07-16 11:31:53 +01:00
Edwin Brady
3ee965e30d FAQ/CONTRIBUTION updates
We had a lot of things missing here, and the contributing guidelines
were extremely out of date and reflected the state when I first made the
Idris 2 repo public. I've updated both to reflect the current state of
the way we work, and to give better guidelines about what will be most
helpful.
2021-07-16 11:16:46 +01:00
Edwin Brady
1237417599
Merge pull request #1671 from stepancheg/refc-buffer
Pass Buffer as char* when using C functions in RefC
2021-07-16 10:47:48 +01:00
Edwin Brady
ba8ce048b9
Merge pull request #1689 from LibreCybernetics/gsha
Use gsha256sum when sha256sum doesn't exist [ Re: #1584 ]
2021-07-16 10:46:33 +01:00
Edwin Brady
b385e6063c
Merge pull request #1705 from CodingCellist/pragma-topic
[ doc ] Add command-line help/topic for the various pragmas.
2021-07-16 10:30:13 +01:00
Edwin Brady
66217b6fa6
Merge branch 'master' into refc-buffer 2021-07-16 09:44:40 +01:00
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