Transitive dependencies v2 (#2496)

* make `depends` collect all transitive dependencies

This happens by installing the (modified) ipkg file along with ttc files

* [ fix ] parsing a package shouldn't always set sourceDir

* linter *sigh*

* Fix test, add changelog

`asDepends` has been changed to `setSrc` as that is for me more intuitive

in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder

idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info

* (hopefully) fix idris2/pkg13 test on windows

* Actually install the version
This should make things start working

CHANGELOG.md

@@ -141,6 +141,7 @@
 ### Other changes
 
 * Adds docstrings for the lambda-lifted IR.
+* Package files are now installed along-side build artifacts for installed packages. This means all transitive dependencies of packages you specify with the `depends` field are added automatically.
 
 ## v0.5.0/0.5.1
 

src/Core/Options/Log.idr

@@ -131,6 +131,7 @@ knownTopics = [
     ("metadata.names", Nothing),
     ("module", Nothing),
     ("module.hash", Nothing),
+    ("package.depends", Just "Log which packages are being added"),
     ("quantity", Nothing),
     ("quantity.hole", Nothing),
     ("quantity.hole.update", Nothing),

src/Idris/Package.idr

@@ -27,6 +27,7 @@ import Libraries.Data.StringMap
 import Libraries.Data.StringTrie
 import Libraries.Text.Parser
 import Libraries.Utils.Path
+import Libraries.Text.PrettyPrint.Prettyprinter.Render.String
 
 import Idris.CommandLine
 import Idris.Doc.HTML
@@ -245,16 +246,19 @@ addField (PPostclean fc e)   pkg = pure $ { postclean := Just (fc, e) } pkg
 addFields : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto o : Ref ROpts REPLOpts} ->
+            (setSrc : Bool) ->
             List DescField -> PkgDesc -> Core PkgDesc
-addFields xs desc = do p <- newRef ParsedMods []
-                       m <- newRef MainMod Nothing
-                       added <- go {p} {m} xs desc
-                       setSourceDir (sourcedir added)
-                       ms <- get ParsedMods
-                       mmod <- get MainMod
-                       pure $ { modules := !(traverse toSource ms)
-                              , mainmod := !(traverseOpt toSource mmod)
-                              } added
+addFields setSrc xs desc = do
+  p <- newRef ParsedMods []
+  m <- newRef MainMod Nothing
+  added <- go {p} {m} xs desc
+  when setSrc $ setSourceDir (sourcedir added)
+  ms <- get ParsedMods
+  mmod <- get MainMod
+  pure $
+    { modules := !(traverse toSource ms)
+    , mainmod := !(traverseOpt toSource mmod)
+    } added
   where
     toSource : (FC, ModuleIdent) -> Core (ModuleIdent, String)
     toSource (loc, ns) = pure (ns, !(nsToSource loc ns))
@@ -271,8 +275,55 @@ runScript (Just (fc, s))
          when (res /= 0) $
             throw (GenericMsg fc "Script failed")
 
-addDeps : {auto c : Ref Ctxt Defs} -> PkgDesc -> Core ()
-addDeps pkg = traverse_ (\p => addPkgDir p.pkgname p.pkgbounds) (depends pkg)
+export
+parsePkgFile : {auto c : Ref Ctxt Defs} ->
+               {auto s : Ref Syn SyntaxInfo} ->
+               {auto o : Ref ROpts REPLOpts} ->
+               (setSrc : Bool) -> -- parse package file as a dependency
+               String -> Core PkgDesc
+parsePkgFile setSrc file = do
+    Right (pname, fs) <- coreLift $ parseFile file $ parsePkgDesc file <* eoi
+        | Left err => throw err
+    addFields setSrc fs (initPkgDesc pname)
+
+addDeps :
+    {auto c : Ref Ctxt Defs} ->
+    {auto s : Ref Syn SyntaxInfo} ->
+    {auto o : Ref ROpts REPLOpts} ->
+    PkgDesc ->
+    Core ()
+addDeps pkg = do
+    allPkgs <- getTransitiveDeps pkg.depends empty
+    log "package.depends" 10 $ "all depends: \{show allPkgs}"
+    traverse_ addExtraDir allPkgs
+  where
+    -- Note: findPkgDir throws an error if a package is not found
+    -- *unless* --ignore-missing-ipkg is enabled
+    -- therefore, findPkgDir returns Nothing, skip the package
+    getTransitiveDeps :
+        List Depends ->
+        (done : StringMap (Maybe PkgVersion)) ->
+        Core (List String) -- package directories to add
+    getTransitiveDeps [] done =
+        map catMaybes $ traverse
+            (\(pkg, mv) => findPkgDir pkg (exactBounds mv))
+            $ StringMap.toList done
+    getTransitiveDeps (dep :: deps) done =
+        case lookup dep.pkgname done of
+            Just mv => if inBounds mv dep.pkgbounds
+                then getTransitiveDeps deps done
+                else throw $ GenericMsg EmptyFC "2 versions of the same package are required, this is unsupported"
+            Nothing => do
+                log "package.depends" 50 "adding new dependency: \{dep.pkgname} (\{show dep.pkgbounds})"
+                Just pkgDir <- findPkgDir dep.pkgname dep.pkgbounds
+                    | Nothing => getTransitiveDeps deps done
+                let pkgFile = pkgDir </> dep.pkgname <.> "ipkg"
+                True <- coreLift $ exists pkgFile
+                    | False => getTransitiveDeps deps (insert dep.pkgname Nothing done)
+                pkg <- parsePkgFile False pkgFile
+                getTransitiveDeps
+                    (pkg.depends ++ deps)
+                    (insert pkg.name pkg.version done)
 
 processOptions : {auto c : Ref Ctxt Defs} ->
                  {auto o : Ref ROpts REPLOpts} ->
@@ -458,9 +509,24 @@ install pkg opts installSrc -- not used but might be in the future
          traverse_ (installFrom (wdir </> build) targetDir . fst) toInstall
          when installSrc $ do
            traverse_ (installSrcFrom wdir targetDir) toInstall
+
+         -- install package file
+         let pkgFile = targetDir </> pkg.name <.> "ipkg"
+         coreLift $ putStrLn $ "Installing package file for \{pkg.name} to \{targetDir}"
+         let pkgStr = String.renderString $ layoutUnbounded $ pretty $ savePkgMetadata pkg
+         log "package.depends" 25 $ "  package file:\n\{pkgStr}"
+         coreLift_ $ writeFile pkgFile pkgStr
+
          coreLift_ $ changeDir wdir
 
          runScript (postinstall pkg)
+  where
+    savePkgMetadata : PkgDesc -> PkgDesc
+    savePkgMetadata pkg =
+      the (PkgDesc -> PkgDesc)
+      { depends := pkg.depends
+      , version := pkg.version
+      } $ initPkgDesc pkg.name
 
 -- Check package without compiling anything.
 check : {auto c : Ref Ctxt Defs} ->
@@ -684,19 +750,6 @@ runRepl fname = do
         displayErrors errs
   repl {u} {s}
 
-export
-parsePkgFile : {auto c : Ref Ctxt Defs} ->
-               {auto s : Ref Syn SyntaxInfo} ->
-               {auto o : Ref ROpts REPLOpts} ->
-               String -> Core PkgDesc
-parsePkgFile file = do
-  Right (pname, fs) <- coreLift $ parseFile file
-                                          (do desc <- parsePkgDesc file
-                                              eoi
-                                              pure desc)
-      | Left err => throw err
-  addFields fs (initPkgDesc pname)
-
 ||| If the user did not provide a package file we can look in the working
 ||| directory. If there is exactly one `.ipkg` file then use that!
 localPackageFile : Maybe String -> Core String
@@ -734,9 +787,7 @@ processPackage opts (cmd, mfile)
                  | _ => do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
                            coreLift (exitWith (ExitFailure 1))
              setWorkingDir dir
-             Right (pname, fs) <- coreLift $ parseFile filename (parsePkgDesc filename <* eoi)
-                | Left err => throw err
-             pkg <- addFields fs (initPkgDesc pname)
+             pkg <- parsePkgFile True filename
              whenJust (builddir pkg) setBuildDir
              setOutputDir (outputdir pkg)
              case cmd of
@@ -853,16 +904,11 @@ findIpkg fname
              | Nothing => pure fname
         coreLift_ $ changeDir dir
         setWorkingDir dir
-        Right (pname, fs) <- coreLift $ parseFile ipkgn
-                                 (do desc <- parsePkgDesc ipkgn
-                                     eoi
-                                     pure desc)
-            | Left err => throw err
-        pkg <- addFields fs (initPkgDesc pname)
+        pkg <- parsePkgFile True ipkgn
         maybe (pure ()) setBuildDir (builddir pkg)
         setOutputDir (outputdir pkg)
         processOptions (options pkg)
-        loadDependencies (depends pkg)
+        addDeps pkg
         case fname of
              Nothing => pure Nothing
              Just srcpath  =>
@@ -875,6 +921,3 @@ findIpkg fname
     dropHead str [] = []
     dropHead str (x :: xs)
         = if x == str then xs else x :: xs
-
-    loadDependencies : List Depends -> Core ()
-    loadDependencies = traverse_ (\p => addPkgDir p.pkgname p.pkgbounds)

src/Idris/Package/Types.idr

@@ -83,6 +83,10 @@ export
 anyBounds : PkgVersionBounds
 anyBounds = MkPkgVersionBounds Nothing True Nothing True
 
+export
+exactBounds : Maybe PkgVersion -> PkgVersionBounds
+exactBounds mv = MkPkgVersionBounds mv True mv True
+
 export
 current : PkgVersionBounds
 current = let (maj,min,patch) = semVer version
@@ -148,7 +152,7 @@ Show Depends where
 
 export
 Pretty Void Depends where
-  pretty = pretty . show
+  pretty dep = pretty dep.pkgname <+> pretty dep.pkgbounds
 
 ------------------------------------------------------------------------------
 -- Package description

src/Idris/SetOptions.idr

@@ -91,9 +91,12 @@ localPackageDir
          pure $ srcdir </> depends
 
 export
-addPkgDir : {auto c : Ref Ctxt Defs} ->
-            String -> PkgVersionBounds -> Core ()
-addPkgDir p bounds
+findPkgDir :
+    Ref Ctxt Defs =>
+    String ->
+    PkgVersionBounds ->
+    Core (Maybe String)
+findPkgDir p bounds
     = do defs <- get Ctxt
          globaldir <- globalPackageDir
          localdir <- localPackageDir
@@ -118,9 +121,17 @@ addPkgDir p bounds
          -- (TODO: Can't do this quite yet due to idris2 build system...)
          case sorted of
               [] => if defs.options.session.ignoreMissingPkg
-                       then pure ()
+                       then pure Nothing
                        else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
-              ((p, _) :: ps) => addExtraDir p
+              ((p, _) :: ps) => pure $ Just p
+
+export
+addPkgDir : {auto c : Ref Ctxt Defs} ->
+            String -> PkgVersionBounds -> Core ()
+addPkgDir p bounds = do
+    Just p <- findPkgDir p bounds
+        | Nothing => pure ()
+    addExtraDir p
 
 visiblePackages : String -> IO (List PkgDir)
 visiblePackages dir = filter viable <$> getPackageDirs dir

tests/Main.idr

@@ -245,7 +245,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        "params001", "params002", "params003",
        -- Packages and ipkg files
        "pkg001", "pkg002", "pkg003", "pkg004", "pkg005", "pkg006", "pkg007",
-       "pkg008", "pkg009", "pkg010", "pkg011", "pkg012",
+       "pkg008", "pkg009", "pkg010", "pkg011", "pkg012", "pkg013",
        -- Larger programs arising from real usage. Typically things with
        -- interesting interactions between features
        "real001", "real002",

tests/idris2/pkg006/depends/bar-baz/bar-baz.ipkg

@@ -1,2 +1,2 @@
 package bar-baz
-version = 1.0.1
+-- version = 1.0.1

tests/idris2/pkg006/depends/quux/quux.ipkg

@@ -1,2 +1,2 @@
 package quux
-version = 0.0.0
+-- version = 0.0.0

tests/idris2/pkg010/expected.in

@@ -1,3 +1,4 @@
 1/1: Building Main (Main.idr)
 Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.5.1/testpkg-0
 Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.5.1/testpkg-0
+Installing package file for testpkg to __PWD__currently/nonexistent/dir/idris2-0.5.1/testpkg-0

tests/idris2/pkg010/run

@@ -9,6 +9,8 @@ MY_PWD="${MY_PWD}" ./gen_expected.sh
 export IDRIS2_PACKAGE_PATH=$IDRIS2_PREFIX/$NAME_VERSION
 export IDRIS2_PREFIX=${MY_PWD}currently/nonexistent/dir/
 
+export IDRIS2_INC_CGS=
+
 $1 --install ./testpkg.ipkg
 
 # ../ is there for some extra safety for using rm -rf

tests/idris2/pkg013/.gitignore

@@ -0,0 +1,2 @@
+/expected
+

tests/idris2/pkg013/depends/bar-0.7.2/bar.ipkg

@@ -0,0 +1,4 @@
+package bar
+version = 0.7.2
+
+depends = foo >= 0.1.0

tests/idris2/pkg013/depends/foo-0.1.0/foo.ipkg

@@ -0,0 +1,2 @@
+package foo
+version = 0.1.0

tests/idris2/pkg013/expected.in

@@ -0,0 +1 @@
+LOG package.depends:10: all depends: ["__PWD__depends/bar-0.7.2", "__PWD__depends/foo-0.1.0"]

tests/idris2/pkg013/gen_expected.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env sh
+
+sed -e "s|__PWD__|${MY_PWD}|g" expected.in >expected

tests/idris2/pkg013/run

@@ -0,0 +1,9 @@
+if [ "$OS" = "windows" ]; then
+    MY_PWD="$(cygpath -m "$(pwd)")\\\\"
+else
+    MY_PWD="$(pwd)/"
+fi
+
+MY_PWD="${MY_PWD}" ./gen_expected.sh
+
+$1 --build test.ipkg --log package.depends:10

tests/idris2/pkg013/test.ipkg

@@ -0,0 +1,2 @@
+package test
+depends = bar