idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 16:51:51 +03:00
Code Issues Projects Releases Wiki Activity
322 Commits 6 Branches 9 Tags 114 MiB
932ea60dbc
Commit Graph

322 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Sventimir
932ea60dbc Port Data.Fin.Extra module from Idris1. 2020-06-01 13:29:59 +02:00
Edwin Brady
1d078f7888
Merge pull request #177 from edwinb/fix-imports 
Fix import loading
 2020-05-27 16:37:57 +01:00
Edwin Brady
c88bf7af8d Fix import loading 
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)

This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
  Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
  things were being imported that shouldn't have been. The new way is
  correct!

An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
 2020-05-27 15:49:03 +01:00
Jan de Muijnck-Hughes
8b062f47cc Allow cli given option overriding for ipkg cmds. 
As it was in Idris1 being able to override some, or introduce new, options to an Idris IPKG is beneficial. For example, generate code for multiple codegens from a single source.

Overridable options are:

+ `--quiet`
+ `--verbose`
+ `--timing`
+ `--dumpcases <file>`
+ `--dumplifted <file>`
+ `--dumpvmcode <file>`
+ `--debug-elab-check`
 2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
54fd78a956 Fixed fragility of ipkg file parsing. 
+ Explicitly check if an IPKG has the correct suffix.
+ Add missing case that could return a malformed error message.
 2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
1948bfcfc6 Added 'REPL' as a command line option so the code can be used. 2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
68a4ad2e1c New test for detecting overridable options for IPKG commands. 2020-05-26 14:41:09 +01:00
Niklas Larsson
c23958bf16
Merge pull request #167 from ska80/sync-idris2api 
Sync idris2api.ipkg with idris2.ipkg
 2020-05-26 13:58:24 +02:00
asdfjasdf
6d36b04c72 Possible copy-paste mistake in typesfuns.rst 
In the intial code listing we currently have "x = 42" but in following listing "x == 9 * 9 + 13" returns true.
 2020-05-26 10:21:58 +01:00
Kamil Shakirov
d5743911fe Sync idris2api.ipkg with idris2.ipkg 2020-05-26 12:24:42 +06:00
Niklas Larsson
59800e1f47
Merge pull request #142 from jinwoo/foldl 
[prelude] Use `foldl` for sum and product
 2020-05-25 21:05:56 +02:00
Niklas Larsson
df3d4eb1fa
Merge pull request #159 from melted/ci_self_host 
Run the self-hosting step in CI
 2020-05-25 19:14:30 +02:00
Jinwoo Lee
4a52a84113 update golden files 2020-05-25 10:06:52 -07:00
Jinwoo Lee
893fbb78c9 Provide sum' and product' separate from sum and product 
Not to break backwards compatibility.
 2020-05-25 09:59:18 -07:00
Jinwoo Lee
728149f2d1 [prelude] Use foldl for sum and product 
To make them tail recursive. Fixes #132.
 2020-05-25 09:59:18 -07:00
Niklas Larsson
b2ce91fec4 Run the self-hosting step in CI 
The latest Github Actions windows image contains msys2 so use that.
Also use gcc that comes with the image to save downloading clang.

Skip Racket as it's slow enough already.
 2020-05-25 18:29:59 +02:00
Edwin Brady
1212e56903
Merge pull request #160 from edwinb/fix-test 
Fix build
 2020-05-25 17:04:08 +01:00
Edwin Brady
81e9214c6f Fix build 
Showing a hole should show normalised types for the locals
 2020-05-25 16:45:33 +01:00
Edwin Brady
f38dab7c96
Merge pull request #147 from LibreCybernetics/refactor-substr 
Use library version of substr
 2020-05-25 15:44:13 +01:00
Edwin Brady
bbd3986cfc
Merge pull request #153 from ohad/ide-protocol-holes 
Ide protocol holes
 2020-05-25 15:43:52 +01:00
Edwin Brady
6a1fe4d9a4
Merge pull request #158 from edwinb/scheme-boot 
Update Scheme bootstrap files
 2020-05-25 14:41:47 +01:00
Edwin Brady
4321e9ba0d
Merge pull request #157 from keram/typo 
Fix typos in documentation and comments
 2020-05-25 14:41:31 +01:00
Marek Labos
f691469aa9 Reword a sentence in multiplicities.rst to improve readability. 2020-05-25 14:34:04 +01:00
Edwin Brady
de7dff19b0 Update Scheme bootstrap files 
Ready for a 0.2.0 release
 2020-05-25 14:21:53 +01:00
