git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3092 from jfdm/installable-manpages
1599242Jan de Muijnck-Hughes
CHANGELOG.md+5−3
compare with master
unifiedsplit
@@ -5,7 +5,7 @@
5* `rewrite` can now be used to rewrite equalities on functions over
5* `rewrite` can now be used to rewrite equalities on functions over
6 dependent types
6 dependent types
7* `rewrite` can now be given an optional rewriting lemma, with the syntax
7* `rewrite` can now be given an optional rewriting lemma, with the syntax
8− `rewrite [rule] using [rewrite_lemma] in [scope]`.
8+ `rewrite [rule] using [rewrite_lemma] in [scope]`.
9* Experimental extended `with` syntax, which allows calling functions defined
9* Experimental extended `with` syntax, which allows calling functions defined
10 in a with block directly. For example:
10 in a with block directly. For example:
11
11
@@ -13,9 +13,9 @@
13 data SnocList : List a -> Type where
13 data SnocList : List a -> Type where
14 Empty : SnocList []
14 Empty : SnocList []
15 Snoc : SnocList xs -> SnocList (xs ++ [x])
15 Snoc : SnocList xs -> SnocList (xs ++ [x])
16−
16+
17 snocList : (xs : List a) -> SnocList a
17 snocList : (xs : List a) -> SnocList a
18−
18+
19 my_reverse : List a -> List a
19 my_reverse : List a -> List a
20 my_reverse xs with (snocList xs)
20 my_reverse xs with (snocList xs)
21 my_reverse [] | Empty = []
21 my_reverse [] | Empty = []
@@ -28,6 +28,8 @@
28
28
29## Miscellaneous updates
29## Miscellaneous updates
30
30
31+* The Idris man page is now installed as part of the cabal/stack build process.
32+
31* Improved startup performance by reducing the processing of an already imported
33* Improved startup performance by reducing the processing of an already imported
32 module that has changed accessibility.
34 module that has changed accessibility.
33
35
Setup.hs+9−2
@@ -9,7 +9,7 @@ import Distribution.Simple.InstallDirs as I
9import Distribution.Simple.LocalBuildInfo as L
9import Distribution.Simple.LocalBuildInfo as L
10import qualified Distribution.Simple.Setup as S
10import qualified Distribution.Simple.Setup as S
11import qualified Distribution.Simple.Program as P
11import qualified Distribution.Simple.Program as P
12−import Distribution.Simple.Utils (createDirectoryIfMissingVerbose, rewriteFile)
12+import Distribution.Simple.Utils (createDirectoryIfMissingVerbose, rewriteFile, notice, installOrdinaryFiles)
13import Distribution.Compiler
13import Distribution.Compiler
14import Distribution.PackageDescription
14import Distribution.PackageDescription
15import Distribution.Text
15import Distribution.Text
@@ -228,7 +228,7 @@ idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do
228 where
228 where
229 makeBuild dir = make verbosity [ "-C", dir, "build" , "IDRIS=" ++ idrisCmd local]
229 makeBuild dir = make verbosity [ "-C", dir, "build" , "IDRIS=" ++ idrisCmd local]
230
230
231− buildRTS = make verbosity (["-C", "rts", "build"] ++
231+ buildRTS = make verbosity (["-C", "rts", "build"] ++
232 gmpflag (usesGMP (configFlags local)))
232 gmpflag (usesGMP (configFlags local)))
233
233
234 gmpflag False = []
234 gmpflag False = []
@@ -242,6 +242,7 @@ idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do
242idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do
242idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do
243 installStdLib
243 installStdLib
244 installRTS
244 installRTS
245+ installManPage
245 where
246 where
246 target = datadir $ L.absoluteInstallDirs pkg local copy
247 target = datadir $ L.absoluteInstallDirs pkg local copy
247
248
@@ -254,6 +255,12 @@ idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $
254 putStrLn $ "Installing run time system in " ++ target'
255 putStrLn $ "Installing run time system in " ++ target'
255 makeInstall "rts" target'
256 makeInstall "rts" target'
256
257
258+ installManPage = do
259+ let mandest = (mandir $ L.absoluteInstallDirs pkg local copy) ++ "/man1"
260+ notice verbosity $ unwords ["Copying man page to", mandest]
261+ installOrdinaryFiles verbosity mandest [("man", "idris.1")]
262+
263+
257 makeInstall src target =
264 makeInstall src target =
258 make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local]
265 make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local]
259
266
idris.cabal+2−2
@@ -81,7 +81,6 @@ Extra-doc-files:
81 CONTRIBUTORS
81 CONTRIBUTORS
82 README.md
82 README.md
83 idris-tutorial.pdf
83 idris-tutorial.pdf
84− man/idris.1
85 samples/effects/*.idr
84 samples/effects/*.idr
86 samples/misc/*.idr
85 samples/misc/*.idr
87 samples/misc/*.lidr
86 samples/misc/*.lidr
@@ -91,7 +90,8 @@ Extra-source-files:
91 Makefile
90 Makefile
92 config.mk
91 config.mk
93 stack.yaml
92 stack.yaml
94−
93+ man/idris.1
94+
95 rts/*.c
95 rts/*.c
96 rts/*.h
96 rts/*.h
97 rts/arduino/*.c
97 rts/arduino/*.c