Merge pull request idris-lang#70 from jfdm/expand-ipkg-contents

Align the IPKG format more with the previous Idris implementation.

docs/index.rst

@@ -21,3 +21,4 @@ This is a placeholder, to get set up with readthedocs.
    :maxdepth: 1
 
    faq/faq
+   reference/index

docs/reference/index.rst

@@ -0,0 +1,19 @@
+**********************
+Idris2 Reference Guide
+**********************
+
+.. note::
+
+   The documentation for Idris 2 has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+This is a placeholder, to get set up with readthedocs.
+
+.. toctree::
+   :maxdepth: 1
+
+   packages

docs/reference/packages.rst

@@ -0,0 +1,102 @@
+.. _ref-sect-packages:
+
+********
+Packages
+********
+
+Idris includes a simple system for building packages from a package
+description file.  These files can be used with the Idris compiler to
+manage the development process of your Idris programmes and packages.
+
+Package Descriptions
+====================
+
+A package description includes the following:
+
++ A header, consisting of the keyword package followed by the package
+  name. Package names can be any valid Idris identifier. The iPKG
+  format also takes a quoted version that accepts any valid filename.
++ Fields describing package contents, ``<field> = <value>``
+
+At least one field must be the modules field, where the value is a
+comma separated list of modules.  For example, a library test which
+has two modules ``Foo.idr`` and ``Bar.idr`` as source files would be
+written as follows::
+
+    package test
+
+    modules = Foo, Bar
+
+Other examples of package files can be found in the ``libs`` directory
+of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
+
+Metadata
+--------
+
+The `iPKG` format supports additional metadata associated with the package.
+The added fields are:
+
++ ``brief = "<text>"``, a string literal containing a brief description
+  of the package.
+
++ ``version = "<text>""``, a version string to associate with the package.
+
++ ``readme = "<file>""``, location of the README file.
+
++ ``license = "<text>"``, a string description of the licensing
+  information.
+
++ ``authors = "<text>"``, the author information.
+
++ ``maintainers = "<text>"``, Maintainer information.
+
++ ``homepage = "<url>"``, the website associated with the package.
+
++ ``sourceloc = "<url>"``, the location of the DVCS where the source
+  can be found.
+
++ ``bugtracker = "<url>"``, the location of the project's bug tracker.
+
+
+Common Fields
+-------------
+
+Other common fields which may be present in an ``ipkg`` file are:
+
++ ``executable = <output>``, which takes the name of the executable
+  file to generate. Executable names can be any valid Idris
+  identifier. the iPKG format also takes a quoted version that accepts
+  any valid filename.
+
++ ``main = <module>``, which takes the name of the main module, and
+  must be present if the executable field is present.
+
++ ``opts = "<idris options>"``, which allows options to be passed to
+  Idris.
+
++ ``depends = <pkg name> (',' <pkg name>)+``, a comma separated list of
+  package names that the Idris package requires.
+
+
+Comments
+---------
+
+Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.
+
+Using Package files
+===================
+
+Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler as follows:
+
++ ``idris2 --build test.ipkg`` will build all modules in the package
+
++ ``idris2 --install test.ipkg`` will install the package, making it
+  accessible by other Idris libraries and programs.
+
++ ``idris2 --clean test.ipkg`` will clean the intermediate build files.
+
+Once the test package has been installed, the command line option
+``--package test`` makes it accessible (abbreviated to ``-p test``).
+For example::
+
+    idris -p test Main.idr

src/Idris/Package.idr

@@ -30,6 +30,13 @@ record PkgDesc where
   name : String
   version : String
   authors : String
+  maintainers : Maybe String
+  license : Maybe String
+  brief   : Maybe String
+  readme  : Maybe String
+  homepage : Maybe String
+  sourceloc : Maybe String
+  bugtracker : Maybe String
   depends : List String -- packages to add to search path
   modules : List (List String, String) -- modules to install (namespace, filename)
   mainmod : Maybe (List String, String) -- main file (i.e. file to load at REPL)
@@ -44,6 +51,13 @@ Show PkgDesc where
   show pkg = "Package: " ++ name pkg ++ "\n" ++
              "Version: " ++ version pkg ++ "\n" ++
              "Authors: " ++ authors pkg ++ "\n" ++
+             maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
+             maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++
+             maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++
+             maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++
+             maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++
+             maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++
+             maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++
              "Depends: " ++ show (depends pkg) ++ "\n" ++
              "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
              maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
@@ -56,26 +70,42 @@ Show PkgDesc where
 
 initPkgDesc : String -> PkgDesc
 initPkgDesc pname
-    = MkPkgDesc pname "0" "Anonymous" [] []
+    = MkPkgDesc pname "0" "Anonymous" Nothing Nothing
+                Nothing Nothing Nothing Nothing Nothing
+                [] []
                 Nothing Nothing Nothing Nothing Nothing Nothing Nothing
 
 data DescField : Type where
