Merge pull request ucsd-progsys#1706 from ucsd-progsys/adinapoli/liqu…

…id-dev-mode Liquid-Dev-Mode prototype
YoshikiTakashima · Jul 21, 2020 · a4fa7a2 · a4fa7a2
2 parents 3eec22c + 6962f29
commit a4fa7a2
Show file tree

Hide file tree

Showing 17 changed files with 141 additions and 7 deletions.
diff --git a/docs/mkDocs/docs/develop.md b/docs/mkDocs/docs/develop.md
@@ -2,6 +2,53 @@
 
 Here are some notes that are generally useful for people *developing* LH itself.
 
+## Fast (re)compilation
+
+When working on the `liquidhaskell` library, usually all we want is to make changes and quickly recompile
+only the bare minimum, to try out new ideas. Using a fully-fledged GHC plugin doesn't help in this sense,
+because packages like `liquid-base` or `liquid-ghc-prim` all have a direct dependency on `liquidhaskell`, and
+therefore every time the latter changes, an expensive rebuild of those packages is triggered, which
+might become tedious overtime. To mitigate this, we offer a faster, "dev-style" build mode which is based
+on the assumption that most changes to the `liquidhaskell` library do not alter the validity of
+already-checked libraries, and therefore things like `liquid-base` and `liquid-ghc-prim` can be considered
+"static assets", avoiding the need for a recompilation. In other terms, we explicitly disable recompilation
+of any of the `liquid-*` ancillary library in dev mode, so that rebuilds would also influence the 
+`liquidhaskell` library.
+
+### Usage and recommended workflow
+
+This is how you can use this:
+
+* To begin with, perform a **full** build of **all** the libraries, by doing either `cabal v2-build` or `stack build`,
+  **without** specifying any extra environment variables from the command line. This is needed to ensure that
+  we things like `liquid-base` and `liquid-ghc-prim` are compiled at least once, as we would need the
+  refinements they contain to correctly checks other downstream programs;
+
+* At this point, the content of the `liquid-*` packages is considered "trusted" and "frozen", until you won't
+  force another full, _non-dev_ build;
+
+* In order to quickly test changes to the `liquidhaskell` library without recompiling the `liquid-*` packages,
+  we need to start a build passing the `LIQUID_DEV_MODE` env var as part of the build command. Examples:
+
+#### Stack
+
+```
+LIQUID_DEV_MODE=true stack build
+```
+
+#### Cabal
+
+```
+LIQUID_DEV_MODE=true cabal v2-build
+```
+
+It's also possible (but not recommended) to add `LIQUID_DEV_MODE` to .bashrc or similar, but this would
+permanently disable building the `liquid-*` packages, and this might silently mask breaking changes to the
+`liquidhaskell` library that would manifest only when compiling these other packages.
+
+If you wish to force building all the libraries again, it's sufficient to issue the same builds commands 
+without the `LIQUID_DEV_MODE`.
+
 ## How To Run Regression Tests
 
 You can run all the tests by

diff --git a/liquid-base/Setup.hs b/liquid-base/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-base/liquid-base.cabal b/liquid-base/liquid-base.cabal
@@ -9,7 +9,7 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
 data-files:         src/Data/*.spec
@@ -22,6 +22,9 @@ data-files:         src/Data/*.spec
                     src/Foreign/*.spec
                     src/Control/*.spec
 
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:  Control.Applicative
                     Control.Arrow

diff --git a/liquid-bytestring/Setup.hs b/liquid-bytestring/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-bytestring/liquid-bytestring.cabal b/liquid-bytestring/liquid-bytestring.cabal
@@ -9,7 +9,7 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
 data-files:           src/Data/ByteString.spec
@@ -19,6 +19,9 @@ data-files:           src/Data/ByteString.spec
                       src/Data/ByteString/Char8.spec
                       src/Data/ByteString/Lazy/Char8.spec
 
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:    Data.ByteString
                       Data.ByteString.Char8

diff --git a/liquid-containers/Setup.hs b/liquid-containers/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-containers/liquid-containers.cabal b/liquid-containers/liquid-containers.cabal
@@ -9,11 +9,14 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
 data-files:           src/Data/Set.spec
 
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:    Data.Containers.ListUtils
                       Data.IntMap

diff --git a/liquid-ghc-prim/Setup.hs b/liquid-ghc-prim/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-ghc-prim/liquid-ghc-prim.cabal b/liquid-ghc-prim/liquid-ghc-prim.cabal
@@ -9,11 +9,15 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
 data-files:         src/GHC/*.spec
 
+
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:
                     -- We can't really export 'GHC.Prim' or this won't build on Windows,

diff --git a/liquid-parallel/Setup.hs b/liquid-parallel/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-parallel/liquid-parallel.cabal b/liquid-parallel/liquid-parallel.cabal
@@ -9,11 +9,14 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
 data-files:           src/Control/Parallel/Strategies.spec
 
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:    Control.Seq
                       Control.Parallel

diff --git a/liquid-prelude/Setup.hs b/liquid-prelude/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-prelude/liquid-prelude.cabal b/liquid-prelude/liquid-prelude.cabal
@@ -9,9 +9,12 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:  Language.Haskell.Liquid.RTick
                     Language.Haskell.Liquid.Prelude

diff --git a/liquid-vector/Setup.hs b/liquid-vector/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-vector/liquid-vector.cabal b/liquid-vector/liquid-vector.cabal
@@ -9,11 +9,14 @@ author:             Ranjit Jhala, Niki Vazou, Eric Seidel
 maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
-build-type:         Simple
+build-type:         Custom
 cabal-version:      >= 1.22
 
 data-files:           src/Data/Vector.spec
 
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
 library
   exposed-modules:    Data.Vector.Internal.Check
                       Data.Vector.Fusion.Util

diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
@@ -91,6 +91,7 @@ library
                       Gradual.Trivial
                       Gradual.Types
                       Gradual.Uniquify
+                      Language.Haskell.Liquid.Cabal
                       Language.Haskell.Liquid.Bare
                       Language.Haskell.Liquid.Bare.Axiom
                       Language.Haskell.Liquid.Bare.Check
@@ -207,6 +208,7 @@ library
                     , aeson
                     , binary
                     , bytestring           >= 0.10
+                    , Cabal                < 3.3
                     , cereal
                     , cmdargs              >= 0.10
                     , containers           >= 0.5

diff --git a/src/Language/Haskell/Liquid/Cabal.hs b/src/Language/Haskell/Liquid/Cabal.hs
@@ -0,0 +1,21 @@
+{- | This module provides a drop-in replacement for Cabal's 'defaultMain', to be used inside 'Setup.hs'
+     modules of packages that wants to use the \"dev mode\". For more information, visit the documentation,
+     especially the \"Developers' guide\".
+-}
+
+{-# LANGUAGE LambdaCase #-}
+module Language.Haskell.Liquid.Cabal (liquidHaskellMain) where
+
+import Distribution.Simple
+import System.Environment
+
+liquidHaskellMain :: IO ()
+liquidHaskellMain = do
+  mbDevMode <- lookupEnv "LIQUID_DEV_MODE"
+  defaultMainWithHooks (devModeHooks mbDevMode)
+
+devModeHooks :: Maybe String -> UserHooks
+devModeHooks = \case
+  Nothing               -> simpleUserHooks
+  Just x | x == "false" -> simpleUserHooks
+  Just _                -> simpleUserHooks { buildHook = \_ _ _ _ -> return () }