diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -6,6 +6,17 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.5.3 — 2022-07-12 + +This version contains a few minor improvements: + +1. Allow patterns in dependent function types (see [#67](https://github.com/rzk-lang/rzk/pull/67)); +2. Hint about possible shape coercions (see [#67](https://github.com/rzk-lang/rzk/pull/67)); +3. Enable doctests (see [#68](https://github.com/rzk-lang/rzk/pull/68)); +4. Improve documentation (add recommended installation instructions via VS Code) +5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983)); +6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66)); + ## v0.5.2 — 2022-07-05 This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit: @@ -20,42 +31,42 @@ This version fixes `Unit` type and makes some changes to documentation: -- Fix computation for `Unit` (see [2f7d6295]( https://github.com/rzk-lang/rzk/commit/2f7d6295 )); -- Update documentation (see [ea2d176b]( https://github.com/rzk-lang/rzk/commit/ea2d176b )); -- Use mike to deploy versioned docs (see [99cf721a]( https://github.com/rzk-lang/rzk/commit/99cf721a )); -- Replace MkDocs hook with the published plugin (see [#58]( https://github.com/rzk-lang/rzk/pull/58 )); -- Switch to Material theme for MkDocs (see [#57]( https://github.com/rzk-lang/rzk/pull/57 )); -- Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b]( https://github.com/rzk-lang/rzk/commit/8ba1c55b )); +- Fix computation for `Unit` (see [2f7d6295](https://github.com/rzk-lang/rzk/commit/2f7d6295)); +- Update documentation (see [ea2d176b](https://github.com/rzk-lang/rzk/commit/ea2d176b)); +- Use mike to deploy versioned docs (see [99cf721a](https://github.com/rzk-lang/rzk/commit/99cf721a)); +- Replace MkDocs hook with the published plugin (see [#58](https://github.com/rzk-lang/rzk/pull/58)); +- Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57)); +- Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b)); ## v0.5 — 2022-06-20 This version contains the following changes: -- `Unit` type (with `unit` value) (see [ede02611]( https://github.com/rzk-lang/rzk/commit/ede02611 ) and [bf9d6cd9]( https://github.com/rzk-lang/rzk/commit/bf9d6cd9 ); -- Add basic tokenizer support via `rzk tokenize` (see [#53]( https://github.com/rzk-lang/rzk/pull/53 )); -- Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9]( https://github.com/rzk-lang/rzk/commit/bf9d6cd9 )). +- `Unit` type (with `unit` value) (see [ede02611](https://github.com/rzk-lang/rzk/commit/ede02611) and [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9); +- Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53)); +- Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)). ## v0.4.1 — 2022-06-16 This is version contains minor changes, primarily in tools around rzk: -- Add `rzk version` command (see [f1709dc7]( https://github.com/rzk-lang/rzk/commit/f1709dc7 )); -- Add action to release binaries (see [9286afae]( https://github.com/rzk-lang/rzk/commit/9286afae )); -- Automate SVG rendering in MkDocs (see [#49]( https://github.com/rzk-lang/rzk/pull/49 )); -- Read `stdin` when no filepaths are given (see [936c15a3]( https://github.com/rzk-lang/rzk/commit/936c15a3 )); -- Add Pygments highlighting (see [01c2a017]( https://github.com/rzk-lang/rzk/commit/01c2a017 ), [cbd656cc]( https://github.com/rzk-lang/rzk/commit/cbd656cc ), [5220ddf9]( https://github.com/rzk-lang/rzk/commit/5220ddf9 ), [142ec003]( https://github.com/rzk-lang/rzk/commit/142ec003 ), [5c7425f2]( https://github.com/rzk-lang/rzk/commit/5c7425f2 )); -- Update HighlightJS config for rzk v0.4.0 (see [171ee63f]( https://github.com/rzk-lang/rzk/commit/171ee63f )); +- Add `rzk version` command (see [f1709dc7](https://github.com/rzk-lang/rzk/commit/f1709dc7)); +- Add action to release binaries (see [9286afae](https://github.com/rzk-lang/rzk/commit/9286afae)); +- Automate SVG rendering in MkDocs (see [#49](https://github.com/rzk-lang/rzk/pull/49)); +- Read `stdin` when no filepaths are given (see [936c15a3](https://github.com/rzk-lang/rzk/commit/936c15a3)); +- Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2)); +- Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f)); ## v0.4.0 — 2022-05-18 This version introduces sections and variables. The feature is similar to `Variable` command in Coq. An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental. -- Variables and sections (Coq-style) (see [#38]( https://github.com/rzk-lang/rzk/pull/38 )); +- Variables and sections (Coq-style) (see [#38](https://github.com/rzk-lang/rzk/pull/38)); Minor improvements: -- Add flake, set up nix and cabal builds, cache nix store on CI (see [#39]( https://github.com/rzk-lang/rzk/pull/39 )); -- Apply stylish-haskell (see [7d42ef62]( https://github.com/rzk-lang/rzk/commit/7d42ef62 )); +- Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39)); +- Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62)); ## v0.3.0 — 2022-04-28 @@ -90,7 +101,7 @@ The only known breaking changes are: 1. Terms like `second x y` which previous have been parsed as `second (x y)` - now are properly parsed as `(second x) y`. + now are properly parsed as `(second x) y`. 2. It is now necessary to have at least a minimal indentation in the definition of a term after a newline. 3. Unicode syntax is temporarily disabled, except for dependent sums and arrows in function types. 4. The restriction syntax `[ ... ]` now has a slightly different precedence, so some parentheses are required, e.g. in `(A -> B) [ phi |-> f]` or `(f t = g t) [ phi |-> f]`. @@ -111,33 +122,33 @@ 3. Nullary extension types are possible: `A t [ phi t |-> a t ]` 4. Lambda abstractions can introduce multiple arguments: - ```rzk - #def hom : (A : U) -> A -> A -> U - := \A x y -> - (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ] - ``` + ```rzk + #def hom : (A : U) -> A -> A -> U + := \A x y -> + (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ] + ``` 5. Parameters can be introduced simultaneously for the type and body. Moreover, multiple parameters can be introduced with the same type: - ```rzk - #def hom (A : U) (x y : A) : U - := (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ] - ``` + ```rzk + #def hom (A : U) (x y : A) : U + := (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ] + ``` 6. Restrictions can now support multiple subshapes, effectively internalising `recOR`: - ```rzk - #def hom (A : U) (x y : A) : U - := (t : Δ¹) -> A [ t === 0_2 |-> x, t === 1_2 |-> y ] - ``` + ```rzk + #def hom (A : U) (x y : A) : U + := (t : Δ¹) -> A [ t === 0_2 |-> x, t === 1_2 |-> y ] + ``` 7. There are now 3 syntactic versions of `refl` with different amount of explicit annotations: - `refl`, `refl_{x}` and `refl_{x : A}` + `refl`, `refl_{x}` and `refl_{x : A}` 8. There are now 2 syntactic versions of identity types (`=`): `x = y` and `x =_{A} y`. 9. `recOR` now supports alternative syntax with an arbitrary number of subshapes: - `recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )` + `recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )` 10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalisations, or to upcast types. @@ -150,11 +161,11 @@ 5. `#compute-nf ` — compute normal form of a term 6. `#compute ` — alias for `#compute-whnf` 7. `#set-option