idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 21:23:53 +03:00
Code Issues Projects Releases Wiki Activity
3,063 Commits 6 Branches 9 Tags 115 MiB
3c0eadee07
Commit Graph

3063 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
e292f18029 Update installing instructions in docs 2020-05-20 19:09:26 +01:00
andylokandy
8de668f1a4 Add folds without default value to List 2020-05-21 02:09:14 +08:00
Edwin Brady
1fb8904992 Fix latex rtd generation 
@jfdm tells me that you can only generate one latex document, so let's
make it the tutorial
 2020-05-20 18:53:56 +01:00
Edwin Brady
3a915943fc Add icons 2020-05-20 18:48:55 +01:00
Edwin Brady
940570e083 Remove the :force: that RTD complains about 
This isn't the right solution since it removes the highlighting but
maybe it makes the build work again (it does for me locally)
 2020-05-20 18:46:09 +01:00
Edwin Brady
0563f7dcec Gambit fix from Idris2-boot 
Importing @andylokandy's fix from Idris2-boot
 2020-05-20 18:25:10 +01:00
Edwin Brady
9baa5385d4 Drop testing step from racket bootstrap step 
I'll put it back when the tests actually pass on racket. Also when
making the test.ipkg pays attention to the CG setting in the makefile so
it doesn't try to build via Chez.
 2020-05-20 18:10:11 +01:00
Edwin Brady
ac859a9c50 Move bootstrap racket to the right place 2020-05-20 16:55:20 +01:00
Edwin Brady
0cd484fa09 Add idris2api.ipkg 
This is a small variation that installs all the modules as a library,
which could be used by external tools, eg fancy REPLs, code generators,
etcs.
 2020-05-20 16:38:46 +01:00
Edwin Brady
d6cdef99e1
Merge pull request #81 from jfdm/patch-3 
Update README.md
 2020-05-20 16:15:16 +01:00
Edwin Brady
0dec90b23f
Merge pull request #82 from andylokandy/path 
Add System.Path
 2020-05-20 16:14:39 +01:00
andylokandy
0d82b5d7da Add System.Path 2020-05-20 22:51:01 +08:00
Edwin Brady
de8acf781b Add a .gitattributes 
Amusing as it is to display as being implemented in Scheme, it's
probably best to ignore the bootstrap files!
 2020-05-20 15:37:28 +01:00
Jan de Muijnck-Hughes
120aa69eb1
Update README.md 2020-05-20 15:19:27 +01:00
Jan de Muijnck-Hughes
f595ce3ef1 Update INSTALL.md 2020-05-20 15:01:19 +01:00
Jan de Muijnck-Hughes
07b1ba47d2 Update README.md 2020-05-20 14:55:40 +01:00
Edwin Brady
4aabc06b31 Fix bootstrap script (again) 
I'm doing this in too much of a hurry... but it definitely works for me
locally now!
 2020-05-20 14:33:34 +01:00
Edwin Brady
43ef716fa8 Update idris2-boot 2020-05-20 14:27:26 +01:00
Edwin Brady
b94ff558f3 Put idris2.ss back in the right place 2020-05-20 14:23:26 +01:00
Edwin Brady
451ed0f213 Update Makefile 
Remove all idris2sh so that travis and the bootstrap scripts look in the
right place
 2020-05-20 14:19:06 +01:00
Edwin Brady
32263883ee Update bootstrapping scripts for new exec name 
(Also, hopefully, this will poke travis to build the repo in its new
location!)
 2020-05-20 14:00:15 +01:00
Edwin Brady
9cc4cba065 Change executable name 
I think we can be the official Idris2 now
 2020-05-20 13:31:04 +01:00
Edwin Brady
8c4727d308
Merge pull request #12 from ska80/silence-package-clean 
Silence 'idris2 --clean idris2.ipkg' errors
 2020-05-20 13:25:49 +01:00
Edwin Brady
34c542d29e
Merge pull request #11 from ska80/ignore-bootstrap 
Ignore Racket's build artifacts in 'bootstrap' directory
 2020-05-20 13:25:37 +01:00
Edwin Brady
913de4cbaf
Merge pull request #6 from LibreCybernetics/refactor-mapError 
Create new mapError utility function and refactor some parser code
 2020-05-20 12:55:33 +01:00
