Run ready typed modules concurrently

1 files changed, 42 insertions, 8 deletions

diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index 682064a..aab23b7 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -29,12 +29,14 @@ import Data.ByteString qualified as ByteString
 import Data.Maybe (catMaybes)
 import Data.Text qualified as StrictText
 import Data.Text.IO qualified as Text
+import GHC.Conc qualified
 import Options.Applicative hiding (renderFailure)
 import System.Directory qualified as Directory
 import System.Environment (getArgs, lookupEnv)
 import System.Exit (ExitCode(..), exitWith)
 import System.FilePath.Posix qualified as Posix
 import System.IO (stderr)
+import Text.Read (readMaybe)
 
 
 newtype Input = Input
@@ -51,6 +53,7 @@ data VerificationOptions = VerificationOptions
     { verificationStoreSelection :: !Store.StoreSelection
     , verificationTimeLimit :: !Provers.TimeLimit
     , verificationMemoryLimit :: !Provers.MemoryLimit
+    , verificationJobsOverride :: !(Maybe Provers.EffectiveJobs)
     , verificationDumpDestination :: !(Maybe FilePath)
     , verificationHtmlRequested :: !Bool
     , verificationDiagnostics :: !VerificationDiagnostics
@@ -109,7 +112,7 @@ data ProverFailure
 data DumpObservationError
     = DumpDirectoryCreationFailed !FilePath !Text
     | DumpRequestWriteFailed
-        !VerificationRequestOrdinal
+        !WorkPosition
         !FilePath
         !Text
     deriving stock (Show, Eq)
@@ -282,22 +285,28 @@ runOpenVerification input options outputPlan store = do
                             WarmStoreValidation
                         Store.ExplicitStore{} ->
                             WarmStoreValidation
+            jobs <-
+                Provers.selectEffectiveJobs
+                    (verificationJobsOverride options)
+                    GHC.Conc.getNumProcessors
             observed <-
                 captureDumpFailure
                     (case verificationDiagnostics options of
                         QuietVerification ->
                             runNoLoggingT
-                                (verifyWithObserverAndStoreMode
+                                (verifyWithObserverAndStoreModeAndJobs
                                     store
                                     validationMode
+                                    jobs
                                     observer
                                     vampire
                                     (inputFilePath input))
                         LogVerification ->
                             runStderrLoggingT
-                                (verifyWithObserverAndStoreMode
+                                (verifyWithObserverAndStoreModeAndJobs
                                     store
                                     validationMode
+                                    jobs
                                     observer
                                     vampire
                                     (inputFilePath input)))
@@ -341,14 +350,18 @@ prepareRequestObserver = \case
 
 writeDumpRequest
     :: FilePath
-    -> VerificationRequestOrdinal
+    -> WorkPosition
     -> Provers.PreparedVerificationRequest
     -> IO ()
-writeDumpRequest root ordinal request = do
+writeDumpRequest root position request = do
     let destination =
             root
-                Posix.</> show
-                    (verificationRequestOrdinalValue ordinal)
+                Posix.</> ( show
+                            (workPositionModuleOrdinal position)
+                            <> "-"
+                            <> show
+                                (workPositionLocalRequestOrdinal position)
+                         )
                 Posix.<.> "p"
     result <- tryIOError
         (publishDumpFile
@@ -358,7 +371,7 @@ writeDumpRequest root ordinal request = do
         Left failure ->
             Exception.throwIO
                 (DumpRequestWriteFailed
-                    ordinal
+                    position
                     destination
                     (StrictText.pack
                         (displayException failure)))
@@ -640,6 +653,8 @@ verificationDriverFailureMessage = \case
             <> Store.renderStoreLifecycleError failure
     VerificationModuleArtifactKeyError{} ->
         "Typed module artifact inputs are inconsistent."
+    VerificationModuleSchedulerInvariant message ->
+        "Typed module scheduler invariant failed: " <> message
     VerificationFoundationManifestError{} ->
         "The fixed foundation manifest is invalid."
     VerificationMissingImportedModule address ->
@@ -775,6 +790,7 @@ data RawFileCommand = RawFileCommand
     , rawFresh :: !Bool
     , rawTimeLimit :: !(Maybe Provers.TimeLimit)
     , rawMemoryLimit :: !(Maybe Provers.MemoryLimit)
+    , rawJobs :: !(Maybe Provers.EffectiveJobs)
     , rawDump :: !(Maybe FilePath)
     , rawHtml :: !Bool
     , rawLogging :: !Bool
@@ -814,6 +830,7 @@ rawFileCommandParser =
                 <> help "Use a fresh temporary disposable store.")
         <*> optional timeLimitParser
         <*> optional memoryLimitParser
+        <*> optional jobsParser
         <*> optional
             (strOption
                 (long "dump"
@@ -884,6 +901,7 @@ validateRawCommand = \case
                             fromMaybe
                                 Provers.defaultMemoryLimit
                                 (rawMemoryLimit raw)
+                        , verificationJobsOverride = rawJobs raw
                         , verificationDumpDestination =
                             rawDump raw
                         , verificationHtmlRequested =
@@ -900,6 +918,7 @@ validateRawCommand = \case
                 , if rawFresh raw then Just "--fresh" else Nothing
                 , "--timelimit" <$ rawTimeLimit raw
                 , "--memlimit" <$ rawMemoryLimit raw
+                , "--jobs" <$ rawJobs raw
                 , "--dump" <$ rawDump raw
                 , if rawHtml raw then Just "--html" else Nothing
                 , if rawLogging raw then Just "--log" else Nothing
@@ -924,3 +943,18 @@ memoryLimitParser =
                 <> metavar "MB"
                 <> help "Memory limit for each Vampire process."
             )
+
+jobsParser :: Parser Provers.EffectiveJobs
+jobsParser =
+    option
+        (eitherReader parseJobs)
+        ( long "jobs"
+            <> short 'j'
+            <> metavar "JOBS"
+            <> help "Run at most JOBS module checkers and Vampire processes."
+        )
+  where
+    parseJobs raw =
+        case readMaybe raw >>= Provers.effectiveJobs of
+            Just jobs -> Right jobs
+            Nothing -> Left "JOBS must be a positive integer"