Add --ignore-missing-ipkg flag

When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.

We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!

libs/base/base.ipkg

@@ -1,6 +1,8 @@
 package base
 version = 0.3.0
 
+opts = "--ignore-missing-ipkg"
+
 modules = Control.App,
           Control.App.Console,
           Control.App.FileIO,

libs/contrib/contrib.ipkg

@@ -1,6 +1,8 @@
 package contrib
 version = 0.3.0
 
+opts = "--ignore-missing-ipkg"
+
 modules = Control.ANSI,
           Control.ANSI.SGR,
           Control.ANSI.CSI,

libs/network/network.ipkg

@@ -1,7 +1,7 @@
 package network
 version = 0.3.0
 
-opts = "-p contrib"
+opts = "--ignore-missing-ipkg -p contrib"
 
 modules = Control.Linear.Network,
 

libs/prelude/prelude.ipkg

@@ -1,7 +1,7 @@
 package prelude
 version = 0.3.0
 
-opts = "--no-prelude"
+opts = "--ignore-missing-ipkg --no-prelude"
 
 modules = Builtin,
           PrimIO,

src/Core/Options.idr

@@ -135,6 +135,9 @@ record Session where
   directives : List String
   logLevel : LogLevels
   logTimings : Bool
+  ignoreMissingPkg : Bool -- fail silently on missing packages. This is because
+          -- while we're bootstrapping, we find modules by a different route
+          -- but we still want to have the dependencies listed properly
   debugElabCheck : Bool -- do conversion check to verify results of elaborator
   dumpcases : Maybe String -- file to output compiled case trees
   dumplifted : Maybe String -- file to output lambda lifted definitions
@@ -186,7 +189,7 @@ defaultPPrint = MkPPOpts False True False
 export
 defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
-                               False False Nothing Nothing
+                               False False False Nothing Nothing
                                Nothing Nothing
 
 export

src/Idris/CommandLine.idr

@@ -163,6 +163,7 @@ data CLOpt
   DumpVMCode String |
    ||| Run a REPL command then exit immediately
   RunREPL String |
+  IgnoreMissingIPKG |
   FindIPKG |
   Timing |
   DebugElabCheck |
@@ -264,7 +265,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
            MkOpt ["--repl"] [Required "package file"] (\f => [Package REPL f])
               (Just "Build the given package and launch a REPL instance."),
            MkOpt ["--find-ipkg"] [] [FindIPKG]
-              (Just "Find and use an .ipkg file in a parent directory"),
+              (Just "Find and use an .ipkg file in a parent directory."),
+           MkOpt ["--ignore-missing-ipkg"] [] [IgnoreMissingIPKG]
+              (Just "Fail silently if a dependency is missing."),
 
            optSeparator,
            MkOpt ["--ide-mode"] [] [IdeMode]

src/Idris/Driver.idr

@@ -74,8 +74,9 @@ updateEnv
          -- for the tests means they test the local version not the installed
          -- version
          defs <- get Ctxt
-         addPkgDir "prelude" anyBounds
-         addPkgDir "base" anyBounds
+         -- These might fail while bootstrapping
+         catch (addPkgDir "prelude" anyBounds) (const (pure ()))
+         catch (addPkgDir "base" anyBounds) (const (pure ()))
          addDataDir (prefix_dir (dirs (options defs)) </>
                         ("idris2-" ++ showVersion False version) </> "support")
          addLibDir (prefix_dir (dirs (options defs)) </>
@@ -110,6 +111,11 @@ tryYaffle (Yaffle f :: _) = do yaffleMain f []
                                pure True
 tryYaffle (c :: cs) = tryYaffle cs
 
+ignoreMissingIpkg : List CLOpt -> Bool
+ignoreMissingIpkg [] = False
+ignoreMissingIpkg (IgnoreMissingIPKG :: _) = True
+ignoreMissingIpkg (c :: cs) = ignoreMissingIpkg cs
+
 tryTTM : List CLOpt -> Core Bool
 tryTTM [] = pure False
 tryTTM (Metadata f :: _) = do dumpTTM f
@@ -145,6 +151,9 @@ stMain cgs opts
          addPrimitives
 
          setWorkingDir "."
+         when (ignoreMissingIpkg opts) $
+            setSession (record { ignoreMissingPkg = True } !getSession)
+
          updateEnv
          let ide = ideMode opts
          let ideSocket = ideModeSocket opts

src/Idris/Package.idr

@@ -360,9 +360,10 @@ prepareCompilation : {auto c : Ref Ctxt Defs} ->
 prepareCompilation pkg opts =
   do
     defs <- get Ctxt
-    addDeps pkg
 
     processOptions (options pkg)
+    addDeps pkg
+
     ignore $ preOptions opts
 
     runScript (prebuild pkg)

src/Idris/SetOptions.idr

@@ -93,7 +93,9 @@ addPkgDir p bounds
          -- If there's none, report it
          -- (TODO: Can't do this quite yet due to idris2 build system...)
          case sorted of
-              [] => throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
+              [] => if defs.options.session.ignoreMissingPkg
+                       then pure ()
+                       else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
               ((p, _) :: ps) => addExtraDir p
 
 dirOption : Dirs -> DirCommand -> Core ()
@@ -174,6 +176,9 @@ preOptions (RunREPL _ :: opts)
 preOptions (FindIPKG :: opts)
     = do setSession (record { findipkg = True } !getSession)
          preOptions opts
+preOptions (IgnoreMissingIPKG :: opts)
+    = do setSession (record { ignoreMissingPkg = True } !getSession)
+         preOptions opts
 preOptions (DumpCases f :: opts)
     = do setSession (record { dumpcases = Just f } !getSession)
          preOptions opts