@@ -15,7 +15,7 @@ Here are a few guidelines that we would like contributors to follow so that we c
1515 * [Debian](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Debian)
1616 * [Windows](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Windows)
1717
18−# Issue Reporting
18+## Issue Reporting
1919
2020Before you report an issue, or wish to add cool functionality please try and check to see if there are existing [issues](https://github.com/idris-lang/Idris-dev/issues) and [pull requests](https://github.com/idris-lang/Idris-dev/pulls).
2121We do not want you wasting your time, duplicating somebody's work!
@@ -25,6 +25,25 @@ We do not want you wasting your time, duplicating somebody's work!
2525A basic rule when contributing to Idris is the **campsite rule**: leave the codebase in better condition than you found it.
2626Please clean up any messes that you find, and don't leave behind new messes for the next contributor.
2727
28+## Contributing to the default libraries.
29+
30+`Idris` ships with a set of packages in `libs/` that is provided as a default library.
31+These packages should not be seen as the *standard* as when working with dependent types we do not necessarily know how best to work with dependent types.
32+These packages offer functionality that can be built on top of when constructing `Idris` programs.
33+
34+One major point to make is that everything in prelude will be imported automatically, unless given
35+the `--noprelude` option.
36+A central idea within the `Idris` Community is that what counts as `Idris` is: **the compiler plus the Standard Prelude**.
37+Other libraries (base, effects, etc) are still part of the distribution, but not necessarily standard.
38+
39+As `Idris` is still being developed we are open to suggestions and changes that make improvements to these default packages.
40+Major changes to the library (or `Idris` itself) should ideally be discussed first through the projects official channels of communication i.e. the mailing list, github wiki, or IRC, or as a [Dragon Egg](https://github.com/idris-lang/Idris-dev/wiki/Feature-proposals).
41+Developers then seeking to add content to `Idris`s prelude and default library, should do so through a PR where more discussion's and refinements can be made.
42+
43+We do not want you wasting your time nor duplicating somebody's work!
44+
45+Of note: developers should be prepared to wait until their PR has been discussed and authorized prior to the PRs inclusion.
46+
2847## Making Changes
2948
3049Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).
@@ -88,11 +107,11 @@ $ git diff --check
88107 line separating the summary from the body is critical (unless you omit
89108 the body entirely); tools like rebase can get confused if you run the
90109 two together.
91−
110+
92111 Further paragraphs come after blank lines.
93−
112+
94113 - Bullet points are okay, too
95−
114+
96115 - Typically a hyphen or asterisk is used for the bullet, preceded by a
97116 single space, with blank lines in between, but conventions vary here
98117
@@ -137,5 +156,3 @@ To help increase the chance of your pull request being accepted:
137156
138157
139158Adapted from the most excellent contributing files from the [Puppet project](https://github.com/puppetlabs/puppet) and [Factroy Girl Rails](https://github.com/thoughtbot/factory_girl_rails/blob/master/CONTRIBUTING.md)
140−
141−