-  PVersion : FC -> String -> DescField
-  PAuthors : FC -> String -> DescField
-  PDepends : List String -> DescField
-  PModules : List (FC, List String) -> DescField
-  PMainMod : FC -> List String -> DescField
-  PExec : String -> DescField
-  POpts : FC -> String -> DescField
-  PPrebuild : FC -> String -> DescField
-  PPostbuild : FC -> String -> DescField
-  PPreinstall : FC -> String -> DescField
+  PVersion     : FC -> String -> DescField
+  PAuthors     : FC -> String -> DescField
+  PMaintainers : FC -> String -> DescField
+  PLicense     : FC -> String -> DescField
+  PBrief       : FC -> String -> DescField
+  PReadMe      : FC -> String -> DescField
+  PHomePage    : FC -> String -> DescField
+  PSourceLoc   : FC -> String -> DescField
+  PBugTracker  : FC -> String -> DescField
+  PDepends     : List String -> DescField
+  PModules     : List (FC, List String) -> DescField
+  PMainMod     : FC -> List String -> DescField
+  PExec        : String -> DescField
+  POpts        : FC -> String -> DescField
+  PPrebuild    : FC -> String -> DescField
+  PPostbuild   : FC -> String -> DescField
+  PPreinstall  : FC -> String -> DescField
   PPostinstall : FC -> String -> DescField
 
 field : String -> Rule DescField
 field fname
       = strField PVersion "version"
     <|> strField PAuthors "authors"
+    <|> strField PMaintainers "maintainers"
+    <|> strField PLicense "license"
+    <|> strField PBrief "brief"
+    <|> strField PReadMe "readme"
+    <|> strField PHomePage "homepage"
+    <|> strField PSourceLoc "sourceloc"
+    <|> strField PBugTracker "bugtracker"
     <|> strField POpts "options"
     <|> strField POpts "opts"
     <|> strField PPrebuild "prebuild"
@@ -86,7 +116,7 @@ field fname
            ds <- sepBy1 (symbol ",") unqualifiedName
            pure (PDepends ds)
     <|> do exactIdent "modules"; symbol "="