Edwin Brady
697a71aef1
Merge pull request #156 from edwinb/chez-message 
Add a specific error message to bootstrap.sh
 2020-05-25 14:12:54 +01:00
Marek Labos
9160d2772a Fix typo in backends/index.rst and racket/support.rkt 2020-05-25 14:02:49 +01:00
Marek Labos
fc08b361f3 Fix typo in multiplicities.rst 2020-05-25 13:58:45 +01:00
Edwin Brady
c0d5ff8972 Add a specific error message to bootstrap.sh 2020-05-25 13:47:44 +01:00
Edwin Brady
a95b607d78
Merge pull request #149 from wchresta/master 
Split bootstrap into separate build and test stage
 2020-05-25 13:45:41 +01:00
Edwin Brady
cfd807bba0
Merge pull request #155 from edwinb/nameless-pi 
Allow _ in pi binders
 2020-05-25 13:40:10 +01:00
Edwin Brady
3120fcb84a Allow _ for names in pi binders 
This is mostly to make it easier to write linear function types without
having to invent names for everything, which might be noisy. Also it
improves the display of linear function types when the name isn't used
in the scope.
 2020-05-25 13:14:51 +01:00
Edwin Brady
b59c336330 Merge remote-tracking branch 'upstream/master' 2020-05-25 11:57:24 +01:00
Edwin Brady
087cb84dda
Merge pull request #130 from clayrat/list-quantifiers 
add Data.List.Quantifiers
 2020-05-25 11:57:08 +01:00
Ohad Kammar
f4797be529 Merge branch 'master' of github.com:idris-lang/Idris2 into ide-protocol-holes 2020-05-25 11:51:39 +01:00
Ohad Kammar
fe1d5ee381 Transmit hole information in the IDEMode protocol 
Move printing routines into the `Idris.IDEMode.Holes` module
 2020-05-25 11:51:16 +01:00
Edwin Brady
d8f8718424
Merge pull request #151 from edwinb/appdocs 
Some documentation updates
 2020-05-25 11:50:02 +01:00
Ohad Kammar
92eaa247a6 Refactor FoundHoles : REPLResult to carry more structured information about holes 2020-05-25 10:38:22 +01:00
Fabián Heredia Montiel
1fbce6a593 Add emacs/vim swap files to gitignore 2020-05-25 09:18:49 +01:00
Edwin Brady
3859f60d7a Merge remote-tracking branch 'upstream/master' 2020-05-25 09:11:54 +01:00
Edwin Brady
227bd3b457
Merge pull request #119 from idris-lang/idemode 
[ refactor ] Idris.IDEMode.CaseSplit
 2020-05-25 09:09:37 +01:00
Edwin Brady
2206692533 Some documentation updates 
Remove things from CONTRIBUTING that are done, and initial App
documentation (though it could use more examples).
 2020-05-25 09:03:08 +01:00
Edwin Brady
c86848eaa3
Merge pull request #150 from edwinb/master 
Remove unreachable case
 2020-05-25 08:56:39 +01:00
Edwin Brady
f841f4a48a Remove unreachable case 2020-05-25 07:44:52 +01:00
Ohad Kammar
2e17a89ef0 minor bugfix: confused two branches of if 2020-05-25 07:38:31 +01:00
Ohad Kammar
0de2f6dea8 Merge branch 'master' of github.com:idris-lang/Idris2 into ide-protocol-holes 2020-05-25 07:14:33 +01:00
Ohad Kammar
ced6134f79 Refactor hole information extracting functions into a new submodule 
Introduce a new data structure for IDE-related hole data

Separate hole printing from informationextraction
 2020-05-25 07:13:12 +01:00
wchresta
788e6943a4 Split bootstrap into separate build and test stage 
* Refactor bootstrap and bootstrap-rkt scripts
* Move the execution of the test phase after bootstrapping from bootstrap
  scripts into the Makefile. This allows separate execution of build
  and test seperately.
* Solves #125
 2020-05-25 00:59:12 -04:00
Alex Gryzlov
eb04046b43 inline removed anyElim, refactor more 2020-05-25 03:53:29 +02:00
Fabián Heredia Montiel
4f040f2bbe Use library version of substr added on commit dec7dff622 2020-05-24 19:45:12 -05:00
Alex Gryzlov
5757c5e5cb remove anyElim 2020-05-25 02:27:19 +02:00