Trans deps v3 (#2584)

* 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

* [ fix ] use backtracking to resolve transitive dependencies

* [ fix ] use backtracking to resolve dependencies

* [ fix ] test pkg006

* Fix missing import

Co-authored-by: stefan-hoeck <hock@zhaw.ch>
This commit is contained in:
Zoe Stafford 2022-09-09 07:08:39 +01:00 committed by GitHub
parent e8b1e34f1c
commit 02dfd6ff6c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
43 changed files with 379 additions and 72 deletions

View File

@ -158,6 +158,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

View File

@ -137,6 +137,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),

View File

@ -13,6 +13,7 @@ import Core.Unify
import Data.List
import Data.Maybe
import Data.SnocList
import Data.String
import Data.These
@ -27,6 +28,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 +247,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 +276,143 @@ 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)
--------------------------------------------------------------------------------
-- Dependency Resolution
--------------------------------------------------------------------------------
record Candidate where
constructor MkCandidate
name : String
version : Maybe PkgVersion
directory : String
toCandidate : (name : String) -> (String,Maybe PkgVersion) -> Candidate
toCandidate name (dir,v) = MkCandidate name v dir
record ResolutionError where
constructor MkRE
decisions : List Candidate
depends : Depends
version : Maybe PkgVersion
prepend : Candidate -> ResolutionError -> ResolutionError
prepend p = { decisions $= (p ::)}
reason : Maybe PkgVersion -> String
reason Nothing = "no matching version is installed"
reason (Just x) = "assigned version \{show x} which is out of bounds"
printResolutionError : ResolutionError -> String
printResolutionError (MkRE ds d v) = go [<] ds
where go : SnocList String -> List Candidate -> String
go ss [] =
let pre := "required \{d.pkgname} \{show d.pkgbounds} but"
in fastConcat . intersperse "; " $ ss <>> ["\{pre} \{reason v}"]
go ss (c :: cs) =
let v := fromMaybe defaultVersion c.version
in go (ss :< "\{c.name}-\{show v}") cs
data ResolutionRes : Type where
Resolved : List String -> ResolutionRes
Failed : List ResolutionError -> ResolutionRes
printErrs : PkgDesc -> List ResolutionError -> String
printErrs x es =
unlines $ "Failed to resolve the dependencies for \{x.name}:"
:: map (indent 2 . printResolutionError) es
-- try all possible resolution paths, keeping the first
-- that works
tryAll : List Candidate
-> (Candidate -> Core ResolutionRes)
-> Core ResolutionRes
tryAll ps f = go [<] ps
where go : SnocList ResolutionError
-> List Candidate
-> Core ResolutionRes
go se [] = pure (Failed $ se <>> [])
go se (x :: xs) = do
Failed errs <- f x | Resolved res => pure (Resolved res)
go (se <>< map (prepend x) errs) xs
addDeps :
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc ->
Core ()
addDeps pkg = do
Resolved allPkgs <- getTransitiveDeps pkg.depends empty
| Failed errs => throw $ GenericMsg EmptyFC (printErrs pkg errs)
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
--
-- We use a backtracking algorithm here: If several versions of
-- a package are installed, we must try all, which are are
-- potentially in bounds, because their set of dependencies
-- might be different across versions and not all of them
-- might lead to a resolvable situation.
getTransitiveDeps :
List Depends ->
(done : StringMap (Maybe PkgVersion)) ->
Core ResolutionRes
getTransitiveDeps [] done = do
ms <- for (StringMap.toList done) $
\(pkg, mv) => findPkgDir pkg (exactBounds mv)
pure . Resolved $ catMaybes ms
getTransitiveDeps (dep :: deps) done =
case lookup dep.pkgname done of
Just mv =>
if inBounds mv dep.pkgbounds
-- already resolved dependency is in bounds
-- so we keep it and resolve remaining deps
then getTransitiveDeps deps done
-- the resolved dependency does not satisfy the
-- current bounds. we return an error and backtrack
else pure (Failed [MkRE [] dep $ mv <|> Just defaultVersion])
Nothing => do
log "package.depends" 50 "adding new dependency: \{dep.pkgname} (\{show dep.pkgbounds})"
pkgDirs <- findPkgDirs dep.pkgname dep.pkgbounds
let candidates := toCandidate dep.pkgname <$> pkgDirs
case candidates of
[] => do
defs <- get Ctxt
if defs.options.session.ignoreMissingPkg
-- this corresponds to what `findPkgDir` does in
-- case of `ignoreMissingPkg` being set to `True`
then getTransitiveDeps deps done
else pure (Failed [MkRE [] dep Nothing])
_ => tryAll candidates $ \(MkCandidate name mv pkgDir) => do
let pkgFile = pkgDir </> name <.> "ipkg"
True <- coreLift $ exists pkgFile
| False => getTransitiveDeps deps (insert name mv done)
pkg <- parsePkgFile False pkgFile
getTransitiveDeps
(pkg.depends ++ deps)
(insert pkg.name pkg.version done)
--------------------------------------------------------------------------------
-- Processing Options
--------------------------------------------------------------------------------
processOptions : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
@ -458,9 +598,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 +839,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 +876,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
@ -856,16 +996,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 =>
@ -878,6 +1013,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)