-           ms <- sepBy1 (symbol ",") 
+           ms <- sepBy1 (symbol ",")
                       (do start <- location
                           ns <- namespace_
                           end <- location
@@ -126,8 +156,16 @@ addField : {auto c : Ref Ctxt Defs} ->
            DescField -> PkgDesc -> Core PkgDesc
 addField (PVersion fc n) pkg = pure (record { version = n } pkg)
 addField (PAuthors fc a) pkg = pure (record { authors = a } pkg)
+addField (PMaintainers fc a) pkg = pure (record { maintainers = Just a } pkg)
+addField (PLicense fc a) pkg = pure (record { license = Just a } pkg)
+addField (PBrief fc a) pkg = pure (record { brief = Just a } pkg)
+addField (PReadMe fc a) pkg = pure (record { readme = Just a } pkg)
+addField (PHomePage fc a) pkg = pure (record { homepage = Just a } pkg)
+addField (PSourceLoc fc a) pkg = pure (record { sourceloc = Just a } pkg)
+addField (PBugTracker fc a) pkg = pure (record { bugtracker = Just a } pkg)
+
 addField (PDepends ds) pkg = pure (record { depends = ds } pkg)
-addField (PModules ms) pkg 
+addField (PModules ms) pkg
     = pure (record { modules = !(traverse toSource ms) } pkg)
   where
     toSource : (FC, List String) -> Core (List String, String)
@@ -148,7 +186,7 @@ addFields (x :: xs) desc = addFields xs !(addField x desc)
 
 runScript : Maybe (FC, String) -> Core ()
 runScript Nothing = pure ()
-runScript (Just (fc, s)) 
+runScript (Just (fc, s))
     = do res <- coreLift $ system s
          when (res /= 0) $
             throw (GenericMsg fc "Script failed")
@@ -167,7 +205,7 @@ processOptions Nothing = pure ()
 processOptions (Just (fc, opts))
     = do let Right clopts = getOpts (words opts)
                 | Left err => throw (GenericMsg fc err)
-         preOptions clopts 
+         preOptions clopts
 
 build : {auto c : Ref Ctxt Defs} ->
         {auto s : Ref Syn SyntaxInfo} ->
@@ -200,7 +238,7 @@ installFrom pname builddir destdir ns@(m :: dns)
          let ttcPath = builddir ++ dirSep ++ ttcfile ++ ".ttc"
          let destPath = destdir ++ dirSep ++ showSep "/" (reverse dns)
          let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc"
-         Right _ <- coreLift $ mkdirs (reverse dns) 
+         Right _ <- coreLift $ mkdirs (reverse dns)
              | Left err => throw (FileErr pname err)
          coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
          Right _ <- coreLift $ copyFile ttcPath destFile
@@ -210,10 +248,10 @@ installFrom pname builddir destdir ns@(m :: dns)
 -- Install all the built modules in prefix/package/
 -- We've already built and checked for success, so if any don't exist that's
 -- an internal error.
-install : {auto c : Ref Ctxt Defs} -> 
+install : {auto c : Ref Ctxt Defs} ->
           {auto o : Ref ROpts REPLOpts} ->
           PkgDesc -> Core ()
-install pkg 
+install pkg
     = do defs <- get Ctxt
          let build = build_dir (dirs (options defs))
          runScript (preinstall pkg)
@@ -230,12 +268,12 @@ install pkg
          True <- coreLift $ changeDir (name pkg)
              | False => throw (FileErr (name pkg) FileReadError)
 
-         -- We're in that directory now, so copy the files from 
+         -- We're in that directory now, so copy the files from
          -- srcdir/build into it
          traverse (installFrom (name pkg)
-                               (srcdir ++ dirSep ++ build) 
+                               (srcdir ++ dirSep ++ build)
                                (installPrefix ++ dirSep ++ name pkg)) toInstall
-         coreLift $ changeDir srcdir                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    
+         coreLift $ changeDir srcdir
          runScript (postinstall pkg)
 
 -- Data.These.bitraverse hand specialised for Core
@@ -257,10 +295,10 @@ foldWithKeysC {a} {b} fk fv = go []
     map bifold $ bitraverseC
                    (fv as)
                    (\sm => foldlC
-                             (\x, (k, vs) => 
+                             (\x, (k, vs) =>
                                do let as' = as ++ [k]
                                   y <- assert_total $ go as' vs
-                                  z <- fk as'  
+                                  z <- fk as'
                                   pure $ x <+> y <+> z)
                              neutral
                              (toList sm))
@@ -272,10 +310,10 @@ Semigroup () where
 Monoid () where
   neutral = ()
 
-clean : {auto c : Ref Ctxt Defs} -> 
+clean : {auto c : Ref Ctxt Defs} ->
         {auto o : Ref ROpts REPLOpts} ->
         PkgDesc -> Core ()
-clean pkg 
+clean pkg
     = do defs <- get Ctxt
          let build = build_dir (dirs (options defs))
          let toClean = mapMaybe (\ks => [| MkPair (tail' ks) (head' ks) |]) $
@@ -286,12 +324,12 @@ clean pkg
          let builddir = srcdir ++ dirSep ++ build
          -- the usual pair syntax breaks with `No such variable a` here for some reason
          let pkgTrie = the (StringTrie (List String)) $
-                       foldl (\trie, ksv => 
+                       foldl (\trie, ksv =>
                                 let ks = fst ksv
-                                    v = snd ksv  
-                                  in 
+                                    v = snd ksv
+                                  in
                                 insertWith ks (maybe [v] (v::)) trie) empty toClean
-         foldWithKeysC (deleteFolder builddir) 
+         foldWithKeysC (deleteFolder builddir)
                        (\ks => map concat . traverse (deleteBin builddir ks))
                        pkgTrie
          deleteFolder builddir []
@@ -311,20 +349,20 @@ clean pkg
 
 -- Just load the 'Main' module, if it exists, which will involve building
 -- it if necessary
-runRepl : {auto c : Ref Ctxt Defs} -> 
+runRepl : {auto c : Ref Ctxt Defs} ->
           {auto o : Ref ROpts REPLOpts} ->
           PkgDesc -> Core ()
-runRepl pkg 
-    = do addDeps pkg 
+runRepl pkg
+    = do addDeps pkg
          processOptions (options pkg)
          throw (InternalError "Not implemented")
 
 processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  PkgCommand -> String -> Core ()
-processPackage cmd file 
-    = do Right (pname, fs) <- coreLift $ parseFile file 
+processPackage cmd file
+    = do Right (pname, fs) <- coreLift $ parseFile file
                                   (do desc <- parsePkgDesc file
                                       eoi
                                       pure desc)
@@ -354,7 +392,7 @@ processPackageOpts : {auto c : Ref Ctxt Defs} ->
                      {auto s : Ref Syn SyntaxInfo} ->
                      {auto o : Ref ROpts REPLOpts} ->
                      List CLOpt -> Core Bool
-processPackageOpts [Package cmd f] 
+processPackageOpts [Package cmd f]
     = do processPackage cmd f
          pure True
 processPackageOpts opts = rejectPackageOpts opts

tests/Main.idr

@@ -46,6 +46,7 @@ idrisTests
        "perf001", "perf002",
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
+       "pkg001",
        "record001", "record002",
        "reg001",
        "total001", "total002", "total003", "total004", "total005",