Kamil Shakirov
3491f4965e Silence 'idris2 --clean idris2.ipkg' errors 
Silence annoying errors like 'No such file or directory' if there are no files/directoris to delete
 2020-05-20 16:59:49 +06:00
Kamil Shakirov
5560b75158 Ignore Racket's build artifacts in 'bootstrap' directory 2020-05-20 16:57:49 +06:00
Edwin Brady
14b3919809
Merge pull request #9 from zenntenn/Update_gitignore 
Ignoring autogenerated bootstrap/test files
 2020-05-20 11:49:28 +01:00
Edwin Brady
08c8ec448a
Merge pull request #8 from LibreCybernetics/refactor-utils-string-sh 
Refactor Utils.String.stripQuotes to avoid double reversion on Strings
 2020-05-20 11:48:41 +01:00
Edwin Brady
4d7f122375
Merge pull request #7 from chrrasmussen/fix-chez016 
Fix chez016 test
 2020-05-20 11:48:06 +01:00
Edwin Brady
94b83c22c6
Merge pull request #10 from ska80/misc-fixes 
More fixes and improvements
 2020-05-20 11:47:25 +01:00
Edwin Brady
ae7bdaa7d3
Merge branch 'master' into misc-fixes 2020-05-20 11:46:28 +01:00
Edwin Brady
99e0976b75 Some updates in INSTALL.md 
Hopefully clearer now.
 2020-05-20 11:40:27 +01:00
Edwin Brady
c911c60e77 Fix link to Travis 2020-05-20 11:33:07 +01:00
Edwin Brady
fd2ebd52c3 Add licence and changelog and update REAMDE 2020-05-20 11:31:48 +01:00
Kamil Shakirov
d47202318a Ignore 'docs/build' 2020-05-20 16:28:18 +06:00
Kamil Shakirov
f6e04b99ad Merge branch 'master' into misc-fixes 2020-05-20 16:27:55 +06:00
Edwin Brady
fd55e629ee Copy more files over from Idris2 2020-05-20 11:23:04 +01:00
Edwin Brady
d3fab2d28f Fix typo in bootstrap script 2020-05-20 11:12:54 +01:00
Edwin Brady
8fbce0cdc1 Also need to pass through data directory 2020-05-20 11:02:49 +01:00
Kamil Shakirov
ffc1b490bd Merge branch 'master' into misc-fixes 2020-05-20 16:00:43 +06:00
Edwin Brady
87f0c1c6be Bootstrap script needs to know library path 
This is for locating the libraries for copying to the chez executable.
If they're not installed yet, it'll look in the wrong place.
 2020-05-20 10:52:18 +01:00
Edwin Brady
b39df83002 Maybe the tests need the library path... 
It's surprising because the chez startup script should set it, but let's
see what happens anyway.
 2020-05-20 10:48:29 +01:00
Kamil Shakirov
38b4fe6aca Merge branch 'master' into misc-fixes 2020-05-20 15:45:55 +06:00
Edwin Brady
65f7fb6ab8 Minor edit to bootstrap script 
It's better if the tests aren't interactive, since they're intended for
running on CI as well as to give an idea of whether building was
successful, rather than to give an idea of what has gone wrong.
 2020-05-20 10:38:56 +01:00
Edwin Brady
77c218435b Reorganise some bootstrap/travis steps 2020-05-20 10:33:40 +01:00
Kamil Shakirov
880981d5b4 More fixes and improvements 
* Ignore build artifacts in 'tests' directory
* Remove unused variables in makefiles
* Add 'bootstrap-clean' rule to delete build artifacts from 'bootstrap' directory
* Add 'distclean' rule to delete all build artifacts from the source tree
 2020-05-20 15:31:30 +06:00
Edwin Brady
6437d8070b Need a sudo 2020-05-20 10:24:55 +01:00
Edwin Brady
f61f0a5c40 Fix typo in error 
(Okay, this is just to see if travis does something...)
 2020-05-20 10:23:22 +01:00
Edwin Brady
ca3d519291 Experiment with setting up Travis 
I have no idea what I'm doing
 2020-05-20 10:21:35 +01:00