Add docs about Versioning and Release process (#195)

We add:
- a `VERSIONING.md` file, that documents what we consider a release,
   how and when and what we release
- a `CHANGELOG.md` file, that will keep and classify all the changes between versions
- a `release_template.md`, to serve as a checklist when making new releases

.github/CONTRIBUTING.md

@@ -105,6 +105,18 @@ always roll them back with a new proposal.
 If the change is approved quickly, there is still a minimum 3-day waiting
 period before merging for changes to the standard.
 
+### Soundness of proposed changes
+
+For non-trivial changes there should be a proof-of-concept implementation as a
+sanity check. Moreover, changes to the type system need to have an informal proof
+sketch of the following four soundness rules:
+
+- Type-inference won't diverge
+- If an expression type-checks, normalizing that expression won't diverge
+- Normalizing an inferred type won't diverge
+- Normalizing an expression doesn't change its type
+
+
 ## How do I get the "commit bit"?
 
 Just ask!  I (@Gabriel439) hand out the commit bit freely to anybody who

.github/PULL_REQUEST_TEMPLATE/release_template.md

@@ -0,0 +1,14 @@
+# Release checklist
+
+- [ ] compute the new version number by following the [versioning scheme][versioning-scheme]
+- [ ] update `README.md` with the new version number ([here][readme-version-number]).
+- [ ] update `CHANGELOG.md` with all the changes since the last version.  
+      **N.B.**: this includes also unreleased changes in the `Prelude`.  
+      The changes in each version should be classified in three sections
+      (Note: the subdivision reflects the [versioning scheme numbers][versioning-scheme]):
+  - `Breaking changes`
+  - `New features`
+  - `Other changes`
+
+[readme-version-number]: https://github.com/dhall-lang/dhall-lang#development-status
+[versioning-scheme]: https://github.com/dhall-lang/dhall-lang/blob/master/VERSIONING.md#versioning-scheme

CHANGELOG.md

@@ -0,0 +1,16 @@
+# Changelog
+
+All notable changes to the Dhall language standard will be documented in this file.
+
+For more info about our versioning policy, see [VERSIONING.md](VERSIONING.md).
+
+## `v1.0.0`
+
+Here we start versioning the language standard on its own.
+
+Previously it was versioned together with the [reference implementation][dhall-haskell],
+so see [here][dhall-haskell-changelog] for information on previous breaking changes
+to the language.
+
+[dhall-haskell]: https://github.com/dhall-lang/dhall-haskell/
+[dhall-haskell-changelog]: https://github.com/dhall-lang/dhall-haskell/blob/master/CHANGELOG.md

README.md

@@ -15,6 +15,7 @@ You can think of Dhall as: JSON + functions + types + imports
 * [Features](#features)
 * [Documentation](#documentation)
 * [Standard Library](#standard-library)
+* [Development Status](#development-status)
 * [Overview](#overview)
     * [Interpreter](#interpreter)
     * [Language Bindings](#language-bindings)
@@ -25,7 +26,6 @@ You can think of Dhall as: JSON + functions + types + imports
         * [Bash](#bash)
         * [Text](#text)
 * [Design Philosophy](#design-philosophy)
-* [Development Status](#development-status)
 * [Name](#name)
 
 ## Getting started
@@ -948,6 +948,19 @@ work with the builtin types. Where to find it:
 * [Mirror on IPFS](http://prelude.dhall-lang.org/)
 * [Nix](https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/interpreters/dhall/default.nix): both `dhall` and `dhall.prelude` derivations are built, install the `Prelude` with e.g. `nix-env -iA nixpkgs.dhall.prelude`
 
+## Development status
+
+Language version: `v1.0.0`.
+
+The versioning policy is detailed in the [Versioning document](VERSIONING.md),
+and you can see the latest changes [here in the Changelog](CHANGELOG.md).
+
+There is an effort under way to formalize the language semantics for Dhall, to
+help with porting it to [other languages](#language-bindings).  
+If you would like to assist with either standardizing the language or creating
+new bindings just open a new issue or contribute to existing ones in the [issue
+tracker][issue-tracker].
+
 ## Overview
 
 You can use Dhall in one of three ways:
@@ -1430,13 +1443,6 @@ currently only Haskell bindings.  If you would like to contribute bindings to
 another language then go for it, otherwise I will do my best to contribute them
 as time permits.
 
-## Development status
-
-I am beginning to author a formal language standard for Dhall to help with
-porting Dhall to other languages.  If you would like to assist with either
-standardizing the language or creating new bindings just let me know through the
-issue tracker.
-
 ## Name
 
 The language is named after a
@@ -1469,3 +1475,4 @@ The name rhymes with "tall"/"call"/"hall" (i.e. "dɔl" for a US speaker or
 [hcl]: https://github.com/hashicorp/hcl
 [readme-before-nat-int-swap]: https://github.com/dhall-lang/dhall-lang/blob/1b74481c87b3ed83ecd613420c11de92335652a3/README.md
 [migration-nat-int-swap]: https://github.com/dhall-lang/dhall-lang/wiki/Migration%3A-Swapped-syntax-for-Natural-numbers-and-Integers
+[issue-tracker]: https://github.com/dhall-lang/dhall-lang/issues

VERSIONING.md

@@ -0,0 +1,62 @@
+# Versioning Dhall
+
+This document describes how the Dhall language standard is versioned,
+and how new versions are released.
+
+## What is a "version"
+
+A version of the Dhall language standard consists of a *git tag*
+(i.e. what GitHub calls a "release").
+
+## How are releases made
+
+1. Compute the new version number by following the [versioning scheme](#versioning-scheme)
+2. Open a Pull Request with the "release template" to get a checklist:
+   you do it by appending `?template=release_template.md` to your PR url.
+3. The PR will sit there for the minimum review period of 3 days (no exceptions).  
+   This is to give time to merge the last things to `master` before cutting the new release.
+4. Once that is merged, create a git tag/GitHub release with the new version number
+5. Repeat the above step for the [Prelude repo](https://github.com/dhall-lang/Prelude) as well.  
+   Note: the tagged version should be the same as the new version of the language standard.
+
+## When are releases made
+
+Anybody can cut a release if there is:
+1. an unreleased change *at least 1 month old*, and
+2. no unreleased changes *less than 3 days old*.
+
+The goal is to encourage releasing early and often and to give anybody permission
+to cut a release.  
+This includes people without the ["commit bit"](https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-i-get-the-commit-bit)):
+they should be able to request that somebody cut a release on their behalf.
+
+This implies that the `master` branch of the specification should always be "release-ready".
+
+## Versioning scheme
+
+The specification for the language standard is versioned in the form `vX.Y.Z`,
+where `X`, `Y` and `Z` are Natural numbers.
+
+When introducing changes in a new release, the version should change in the following way:
+- **A change to `X`** reflects a *backwards-incompatible* change to the specification
+  - This means that Dhall code compatible with the previous version might not be
+    compatible with the new one.  
+    This is the only change that **needs action** from the user
+    (to update the existing code to the new version).
+- **A change to `Y`** reflects a *new language feature*
+  - This means that any Dhall code that depends the new language feature will not
+    be compatible with the older specifications (so you wouldn't be able to
+    "downgrade" your interpreter).
+- **A change to `Z`** is basically *semantics-preserving refactors* of the specification
+  - i.e. documentation/whitespace changes or renaming terminals in the grammar, etc.
+  - This means that some existing Dhall code compatible with the previous standard
+    will have the same semantics with the new standard, and viceversa.
+
+## What is a "backwards-incompatible" change? (aka "breaking")
+
+The contract for a "non-breaking" change is that any code that
+parsed/resolved/type-checked/normalized successfully before must continue to do so
+(modulo imported resources changing - that is, if the imports are protected by
+their semantic hash they should not break as well).
+
+Carefully note that this does not include pretty-printing or formatting the code.