Merge pull request #2564 from ucsd-progsys/fd/cores-default

Make using a single core the default

Author: facundominguez

CHANGES.md

@@ -2,6 +2,8 @@
 
 ## Next
 
+- Change `--cores` default to 1 [#2564](https://github.com/ucsd-progsys/liquidhaskell/pull/2564)
+
 ## 0.9.12.2 (2025-03-22)
 
 - Simplify kvar solutions in fqout files [liquid-fixpoint#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741).

README.md

@@ -148,7 +148,8 @@ Then a csv report can be generated from this json files with
 ```
 cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskell -o summary.csv
 ```
-On each line, the report will contain the time taken by each test.
+On each line, the report will contain the the wall-clock time taken by each test.
+Use `--phase LiquidHaskellCPU` to get the CPU time instead.
 
 Comparison charts in `svg` format can be generated by invoking
 

benchmark-timings/app/Main.hs

@@ -17,7 +17,7 @@ import Data.Traversable (for)
 import Data.Maybe (catMaybes)
 
 import Data.ByteString.Lazy.Char8 (writeFile)
-import Data.List (foldl', intersperse, isSuffixOf)
+import Data.List (intersperse, isSuffixOf)
 import qualified Text.ParserCombinators.ReadP as ReadP
 
 data Phase = Phase

liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs

@@ -24,8 +24,14 @@ module Liquid.GHC.API.Extra (
   , thisPackage
   , tyConRealArity
   , untick
+  , withTimingWallClock
   ) where
 
+import Control.Monad
+import Control.Monad.IO.Class
+import GHC.Conc (getAllocationCounter)
+import Debug.Trace
+import GHC.Clock (getMonotonicTimeNSec)
 import           Liquid.GHC.API.StableModule      as StableModule
 import GHC hiding (modInfoLookupName)
 import Data.Data (Data, gmapQr, gmapT)
@@ -51,7 +57,10 @@ import GHC.Types.Name.Reader          (nameRdrName)
 import GHC.Types.SrcLoc               as Ghc
 import GHC.Types.Unique               (getUnique, hasKey)
 
+import GHC.Utils.Error                as Ghc
+import GHC.Utils.Logger               as Ghc
 import GHC.Utils.Outputable           as Ghc hiding ((<>))
+import qualified GHC.Utils.Outputable as Ghc
 
 import GHC.Unit.Module
 
@@ -263,3 +272,72 @@ untick e = e
 
 minus_RDR :: RdrName
 minus_RDR = nameRdrName minusName
+
+-- | A version of 'withTiming' that uses wall clock time instead of CPU time.
+--
+-- This version is copied and modified from GHC's 'GHC.Utils.Error.withTiming'
+withTimingWallClock :: MonadIO m
+           => Logger
+           -> SDoc         -- ^ The name of the phase
+           -> (a -> ())    -- ^ A function to force the result
+                           -- (often either @const ()@ or 'rnf')
+           -> m a          -- ^ The body of the phase to be timed
+           -> m a
+withTimingWallClock logger what force_result action =
+    if logVerbAtLeast logger 2 || logHasDumpFlag logger Opt_D_dump_timings
+    then do when printTimingsNotDumpToFile $ liftIO $
+              logInfo logger $ withPprStyle defaultUserStyle $
+                text "***" <+> what Ghc.<> colon
+            let ctx = log_default_user_context (logFlags logger)
+            alloc0 <- liftIO getAllocationCounter
+            !start <- liftIO getMonotonicTimeNSec
+            eventBegins ctx what
+            recordAllocs alloc0
+            !r <- action
+            () <- pure $ force_result r
+            eventEnds ctx what
+            !end <- liftIO getMonotonicTimeNSec
+            alloc1 <- liftIO getAllocationCounter
+            recordAllocs alloc1
+            -- recall that allocation counter counts down
+            let alloc = alloc0 - alloc1
+                time = (end - start) `div` 1000000
+
+            when (logVerbAtLeast logger 2 && printTimingsNotDumpToFile)
+                $ liftIO $ logInfo logger $ withPprStyle defaultUserStyle
+                    (text "!!!" <+> what Ghc.<> colon <+> text "finished in"
+                     <+> word64 time
+                     <+> text "milliseconds"
+                     Ghc.<> comma
+                     <+> text "allocated"
+                     <+> doublePrec 3 (realToFrac alloc / 1024 / 1024)
+                     <+> text "megabytes")
+
+            liftIO $ putDumpFileMaybe logger Opt_D_dump_timings "" FormatText
+                    $ text $ showSDocOneLine ctx
+                    $ hsep [ what Ghc.<> colon
+                           , text "alloc=" Ghc.<> ppr alloc
+                           , text "time=" Ghc.<> word64 time
+                           ]
+            pure r
+     else action
+
+    where -- Avoid both printing to console and dumping to a file (#20316).
+          printTimingsNotDumpToFile =
+            not (log_dump_to_file (logFlags logger))
+
+          recordAllocs alloc =
+            liftIO $ traceMarkerIO $ "GHC:allocs:" ++ show alloc
+
+          eventBegins ctx w = do
+            let doc = eventBeginsDoc ctx w
+            liftIO $ traceMarkerIO doc
+            liftIO $ traceEventIO doc
+
+          eventEnds ctx w = do
+            let doc = eventEndsDoc ctx w
+            liftIO $ traceMarkerIO doc
+            liftIO $ traceEventIO doc
+
+          eventBeginsDoc ctx w = showSDocOneLine ctx $ text "GHC:started:" <+> w
+          eventEndsDoc   ctx w = showSDocOneLine ctx $ text "GHC:finished:" <+> w

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs

@@ -33,7 +33,6 @@ module Language.Haskell.Liquid.GHC.Interface (
   , modSummaryHsFile
   , makeFamInstEnv
   , clearSpec
-  , checkFilePragmas
   , lookupTyThing
   , updLiftedSpec
   ) where
@@ -50,7 +49,6 @@ import           Liquid.GHC.API as Ghc hiding ( text
                                                                )
 import qualified Liquid.GHC.API as Ghc
 
-import Control.Exception
 import Control.Monad
 import Control.Monad.Trans.Maybe
 
@@ -61,7 +59,6 @@ import qualified Data.HashSet        as S
 
 import Text.PrettyPrint.HughesPJ        hiding (first, (<>))
 import Language.Fixpoint.Types          hiding (err, panic, Error, Result, Expr)
-import qualified Language.Fixpoint.Misc as Misc
 import Language.Haskell.Liquid.GHC.Misc
 import Language.Haskell.Liquid.GHC.Types (MGIModGuts(..))
 import Language.Haskell.Liquid.GHC.Play
@@ -152,19 +149,6 @@ modSummaryHsFile modSummary =
       showPpr (ms_mod modSummary))
     (ml_hs_file $ ms_location modSummary)
 
-checkFilePragmas :: [Located String] -> IO ()
-checkFilePragmas = Misc.applyNonNull (return ()) throw . mapMaybe err
-  where
-    err pragma
-      | check (val pragma) = Just (ErrFilePragma $ fSrcSpan pragma :: Error)
-      | otherwise          = Nothing
-    check pragma           = any (`isPrefixOf` pragma) bad
-    bad =
-      [ "-i", "--idirs"
-      , "-g", "--ghc-option"
-      , "--c-files", "--cfiles"
-      ]
-
 --------------------------------------------------------------------------------
 -- | Family instance information
 --------------------------------------------------------------------------------

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs

@@ -132,7 +132,10 @@ plugin = GHC.defaultPlugin {
     typecheckPluginGo cfg summary gblEnv = do
       logger <- getLogger
       dynFlags <- getDynFlags
-      withTiming logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do
+      GHC.withTiming
+          logger (text "LiquidHaskellCPU" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $
+        GHC.withTimingWallClock
+          logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do
         if gopt Opt_Haddock dynFlags
           then do
             -- Warn the user
@@ -300,15 +303,14 @@ typecheckHook' cfg ms tcGblEnv specComments = do
 
 liquidCheckModule :: Config -> ModSummary -> TcGblEnv -> [BPspec] -> TcM (Either LiquidCheckException TcGblEnv)
 liquidCheckModule cfg0 ms tcg specs = do
-  withPragmas cfg0 thisFile pragmas $ \cfg -> do
+  withPragmas cfg0 pragmas $ \cfg -> do
     pipelineData <- do
       env <- getTopEnv
       session <- Session <$> liftIO (newIORef env)
       liftIO $ flip reflectGhc session $ mkPipelineData ms tcg specs
     liquidLib <- setGblEnv tcg $ liquidHaskellCheckWithConfig cfg pipelineData ms
     traverse (serialiseSpec tcg) liquidLib
   where
-    thisFile = LH.modSummaryHsFile ms
     pragmas = [ s | Pragma s <- specs ]
 
 mkPipelineData :: (GhcMonad m) => ModSummary -> TcGblEnv -> [BPspec] -> m PipelineData
@@ -412,10 +414,10 @@ checkLiquidHaskellContext lhContext = do
       out <- liftIO $ LH.checkTargetInfo pmrTargetInfo
 
       let bareSpec = lhInputSpec lhContext
-          file = LH.modSummaryHsFile $ lhModuleSummary lhContext
 
-      withPragmas (lhGlobalCfg lhContext) file (Ms.pragmas bareSpec) $ \moduleCfg ->  do
+      withPragmas (lhGlobalCfg lhContext) (Ms.pragmas bareSpec) $ \moduleCfg ->  do
         let filters = getFilters moduleCfg
+            file = LH.modSummaryHsFile $ lhModuleSummary lhContext
         -- Report the outcome of the checking
         LH.reportResult (errorLogger file filters) moduleCfg [giTarget (giSrc pmrTargetInfo)] out
         -- If there are unmatched filters or errors, and we are not reporting with
@@ -500,14 +502,8 @@ processModule LiquidHaskellContext{..} = do
   debugLog ("Module ==> " ++ renderModule thisModule)
 
   let bareSpec0       = lhInputSpec
-  -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise
-  -- this won't trigger the \"external name resolution\" as part of 'Language.Haskell.Liquid.Bare.Resolve'
-  -- (cfr. 'allowExtResolution').
-  let file            = LH.modSummaryHsFile lhModuleSummary
-
-  _                   <- liftIO $ LH.checkFilePragmas $ Ms.pragmas bareSpec0
 
-  withPragmas lhGlobalCfg file (Ms.pragmas bareSpec0) $ \moduleCfg -> do
+  withPragmas lhGlobalCfg (Ms.pragmas bareSpec0) $ \moduleCfg -> do
     dependencies <- loadDependencies moduleCfg lhRelevantModules
 
     debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:"
@@ -520,6 +516,7 @@ processModule LiquidHaskellContext{..} = do
     hscEnv <- getTopEnv
     let preNormalizedCore = preNormalizeCore moduleCfg modGuts0
         modGuts = modGuts0 { mg_binds = preNormalizedCore }
+        file = LH.modSummaryHsFile lhModuleSummary
     targetSrc  <- liftIO $ makeTargetSrc moduleCfg file modGuts hscEnv
     logger <- getLogger