diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013-2014, Ranjit Jhala
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/liquid-platform.cabal b/liquid-platform.cabal
new file mode 100644
--- /dev/null
+++ b/liquid-platform.cabal
@@ -0,0 +1,59 @@
+cabal-version:      1.22
+name:               liquid-platform
+version:            0.8.10.1
+synopsis:           A battery-included platform for LiquidHaskell
+description:        A battery-included platform for LiquidHaskell.
+license:            BSD3
+license-file:       LICENSE
+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
+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
+
+flag devel
+  default:     False
+  manual:      True
+  description: turn on stricter error reporting for development
+
+executable liquidhaskell
+  main-is:            src/Liquid.hs
+  default-language:   Haskell2010
+  ghc-options:        -W -threaded
+  if impl(ghc < 8.10.1)
+    buildable: False
+  else
+    buildable: True
+    build-depends:      liquid-base       >= 4.14.0.0 && < 5
+                      , liquid-containers >= 0.6.2.1  && < 0.7
+                      , liquid-prelude    >= 0.8.10.1
+                      , liquid-vector     >= 0.12.1.2 && < 0.13
+                      , liquid-bytestring >= 0.10.0.0 && < 0.11
+                      , liquidhaskell     >= 0.8.10.1
+                      , process           >= 1.6.0.0 && < 1.7
+                      , cmdargs           >= 0.10    && < 0.11
+
+  if flag(devel)
+    ghc-options: -Werror
+
+executable gradual
+  main-is:          src/Gradual.hs
+  build-depends:    base            >= 4.8.1.0 && < 5
+                  , cmdargs
+                  , hscolour
+                  , liquid-fixpoint >= 0.7.0.5
+                  , liquidhaskell   >= 0.8.10.1
+  default-language: Haskell2010
+  buildable:        False
+  ghc-options:      -W -threaded
+
+  if flag(devel)
+    ghc-options: -Werror
+
+executable target
+  main-is:          src/Target.hs
+  build-depends:    base >= 4.8.1.0 && < 5, hint, liquidhaskell >= 0.8.10.1
+  default-language: Haskell2010
+  buildable:        False
+
diff --git a/src/Gradual.hs b/src/Gradual.hs
new file mode 100644
--- /dev/null
+++ b/src/Gradual.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE TupleSections #-}
+
+-- module Main where
+
+import Language.Haskell.Liquid.Liquid (liquidConstraints)
+
+import Language.Haskell.Liquid.Types (GhcInfo(..), Cinfo)
+import Language.Haskell.Liquid.Constraint.Types (CGInfo(..)) -- , FixWfC, SubC(..), CGEnv(..))
+import Language.Haskell.Liquid.UX.Config (Config(..))
+import Language.Haskell.Liquid.UX.CmdLine (getOpts)
+import Language.Haskell.Liquid.Constraint.ToFixpoint (cgInfoFInfo, fixConfig)
+
+import qualified Language.Fixpoint.Types as F
+import qualified Language.Fixpoint.Types.Config as F
+import           Language.Fixpoint.Solver       (simplifyFInfo)
+import           Language.Fixpoint.Solver.Solve (solve)
+import qualified Language.Fixpoint.Solver.GradualSolution as GS
+import           Language.Fixpoint.Misc         (mapSnd)
+import           Language.Fixpoint.Graph.Partition (partition')
+
+import System.Exit                    (exitWith, exitSuccess, exitFailure)
+import System.Environment             (getArgs)
+import System.Console.CmdArgs.Verbosity
+import Control.Monad (when)
+
+import qualified Data.List as L
+
+import Gradual.Concretize
+import Gradual.Types
+import Gradual.Misc (mapSndM, mapMWithLog)
+import Gradual.Uniquify
+import Gradual.Refinements
+import Gradual.PrettyPrinting
+import qualified Gradual.GUI as GUI
+import qualified Gradual.Trivial as T
+
+main :: IO a
+main = do
+  cfg <- getArgs >>= getOpts
+  css <- quietly $ liquidConstraints (cfg{gradual=True})
+  case css of
+    Left cgis -> mapM (runGradual (cfg{gradual=True})) cgis >> exitSuccess
+    Right e   -> exitWith e
+
+
+runGradual :: Config -> CGInfo -> IO [(GSub F.GWInfo,F.Result (Integer, Cinfo))]
+runGradual cfg cgi = do
+  let fname    = target (ghcI cgi)
+  let fcfg     = fixConfig fname cfg
+  finfo       <- quietly $ cgInfoFInfo (ghcI cgi) cgi
+  sinfo <- (uniquify . T.simplify) <$> (quietly $ simplifyFInfo fcfg finfo)
+  let (gsis, sis) = L.partition F.isGradual $ partition' Nothing (snd sinfo)
+  let gcfg     = (makeGConfig cfg) {pNumber = length gsis}
+  sol <- mconcat <$> (quietly $ mapM (solve fcfg) sis)
+  let gcfgs = setPId gcfg <$> [1..(length gsis)]
+  when (not $ F.isSafe sol) $ do
+    putStrLn "The static part cannot be satisfied: UNSAFE"
+    exitFailure
+  whenLoud $ putStrLn ("\nNumber of Gradual Partitions : " ++ show (length gsis) ++"\n")
+  solss <- mapMWithLog "Running Partition" (uncurry $ solveSInfo fcfg) (zip gcfgs gsis)
+  GUI.render gcfg (fst sinfo) solss
+  exitSuccess
+
+
+
+solveSInfo :: F.Config  -> GConfig -> F.SInfo Cinfo -> IO [GSub F.GWInfo]
+solveSInfo fcfg gcfg sinfo = do
+  gmap     <- makeGMap gcfg fcfg sinfo $ GS.init fcfg sinfo
+  let allgs = concretize gmap sinfo
+  putStrLn ("Total number of concretizations: " ++ show (length $ map snd allgs))
+  res   <- quietly $ mapM (mapSndM (solve fcfg)) allgs
+  case filter (F.isSafe . snd) res of
+    (x:xs) -> do putStrLn ( "["++ show (1 + length xs) ++ "/" ++ (show $ length res) ++ "] Solutions Found!" ++ if length xs > 0 then " e.g.," else "")
+                 putStrLn (pretty $ (map (mapSnd snd) $ fromGSub $ fst x))
+                 return (fst <$> (x:xs))
+    _     -> do putStrLn ("[0/" ++ (show $ length res) ++ "] Solutions. UNSAFE!\n")
+                whenLoud $ putStrLn ("UNSAFE PARTITION: " ++ show sinfo)
+                return [mempty]
+
+quietly :: IO a -> IO a
+quietly act = do
+  vb <- getVerbosity
+  setVerbosity Quiet
+  r  <- act
+  setVerbosity vb
+  return r
diff --git a/src/Liquid.hs b/src/Liquid.hs
new file mode 100644
--- /dev/null
+++ b/src/Liquid.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE LambdaCase #-}
+
+{-| Calling LiquidHaskell via the source plugin.
+  This executable is a simple wrapper around 'ghc', which gets passed an '-fplugin' option.
+-}
+
+import Control.Monad
+
+import System.Environment (lookupEnv, getArgs)
+import System.Process
+import System.Exit
+import Data.Maybe
+import Data.Either (partitionEithers)
+import Data.Bifunctor
+import Data.Functor ((<&>))
+import qualified System.Console.CmdArgs.Explicit as CmdArgs
+import Data.List (partition, isPrefixOf, (\\))
+
+import Language.Haskell.Liquid.UX.CmdLine (config, printLiquidHaskellBanner, getOpts)
+
+type GhcArg    = String
+type LiquidArg = String
+
+partitionArgs :: [String] -> ([GhcArg], [LiquidArg])
+partitionArgs args = partitionEithers (map parseArg args)
+  where
+    parseArg :: String -> Either GhcArg LiquidArg
+    parseArg a
+      | forwardToGhc a = Left a
+      | otherwise      = bimap (const a) (const a) (CmdArgs.process config [a])
+
+    -- Unfortunate consequence of the facts things like '-i' needs to be forwarded to GHC
+    -- and not the LH executable.
+    forwardToGhc :: String -> Bool
+    forwardToGhc = isPrefixOf "-i"
+
+
+helpNeeded :: [String] -> Bool
+helpNeeded = elem "--help"
+
+
+main :: IO a
+main = do
+
+  -- If no args are passed, display the help instead of ghc's "no input files." To do so,
+  -- due to the fact GHC needs to always have an input file to actually run a source plugin, we
+  -- run this with '--interactive'.
+  args <- getArgs <&> \case [] -> ["--interactive", "--help"]
+                            xs -> "--make" : xs
+
+  ghcPath <- fromMaybe "ghc" <$> lookupEnv "LIQUID_GHC_PATH"
+
+  -- Strip targets out of the arguments, so that we can forward them to GHC before they
+  -- get intercepted by the LH parser.
+  let (cliArgs, targets)    = partition (isPrefixOf "-") args
+  let (ghcArgs, liquidArgs) = partitionArgs cliArgs
+
+  -- NOTE: Typically for the executable we want to recompile everything-everytime so that
+  -- we could always get an "answer" out of LH. However, using `-fforce-recomp` as the default
+  -- is dangerous, because the executable is used also during tests, so runtime is going to be
+  -- badly affected. If users wants to enable recompilation, they would simply pass
+  -- '-fforce-recomp' as a CLI argument.
+
+  let p = proc ghcPath $ [ "-O0"
+                         , "-no-link"
+                         , "-fplugin=LiquidHaskell"
+                         , "-plugin-package", "liquidhaskell"
+                         , "-package", "liquid-ghc-prim"
+                         , "-package", "liquid-base"
+                         , "-package", "liquid-containers"
+                         , "-package", "liquid-prelude"
+                         , "-package", "liquid-vector"
+                         , "-package", "liquid-bytestring"
+                         , "-hide-package", "ghc-prim"
+                         , "-hide-package", "base"
+                         , "-hide-package", "containers"
+                         , "-hide-package", "vector"
+                         , "-hide-package", "bytestring"
+                         , "-fplugin-opt=LiquidHaskell:--normal" -- normal logging.
+                         ]
+                         <> map (mappend "-fplugin-opt=LiquidHaskell:") liquidArgs
+                         <> ghcArgs
+                         <> targets
+
+  -- Call into 'getOpts' so that things like the json reporter will correctly set the verbosity of the
+  -- logging and avoid printing the banner.
+  _ <- getOpts (args \\ ghcArgs)
+  unless (helpNeeded args) printLiquidHaskellBanner
+
+  withCreateProcess p $ \_mbStdIn _mbStdOut _mbStdErr pHandle -> waitForProcess pHandle >>= exitWith
diff --git a/src/Target.hs b/src/Target.hs
new file mode 100644
--- /dev/null
+++ b/src/Target.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE LambdaCase #-}
+-- module Main where
+
+import Language.Haskell.Interpreter
+import System.Environment
+import System.Exit
+import System.IO
+import Test.Target
+import Text.Printf
+
+main :: IO ()
+main = do
+  [src, binder] <- getArgs
+  r <- runInterpreter $ do
+    loadModules [src]
+    mods <- getLoadedModules
+    -- liftIO $ print mods
+    setImportsQ $ map (\m -> (m,Nothing)) mods
+                             ++ [("Test.Target", Nothing), ("Prelude", Nothing)]
+    set [languageExtensions := [TemplateHaskell]]
+    let expr = printf "$(targetResultTH '%s \"%s\")" binder src
+    -- liftIO $ putStrLn expr
+    interpret expr (as :: IO Result)
+  case r of
+    Left e -> hPrint stderr e >> exitWith (ExitFailure 2)
+    Right x -> x >>= \case
+      Errored e -> hPutStrLn stderr e >> exitWith (ExitFailure 2)
+      Failed s  -> printf "Found counter-example: %s\n" s >> exitWith (ExitFailure 1)
+      Passed n  -> printf "OK! Passed %d tests.\n" n >> exitSuccess