View File

@ -83,16 +83,24 @@ 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
version = Just (MkPkgVersion (maj ::: [min, patch])) in
MkPkgVersionBounds version True version True
export %inline
defaultVersion : PkgVersion
defaultVersion = MkPkgVersion $ 0 ::: []
export
inBounds : Maybe PkgVersion -> PkgVersionBounds -> Bool
inBounds mv bounds
= let v = fromMaybe (MkPkgVersion (0 ::: [])) mv in
= let v = fromMaybe defaultVersion mv in
maybe True (\v' => if bounds.lowerInclusive
then v >= v'
else v > v') bounds.lowerBound &&
@ -148,7 +156,7 @@ Show Depends where
export
Pretty Void Depends where
pretty = pretty . show
pretty dep = pretty dep.pkgname <+> pretty dep.pkgbounds
------------------------------------------------------------------------------
-- Package description

View File

@ -90,37 +90,59 @@ localPackageDir
let depends = depends_dir (dirs (options defs))
pure $ srcdir </> depends
||| Find all package directories (plus version) matching
||| the given package name and version bounds. Results
||| will be sorted with the latest package version first.
export
findPkgDirs :
Ref Ctxt Defs =>
String ->
PkgVersionBounds ->
Core (List (String, Maybe PkgVersion))
findPkgDirs p bounds = do
defs <- get Ctxt
globaldir <- globalPackageDir
localdir <- localPackageDir
-- Get candidate directories from the global install location,
-- and the local package directory
locFiles <- coreLift $ candidateDirs localdir p bounds
globFiles <- coreLift $ candidateDirs globaldir p bounds
-- Look in all the package paths too
let pkgdirs = (options defs).dirs.package_dirs
pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) pkgdirs
-- If there's anything locally, use that and ignore the global ones
let allFiles = if isNil locFiles
then globFiles ++ concat pkgFiles
else locFiles
-- Sort in reverse order of version number
pure $ sortBy (\x, y => compare (snd y) (snd x)) allFiles
export
findPkgDir :
Ref Ctxt Defs =>
String ->
PkgVersionBounds ->
Core (Maybe String)
findPkgDir p bounds = do
defs <- get Ctxt
[] <- findPkgDirs p bounds | ((p,_) :: _) => pure (Just p)
-- From what remains, pick the one with the highest version number.
-- If there's none, report it
-- (TODO: Can't do this quite yet due to idris2 build system...)
if defs.options.session.ignoreMissingPkg
then pure Nothing
else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
export
addPkgDir : {auto c : Ref Ctxt Defs} ->
String -> PkgVersionBounds -> Core ()
addPkgDir p bounds
= do defs <- get Ctxt
globaldir <- globalPackageDir
localdir <- localPackageDir
-- Get candidate directories from the global install location,
-- and the local package directory
locFiles <- coreLift $ candidateDirs localdir p bounds
globFiles <- coreLift $ candidateDirs globaldir p bounds
-- Look in all the package paths too
let pkgdirs = (options defs).dirs.package_dirs
pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) pkgdirs
-- If there's anything locally, use that and ignore the global ones
let allFiles = if isNil locFiles
then globFiles ++ concat pkgFiles
else locFiles
-- Sort in reverse order of version number
let sorted = sortBy (\x, y => compare (snd y) (snd x)) allFiles
-- From what remains, pick the one with the highest version number.
-- If there's none, report it
-- (TODO: Can't do this quite yet due to idris2 build system...)
case sorted of
[] => if defs.options.session.ignoreMissingPkg
then pure ()
else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
((p, _) :: ps) => addExtraDir p
addPkgDir p bounds = do
Just p <- findPkgDir p bounds
| Nothing => pure ()
addExtraDir p
visiblePackages : String -> IO (List PkgDir)
visiblePackages dir = filter viable <$> getPackageDirs dir

View File

@ -241,7 +241,8 @@ idrisTestsWith = MkTestPool "With abstraction" [] Nothing
idrisTestsIPKG : TestPool
idrisTestsIPKG = MkTestPool "Package and .ipkg files" [] Nothing
["pkg001", "pkg002", "pkg003", "pkg004", "pkg005", "pkg006", "pkg007",
"pkg008", "pkg009", "pkg010", "pkg011", "pkg012"]
"pkg008", "pkg009", "pkg010", "pkg011", "pkg012", "pkg013", "pkg014",
"pkg015"]
idrisTests : TestPool
idrisTests = MkTestPool "Misc" [] Nothing

