git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3180 from jfdm/better-pkg-names
bc5d9d4Jan de Muijnck-Hughes
CHANGELOG.md+10−4
compare with master
unifiedsplit
@@ -16,14 +16,14 @@
16 ```
16 ```
17 [PlusNatSemi] Semigroup Nat where
17 [PlusNatSemi] Semigroup Nat where
18 (<+>) x y = x + y
18 (<+>) x y = x + y
19−
19+
20 [MultNatSemi] Semigroup Nat where
20 [MultNatSemi] Semigroup Nat where
21 (<+>) x y = x * y
21 (<+>) x y = x * y
22−
22+
23 -- use PlusNatSemi as the parent implementation
23 -- use PlusNatSemi as the parent implementation
24 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
24 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
25 neutral = 0
25 neutral = 0
26−
26+
27 -- use MultNatSemi as the parent implementation
27 -- use MultNatSemi as the parent implementation
28 [MultNatMonoid] Monoid Nat using MultNatSemi where
28 [MultNatMonoid] Monoid Nat using MultNatSemi where
29 neutral = 1
29 neutral = 1
@@ -107,6 +107,12 @@
107 not, leading to a contradiction. The new fine-grained equality
107 not, leading to a contradiction. The new fine-grained equality
108 prevents this.
108 prevents this.
109
109
110+* Naming conventions for Idris packages in an iPKG file now follow the
111+ same rules for executables. Unquoted names must be valid namespaced
112+ Idris identifiers e.g. ``package my.first.package``. Quoted package
113+ names allow for packages to be given valid file names, for example,
114+ ``package "my-first-package"``.
115+
110## Reflection changes
116## Reflection changes
111
117
112* The implicit coercion from String to TTName was removed.
118* The implicit coercion from String to TTName was removed.
@@ -278,7 +284,7 @@
278 package names that the idris project depends on. This reduces bloat in the
284 package names that the idris project depends on. This reduces bloat in the
279 `opts` option with multiple package declarations.
285 `opts` option with multiple package declarations.
280* iPKG files now allow `executable = "your filename here"` in addition to the
286* iPKG files now allow `executable = "your filename here"` in addition to the
281− existing `executable = yourFilenameHere` style. While the unquoted version is
287+ Existing `Executable = yourFilenameHere` style. While the unquoted version is
282 limited to filenames that look like namespaced Idris identifiers
288 limited to filenames that look like namespaced Idris identifiers
283 (`your.filename.here`), the quoted version accepts any valid filename.
289 (`your.filename.here`), the quoted version accepts any valid filename.
284* Add definition command (`\d` in Vim, `Ctrl-Alt-A` in Atom, `C-c C-s` in Emacs)
290* Add definition command (`\d` in Vim, `Ctrl-Alt-A` in Atom, `C-c C-s` in Emacs)
docs/reference/packages.rst+2−1
@@ -15,7 +15,8 @@ Package Descriptions
15A package description includes the following:
15A package description includes the following:
16
16
17+ A header, consisting of the keyword package followed by the package
17+ A header, consisting of the keyword package followed by the package
18− name. Package names can be any valid Idris identifier.
18+ name. Package names can be any valid Idris identifier. The iPKG
19+ format also takes a quoted version that accepts any valid filename.
19+ Fields describing package contents, ``<field> = <value>``
20+ Fields describing package contents, ``<field> = <value>``
20
21
21At least one field must be the modules field, where the value is a
22At least one field must be the modules field, where the value is a
docs/tutorial/packages.rst+3−2
@@ -4,7 +4,7 @@ Packages
4
4
5
5
6Idris includes a simple build system for building packages and executables from a named package description file.
6Idris includes a simple build system for building packages and executables from a named package description file.
7−These files can be used with the Idris compiler to manage the development process.
7+These files can be used with the Idris compiler to manage the development process .
8
8
9Package Descriptions
9Package Descriptions
10====================
10====================
@@ -12,7 +12,8 @@ Package Descriptions
12A package description includes the following:
12A package description includes the following:
13
13
14+ A header, consisting of the keyword package followed by the package
14+ A header, consisting of the keyword package followed by the package
15− name. Package names can be any valid Idris identifier.
15+ name. Package names can be any valid Idris identifier. The iPKG
16+ format also takes a quoted version that accepts any valid filename.
16+ Fields describing package contents, ``<field> = <value>``
17+ Fields describing package contents, ``<field> = <value>``
17
18
18At least one field must be the modules field, where the value is a
19At least one field must be the modules field, where the value is a
idris.cabal+1−1
@@ -671,7 +671,7 @@ Extra-source-files:
671 test/primitives006/expected
671 test/primitives006/expected
672
672
673 test/pkg001/run
673 test/pkg001/run
674− test/pkg001/test.ipkg
674+ test/pkg001/test-pkg.ipkg
675 test/pkg001/*.idr
675 test/pkg001/*.idr
676 test/pkg001/expected
676 test/pkg001/expected
677
677
src/Pkg/PParser.hs+2−1
@@ -56,7 +56,8 @@ parseDesc fp = do
56
56
57pPkg :: PParser PkgDesc
57pPkg :: PParser PkgDesc
58pPkg = do
58pPkg = do
59− reserved "package"; p <- fst <$> identifier
59+ reserved "package"
60+ p <- filename
60 st <- get
61 st <- get
61 put (st { pkgname = p })
62 put (st { pkgname = p })
62 some pClause
63 some pClause
test/pkg001/run+3−3
@@ -1,5 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --build test.ipkg
2+${IDRIS:-idris} $@ --build test-pkg.ipkg
3rm -f *.ibc
3rm -f *.ibc
4−${IDRIS:-idris} $@ --build test.ipkg --quiet
4+${IDRIS:-idris} $@ --build test-pkg.ipkg --quiet
5−${IDRIS:-idris} $@ --build test.ipkg --logging-categories "elab" --log 1
5+${IDRIS:-idris} $@ --build test-pkg.ipkg --logging-categories "elab" --log 1
test/pkg001/test.ipkg → test/pkg001/test-pkg.ipkgrenamed+1−1
@@ -1,4 +1,4 @@
1−package test
1+package "test-pkg"
2
2
3pkgs = effects
3pkgs = effects
4
4