[ new ] put TTC files in a version-tagged directory (#2684)

src/Compiler/Scheme/Chez.idr

@@ -218,8 +218,9 @@ loadSO : {auto c : Ref Ctxt Defs} ->
 loadSO appdir "" = pure ""
 loadSO appdir mod
     = do d <- getDirs
-         let fs = map (\p => p </> mod)
-                      ((build_dir d </> "ttc") :: extra_dirs d)
+         bdir <- ttcBuildDirectory
+         allDirs <- extraSearchDirectories
+         let fs = map (\p => p </> mod) (bdir :: allDirs)
          Just fname <- firstAvailable fs
             | Nothing => throw (InternalError ("Missing .so:" ++ mod))
          -- Easier to put them all in the same directory, so we don't need
@@ -629,7 +630,7 @@ incCompile c s sourceFile
          cdata <- getIncCompileData False Cases
 
          d <- getDirs
-         let outputDir = build_dir d </> "ttc"
+         outputDir <- ttcBuildDirectory
 
          let ndefs = namedDefs cdata
          if isNil ndefs

src/Core/Context.idr

@@ -2088,7 +2088,7 @@ addExtraDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 addExtraDir dir = update Ctxt { options->dirs->extra_dirs $= (++ [dir]) }
 
 export
-addPackageDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
+addPackageDir: {auto c : Ref Ctxt Defs} -> String -> Core ()
 addPackageDir dir = update Ctxt { options->dirs->package_dirs $= (++ [dir]) }
 
 export

src/Core/Directory.idr

@@ -1,13 +1,17 @@
 module Core.Directory
 
+import Core.Binary
 import Core.Context
 import Core.Context.Log
 import Core.Core
 import Core.FC
 import Core.Options
 
+import Idris.Version
+
 import Parser.Unlit
 
+import Libraries.Data.Version
 import Libraries.Utils.Path
 
 import Data.List
@@ -17,6 +21,46 @@ import System.Directory
 
 %default total
 
+------------------------------------------------------------------------
+-- Package directories
+
+export
+pkgGlobalDirectory : {auto c : Ref Ctxt Defs} -> Core String
+pkgGlobalDirectory =
+  do d <- getDirs
+     pure (prefix_dir d </> "idris2-" ++ showVersion False version)
+
+export
+pkgLocalDirectory : {auto c : Ref Ctxt Defs} -> Core String
+pkgLocalDirectory =
+  do d <- getDirs
+     Just srcdir <- coreLift currentDir
+       | Nothing => throw (InternalError "Can't get current directory")
+     pure $ srcdir </> depends_dir d
+
+------------------------------------------------------------------------
+-- TTC directories
+
+export
+ttcBuildDirectory : {auto c : Ref Ctxt Defs} -> Core String
+ttcBuildDirectory =
+  do d <- getDirs
+     pure (build_dir d </> "ttc" </> show ttcVersion)
+
+export
+ttcInstallDirectory : {auto c : Ref Ctxt Defs} -> String -> Core String
+ttcInstallDirectory lib =
+  do gbdir <- pkgGlobalDirectory
+     pure (gbdir </> lib </> show ttcVersion)
+
+export
+extraSearchDirectories : {auto c : Ref Ctxt Defs} -> Core (List String)
+extraSearchDirectories =
+  do d <- getDirs
+     pure (map (</> show ttcVersion) (extra_dirs d ++ package_dirs d))
+
+------------------------------------------------------------------------
+
 public export
 data IdrSrcExt = E_idr | E_lidr | E_yaff | E_org | E_md
 
@@ -126,10 +170,10 @@ export
 nsToPath : {auto c : Ref Ctxt Defs} ->
            FC -> ModuleIdent -> Core (Either Error String)
 nsToPath loc ns
-    = do d <- getDirs
+    = do bdir <- ttcBuildDirectory
+         ttcs <- extraSearchDirectories
          let fnameBase = ModuleIdent.toPath ns
-         let fs = map (\p => cleanPath $ p </> fnameBase <.> "ttc")
-                      ((build_dir d </> "ttc") :: extra_dirs d)
+         let fs = map (\p => cleanPath $ p </> fnameBase <.> "ttc") (bdir :: ttcs)
          Just f <- firstAvailable fs
             | Nothing => pure (Left (ModuleNotFound loc ns))
          pure (Right f)
@@ -207,12 +251,11 @@ covering
 makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                      ModuleIdent -> Core ()
 makeBuildDirectory ns
-    = do d <- getDirs
-         let bdir = build_dir d </> "ttc"
+    = do bdir <- ttcBuildDirectory
          let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name
          let ndir = joinPath ns
          Right _ <- coreLift $ mkdirAll (bdir </> ndir)
-            | Left err => throw (FileErr (build_dir d </> ndir) err)
+            | Left err => throw (FileErr (bdir </> ndir) err)
          pure ()
 
 export
@@ -232,9 +275,8 @@ getTTCFileName inp ext
          -- and generate the ttc file from that
          ns <- ctxtPathToNS inp
          let fname = ModuleIdent.toPath ns <.> ext
-         d <- getDirs
-         let bdir = build_dir d
-         pure $ bdir </> "ttc" </> fname
+         bdir <- ttcBuildDirectory
+         pure $ bdir </> fname
 
 -- Given a source file, return the name of the corresponding object file.
 -- As above, but without the build directory

src/Idris/Package.idr

@@ -357,7 +357,7 @@ 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
+  traverse_ addPackageDir allPkgs
   where
     -- Note: findPkgDir throws an error if a package is not found
     -- *unless* --ignore-missing-ipkg is enabled
@@ -487,14 +487,14 @@ installFrom : {auto o : Ref ROpts REPLOpts} ->
               String -> String -> ModuleIdent -> Core ()
 installFrom builddir destdir ns
     = do let ttcfile = ModuleIdent.toPath ns
-         let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
+         let ttcPath = builddir </> ttcfile <.> "ttc"
          objPaths_in <- traverse
                      (\cg =>
                         do Just cgdata <- getCG cg
                                 | Nothing => pure Nothing
                            let Just ext = incExt cgdata
                                 | Nothing => pure Nothing
-                           let srcFile = builddir </> "ttc" </> ttcfile <.> ext
+                           let srcFile = builddir </> ttcfile <.> ext
                            let destFile = destdir </> ttcfile <.> ext
                            let Just (dir, _) = splitParent destFile
                                 | Nothing => pure Nothing
@@ -574,7 +574,8 @@ install : {auto c : Ref Ctxt Defs} ->
           Core ()
 install pkg opts installSrc -- not used but might be in the future
     = do defs <- get Ctxt
-         let build = build_dir (dirs (options defs))
+         build <- ttcBuildDirectory
+         targetDir <- ttcInstallDirectory (installDir pkg)
          let src = source_dir (dirs (options defs))
          runScript (preinstall pkg)
          let toInstall = maybe (modules pkg)
@@ -582,9 +583,6 @@ install pkg opts installSrc -- not used but might be in the future
                                (mainmod pkg)
          wdir <- getWorkingDir
          -- Make the package installation directory
-         let targetDir = prefix_dir (dirs (options defs)) </>
-                             "idris2-" ++ showVersion False version </>
-                             installDir pkg
          Right _ <- coreLift $ mkdirAll targetDir
              | Left err => throw $ InternalError $ unlines
                              [ "Can't make directory " ++ targetDir
@@ -785,7 +783,8 @@ clean pkg opts -- `opts` is not used but might be in the future
                           pkgmods
          srcdir <- getWorkingDir
          let d = dirs (options defs)
-         let builddir = srcdir </> build_dir d </> "ttc"
+         bdir <- ttcBuildDirectory
+         let builddir = srcdir </> bdir </> "ttc"
          let outputdir = srcdir </> outputDirWithDefault d
          -- the usual pair syntax breaks with `No such variable a` here for some reason
          let pkgTrie : StringTrie (List String)

src/Idris/REPL.idr

@@ -1074,7 +1074,7 @@ process ShowVersion
     = pure $ VersionIs  version
 process (ImportPackage package) = do
   defs <- get Ctxt
-  let searchDirs = defs.options.dirs.extra_dirs
+  searchDirs <- extraSearchDirectories
   let Just packageDir = find
         (\d => isInfixOf package (fromMaybe d (fileName d)))
         searchDirs

src/Idris/SetOptions.idr

@@ -3,6 +3,7 @@ module Idris.SetOptions
 import Compiler.Common
 
 import Core.Context
+import Core.Directory
 import Core.Metadata
 import Core.Options
 import Core.Unify
@@ -76,20 +77,6 @@ candidateDirs dname pkg bounds =
           do guard (pkgName == pkg && inBounds ver bounds)
              pure ((dname </> dirName), ver)
 
-globalPackageDir : {auto c : Ref Ctxt Defs} -> Core String
-globalPackageDir
-    = do defs <- get Ctxt
-         pure $ prefix_dir (dirs (options defs)) </>
-                  "idris2-" ++ showVersion False version
-
-localPackageDir : {auto c : Ref Ctxt Defs} -> Core String
-localPackageDir
-    = do defs <- get Ctxt
-         Just srcdir <- coreLift currentDir
-             | Nothing => throw (InternalError "Can't get current directory")
-         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.
@@ -100,17 +87,16 @@ findPkgDirs :
     PkgVersionBounds ->
     Core (List (String, Maybe PkgVersion))
 findPkgDirs p bounds = do
-  defs <- get Ctxt
-  globaldir <- globalPackageDir
-  localdir <- localPackageDir
+  globaldir <- pkgGlobalDirectory
+  localdir <- pkgLocalDirectory
 
   -- 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
+  d <- getDirs
+  pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) (package_dirs d)
 
   -- If there's anything locally, use that and ignore the global ones
   let allFiles = if isNil locFiles
@@ -142,7 +128,7 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
 addPkgDir p bounds = do
     Just p <- findPkgDir p bounds
         | Nothing => pure ()
-    addExtraDir p
+    addPackageDir p
 
 visiblePackages : String -> IO (List PkgDir)
 visiblePackages dir = filter viable <$> getPackageDirs dir
@@ -158,14 +144,13 @@ visiblePackages dir = filter viable <$> getPackageDirs dir
 findPackages : {auto c : Ref Ctxt Defs} -> Core (List PkgDir)
 findPackages
     = do -- global packages
-         defs <- get Ctxt
-         globalPkgs <- coreLift $ visiblePackages !globalPackageDir
+         globalPkgs <- coreLift $ visiblePackages !pkgGlobalDirectory
          -- additional packages in directories specified
-         let pkgDirs = (options defs).dirs.package_dirs
-         additionalPkgs <- coreLift $ traverse (\d => visiblePackages d) pkgDirs
+         d <- getDirs
+         additionalPkgs <- coreLift $ traverse (\d => visiblePackages d) (package_dirs d)
          -- local packages
-         localPkgs <- coreLift $ visiblePackages !localPackageDir
-         pure $ globalPkgs ++ (join additionalPkgs) ++ localPkgs
+         localPkgs <- coreLift $ visiblePackages !pkgLocalDirectory
+         pure $ globalPkgs ++ join additionalPkgs ++ localPkgs
 
 listPackages : {auto c : Ref Ctxt Defs} ->
                {auto o : Ref ROpts REPLOpts} ->

tests/Main.idr

@@ -261,7 +261,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        "eta001",
        -- Modules and imports
        "import001", "import002", "import003", "import004", "import005", "import006",
-       "import007",
+       "import007", "import008",
        -- Implicit laziness, lazy evaluation
        "lazy001", "lazy002",
        -- Namespace blocks

tests/chez/chez035/run

@@ -5,6 +5,6 @@ export IDRIS2_INC_CGS=chez
 $1 --no-banner --no-color --console-width 0 -o test Mod2.idr < input
 ./build/exec/test
 
-ls build/ttc/Mod1.so
+ls build/ttc/*/Mod1.so | sed -r "s/.([0-9]){10}//g"
 
 rm -rf build

tests/idris2/import008/Exe/Mod.idr

@@ -0,0 +1,6 @@
+module Mod
+
+import Conf
+
+main : IO ()
+main = putStrLn msg

tests/idris2/import008/Exe/depends/lib-0

@@ -0,0 +1 @@
+../../Lib/build/ttc/

tests/idris2/import008/Exe/exe.ipkg

@@ -0,0 +1,47 @@
+package exe
+-- version =
+-- authors =
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+depends = lib
+
+-- modules to install
+modules = Mod
+
+-- main file (i.e. file to load at REPL)
+-- main =
+
+-- name of executable
+-- executable =
+-- opts =
+-- sourcedir =
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =

tests/idris2/import008/Lib/Conf.idr

@@ -0,0 +1,7 @@
+module Conf
+
+%default total
+
+export
+msg : String
+msg = "hello world"

tests/idris2/import008/Lib/lib.ipkg

@@ -0,0 +1,47 @@
+package lib
+-- version =
+-- authors =
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+-- depends =
+
+-- modules to install
+modules = Conf
+
+-- main file (i.e. file to load at REPL)
+-- main =
+
+-- name of executable
+-- executable =
+-- opts =
+-- sourcedir =
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =

tests/idris2/import008/expected

@@ -0,0 +1,3 @@
+1/1: Building Conf (Conf.idr)
+1/1: Building Mod (Mod.idr)
+hello world

tests/idris2/import008/run

@@ -0,0 +1,9 @@
+rm -rf Exe/build
+rm -rf Lib/build
+
+cd Lib
+$1 --build
+cd ..
+cd Exe
+$1 --no-color --console-width 0 --no-banner --check --find-ipkg Mod.idr
+$1 --no-color --console-width 0 --no-banner --exec main --find-ipkg Mod.idr

tests/idris2/pkg010/run

@@ -11,7 +11,7 @@ export IDRIS2_PREFIX=${MY_PWD}currently/nonexistent/dir/
 
 export IDRIS2_INC_CGS=
 
-$1 --install ./testpkg.ipkg
+$1 --install ./testpkg.ipkg | sed -r "s/.([0-9]){10}//g"
 
 # ../ is there for some extra safety for using rm -rf
 rm -rf ../pkg010/build ../pkg010/currently

tests/idris2/reg043/NotFake.idr

@@ -0,0 +1 @@
+module NotFake

tests/idris2/reg043/expected

@@ -1,2 +1,3 @@
+1/1: Building NotFake (NotFake.idr)
 1/1: Building TestFake (TestFake.idr)
 Error: Error in TTC file: Corrupt TTC data for String (the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files)

tests/idris2/reg043/run

@@ -1,7 +1,7 @@
 rm -rf build
 
-mkdir -p build/ttc
-echo "TT2This Is A Fake TTC" > build/ttc/Fake.ttc
+$1 --no-color --console-width 0 --check NotFake.idr
+
+echo "TT2This Is A Fake TTC" > build/ttc/$(ls build/ttc)/Fake.ttc
 
 $1 --no-color --console-width 0 --check TestFake.idr
-

tests/idris2/total012/run

@@ -1,12 +1,12 @@
 rm -rf build
 
 $1 --no-color --console-width 0 Issue1828.idr --check
-$1 --no-color --console-width 0 Issue1828.idr --check --total --log totality.requirement:20
+$1 --no-color --console-width 0 Issue1828.idr --check --total --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g"
 
 $1 --no-color --console-width 0 Issue1828.idr --check
-$1 --no-color --console-width 0 Issue1828.idr --check --log totality.requirement:20
+$1 --no-color --console-width 0 Issue1828.idr --check --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g"
 
 
 $1 --no-color --console-width 0 TotallyTotal.idr --check
-$1 --no-color --console-width 0 TotallyTotal.idr --check --log totality.requirement:20
-$1 --no-color --console-width 0 TotallyTotal.idr --check --total --log totality.requirement:20
+$1 --no-color --console-width 0 TotallyTotal.idr --check --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g"
+$1 --no-color --console-width 0 TotallyTotal.idr --check --total --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g"

tests/templates/ttimp/run

@@ -1,5 +1,4 @@
 rm -rf build
 
 $1 --yaffle Interp.yaff < input
-$1 --yaffle build/ttc/Interp.ttc < input
-
+$1 --yaffle build/ttc/$(ls build/ttc/)/Interp.ttc < input

tests/ttimp/basic001/run

@@ -1,5 +1,4 @@
 rm -rf build
 
 $1 --yaffle Interp.yaff < input
-$1 --yaffle build/ttc/Interp.ttc < input
-
+$1 --yaffle build/ttc/*/Interp.ttc < input

tests/ttimp/basic003/run

@@ -1,5 +1,4 @@
 rm -rf build
 
 $1 --yaffle Hole.yaff < input
-$1 --yaffle build/ttc/Hole.ttc < input
-
+$1 --yaffle build/ttc/*/Hole.ttc < input

tests/ttimp/lazy001/run

@@ -2,5 +2,4 @@ rm -rf build
 
 $1 --yaffle Lazy.yaff < input
 $1 --yaffle LazyInf.yaff < input
-$1 --yaffle build/ttc/LazyInf.ttc < input
-
+$1 --yaffle build/ttc/*/LazyInf.ttc < input

tests/ttimp/record001/run

@@ -1,5 +1,4 @@
 rm -rf build
 
 $1 --yaffle Record.yaff < input
-$1 --yaffle build/ttc/Record.ttc < input
-
+$1 --yaffle build/ttc/*/Record.ttc < input

tests/ttimp/record003/run

@@ -1,5 +1,4 @@
 rm -rf build
 
-$1 --yaffle Record.yaff          < input
-$1 --yaffle build/ttc/Record.ttc < input
-
+$1 --yaffle Record.yaff < input
+$1 --yaffle build/ttc/*/Record.ttc < input

tests/ttimp/record004/run

@@ -1,4 +1,4 @@
 rm -rf build
 
-$1 --yaffle Record.yaff          < input
-$1 --yaffle build/ttc/Record.ttc < input
+$1 --yaffle Record.yaff < input
+$1 --yaffle build/ttc/*/Record.ttc < input