135 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Edwin Brady	941c8b1ab5	Point bootstrap tests at the right place ... We also need to separate building the runtests binary from running the tests, because runtests refers to the boostrap libraries, and the tests refer to the newly built libraries. This worked locally, using inconsistent TTC versions for the bootstrap version and new version, but let's see what it does on a clean machine	2020-05-21 17:11:12 +01:00
Edwin Brady	4ed38bd47d	Try to fix bootstrap script ... I think the tests are using the libraries from the bootstrap Idris 2, not the just built Idris 2, so if the ttc formats aren't idential the tests won't work. Let's see if that theory is correct...	2020-05-21 16:32:10 +01:00
Edwin Brady	bd093e9cba	Propagate totality options on methods ... As in Idris 1 - if an interface declares a method as total or covering, then all implementations have to satisfy that. Temporarily turn off %default directive again, at least until totality checking works as it should (this is probably better than removing it from various places because I'll forget to put them back)	2020-05-21 16:04:22 +01:00
Edwin Brady	0f724fbc7f	Report errors on totality check failure ... This means temporarily removing some '%default total' from the libraries and tests, since the input for codata checking isn't right yet (it needs appropriate use of inlining)	2020-05-21 13:08:19 +01:00
Edwin Brady	8291c8bbeb	Add runtime error for unhandled cases ... Should have done this ages ago, it was much easier than I expected... this adds an explicit error clause before running the pattern match compiler for runtime case trees, but only if the coverage checker finds there are missing cases.	2020-05-21 10:54:22 +01:00
Edwin Brady	5b4e1492a8	Merge pull request #91 from ska80/patch-1 ... Correct ‘Installation problem’ issue template	2020-05-21 10:07:13 +01:00
Marek L	1a998d8944	Fix typo seperate -> separate in System/Path.idr ... https://www.grammarly.com/blog/separate-seperate/	2020-05-21 09:28:11 +01:00
Kamiλ Shakirov	2c85940031	Correct ‘Installation problem’ issue template	2020-05-21 09:33:47 +06:00
Edwin Brady	b2e7c40da9	Remove duplicate template	2020-05-20 22:04:22 +01:00
Edwin Brady	f819c0b855	Update installation-problem.md	2020-05-20 22:03:14 +01:00
Edwin Brady	987b2b0a77	Update feature-requests-and-proposals.md	2020-05-20 21:59:14 +01:00
Edwin Brady	918bf58763	Copy issue templates from Idris2-boot	2020-05-20 21:51:58 +01:00
Edwin Brady	c98d8a3e55	Merge pull request #88 from ohad/network-ffi ... libs/network: Port FFI calls from deprecated interface to `%foreign` pragma	2020-05-20 21:44:03 +01:00
Edwin Brady	bf5bfba712	Merge pull request #87 from ska80/prefix-update ... Remove stale src/IdrisPath.idr on each 'make clean' run	2020-05-20 21:42:45 +01:00
Edwin Brady	215ad99308	Merge pull request #86 from andylokandy/just ... Add a total version of the fromMaybe	2020-05-20 21:41:35 +01:00
Edwin Brady	2decd88152	Merge pull request #85 from andylokandy/fold ... Add List folds without default value	2020-05-20 21:39:45 +01:00
Edwin Brady	dd28e53c5f	Merge pull request #84 from LibreCybernetics/split-parser-support ... Split Parser.Support	2020-05-20 21:38:23 +01:00
Fabián Heredia Montiel	6a5d6647c1	Split Parser.Support	2020-05-20 15:00:42 -05:00
Ohad Kammar	1945619db7	libs/network: Port FFI calls from deprecated interface to %foreign pragma	2020-05-20 20:09:56 +01:00
Kamil Shakirov	ebb98700bf	Remove stale src/IdrisPath.idr on each 'make clean' run ... ${PREFIX} can now be properly changed on each rebuild	2020-05-21 00:38:43 +06:00
andylokandy	a51a665668	Reuse foldr1 in foldr1'	2020-05-21 02:35:18 +08:00
andylokandy	5252a7ae3b	Add a total version of the fromMaybe	2020-05-21 02:11:35 +08:00
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