View File

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

View File

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

View File

@ -1,3 +1,7 @@
Uncaught error: Can't find package foo (>= 0.4 && < 0.5)
Uncaught error: Can't find package baz (any)
Uncaught error: EmptyFC:Failed to resolve the dependencies for test3:
required foo >= 0.4 && < 0.5 but no matching version is installed
Uncaught error: EmptyFC:Failed to resolve the dependencies for test4:
required baz any but no matching version is installed
Warning: Deprecation warning: version numbers must now be of the form x.y.z

View File

@ -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

View File

@ -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

2
tests/idris2/pkg013/.gitignore vendored Normal file
View File

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

View File

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

View File

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

View File

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

View File

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

9
tests/idris2/pkg013/run Normal file
View File

@ -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

View File

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

2
tests/idris2/pkg014/.gitignore vendored Normal file
View File

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

View File

@ -0,0 +1,3 @@
package bar
version = 0.1.0
depends = baz >= 0.1.0

View File

@ -0,0 +1,3 @@
package bar
version = 0.1.1
depends = baz < 0.2.0

View File

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

View File

@ -0,0 +1,2 @@
package baz
version = 0.2.0

View File

@ -0,0 +1,4 @@
package baz
version = 0.3.0
depends = quux

View File

@ -0,0 +1,3 @@
package foo
version = 0.1.0
depends = baz < 0.1.0

View File

@ -0,0 +1,3 @@
package foo
version = 0.2.0
depends = baz >= 0.2.0

View File

@ -0,0 +1,3 @@
package foo
version = 0.3.0
depends = baz >= 0.3.0

View File

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

View File

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

9
tests/idris2/pkg014/run Normal file
View File

@ -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

View File

@ -0,0 +1,20 @@
-- dependencies:
--
-- test
-- |_______
-- | |
-- foo bar
-- | |_____
-- | | |
-- baz baz (quux for bar >= 0.3)
--
-- We can't use the latest foo, because we have a <= 0.2.0 restriction.
-- We also can't use foo-0.1.0, because it transitively depends on baz < 0.1.0,
-- which is not installed. So foo-0.2.0 it is.
--
-- foo-0.2.0 requires baz >= 0.2.0, but baz-0.3.0 requires quux, which is
-- not installed. So baz-0.2.0 it is. So, we can't use bar-0.1.1,
-- which requires baz < 0.2.0. Hence, bar-0.1.0 it is.
package test
depends = foo <= 0.2.0
, bar >= 0.1.0

View File

@ -0,0 +1,4 @@
package bar
version = 0.1.0
depends = baz >= 0.1.0
, prz > 0.1.0

View File

@ -0,0 +1,3 @@
package bar
version = 0.1.1
depends = baz < 0.2.0

View File

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

View File

@ -0,0 +1,2 @@
package baz
version = 0.2.0

View File

@ -0,0 +1,4 @@
package baz
version = 0.3.0
depends = quux

View File

@ -0,0 +1,3 @@
package foo
version = 0.1.0
depends = baz < 0.1.0

View File

@ -0,0 +1,3 @@
package foo
version = 0.2.0
depends = baz >= 0.2.0

View File

@ -0,0 +1,3 @@
package foo
version = 0.3.0
depends = baz >= 0.3.0

View File

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

View File

@ -0,0 +1,6 @@
Uncaught error: EmptyFC:Failed to resolve the dependencies for test:
foo-0.2.0; baz-0.3.0; required quux any but no matching version is installed
foo-0.2.0; baz-0.2.0; bar-0.1.1; required baz < 0.2.0 but assigned version 0.2.0 which is out of bounds
foo-0.2.0; baz-0.2.0; bar-0.1.0; required prz > 0.1.0 but no matching version is installed
foo-0.1.0; required baz < 0.1.0 but no matching version is installed

1
tests/idris2/pkg015/run Normal file
View File

@ -0,0 +1 @@
$1 --build test.ipkg --log package.depends:10

View File

@ -0,0 +1,21 @@
-- dependencies:
--
-- test
-- |_______
-- | |
-- foo bar
-- | |_____
-- | | |
-- baz baz (quux for bar >= 0.3)
--
-- We can't use the latest foo, because we have a <= 0.2.0 restriction.
-- We also can't use foo-0.1.0, because it transitively depends on baz < 0.1.0,
-- which is not installed. So foo-0.2.0 it is.
--
-- foo-0.2.0 requires baz >= 0.2.0, but baz-0.3.0 requires quux, which is
-- not installed. So baz-0.2.0 it is. So, we can't use bar-0.1.1,
-- which requires baz < 0.2.0. Hence, bar-0.1.0 it is, but this
-- requires prz, which is not installed. And so this fails.
package test
depends = foo <= 0.2.0
, bar >= 0.1.0