mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-11 08:37:35 +03:00
tweak how the prelude is loaded
This removes the `self-contained` flag, since it is fine for all builds to have the baked-in prelude as a last resort. Tinkerers can still change the prelude as long as it's in the search path. Also removes some unnecessary extra prelude loading by the Cryptol server by means of a new command
This commit is contained in:
parent
6203eedf3a
commit
4796b0a75a
5
Makefile
5
Makefile
@ -131,7 +131,7 @@ endif
|
||||
ifneq (,${PREFIX})
|
||||
PREFIX_ARG := --prefix=$(call adjust-path,${PREFIX_ABS})
|
||||
DESTDIR_ARG := --destdir=${PKG}
|
||||
CONFIGURE_ARGS := -f-relocatable -f-self-contained \
|
||||
CONFIGURE_ARGS := -f-relocatable \
|
||||
--docdir=$(call adjust-path,${PREFIX}/${PREFIX_SHARE}/${PREFIX_DOC}) \
|
||||
${SERVER_FLAG}
|
||||
else
|
||||
@ -141,8 +141,7 @@ else
|
||||
# `cabal copy` will make a mess in the PKG directory.
|
||||
PREFIX_ARG := --prefix=$(call adjust-path,${ROOT_PATH})
|
||||
DESTDIR_ARG := --destdir=${PKG}
|
||||
CONFIGURE_ARGS := -f-self-contained \
|
||||
--docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC}) \
|
||||
CONFIGURE_ARGS := --docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC}) \
|
||||
${SERVER_FLAG}
|
||||
endif
|
||||
|
||||
|
@ -58,6 +58,7 @@ data RCommand
|
||||
| RCExhaust Text
|
||||
| RCProve Text
|
||||
| RCSat Text
|
||||
| RCLoadPrelude
|
||||
| RCLoadModule FilePath
|
||||
| RCDecls
|
||||
| RCUnknownCmd Text
|
||||
@ -67,18 +68,19 @@ instance FromJSON RCommand where
|
||||
parseJSON = withObject "RCommand" $ \o -> do
|
||||
tag <- o .: "tag"
|
||||
flip (withText "tag") tag $ \case
|
||||
"evalExpr" -> RCEvalExpr <$> o .: "expr"
|
||||
"applyFun" -> RCApplyFun <$> o .: "handle" <*> o .: "arg"
|
||||
"typeOf" -> RCTypeOf <$> o .: "expr"
|
||||
"setOpt" -> RCSetOpt <$> o .: "key" <*> o .: "value"
|
||||
"check" -> RCCheck <$> o .: "expr"
|
||||
"exhaust" -> RCExhaust <$> o .: "expr"
|
||||
"prove" -> RCProve <$> o .: "expr"
|
||||
"sat" -> RCSat <$> o .: "expr"
|
||||
"loadModule" -> RCLoadModule . T.unpack <$> o .: "filePath"
|
||||
"browse" -> return RCDecls
|
||||
"exit" -> return RCExit
|
||||
unknown -> return (RCUnknownCmd unknown)
|
||||
"evalExpr" -> RCEvalExpr <$> o .: "expr"
|
||||
"applyFun" -> RCApplyFun <$> o .: "handle" <*> o .: "arg"
|
||||
"typeOf" -> RCTypeOf <$> o .: "expr"
|
||||
"setOpt" -> RCSetOpt <$> o .: "key" <*> o .: "value"
|
||||
"check" -> RCCheck <$> o .: "expr"
|
||||
"exhaust" -> RCExhaust <$> o .: "expr"
|
||||
"prove" -> RCProve <$> o .: "expr"
|
||||
"sat" -> RCSat <$> o .: "expr"
|
||||
"loadPrelude" -> return RCLoadPrelude
|
||||
"loadModule" -> RCLoadModule . T.unpack <$> o .: "filePath"
|
||||
"browse" -> return RCDecls
|
||||
"exit" -> return RCExit
|
||||
unknown -> return (RCUnknownCmd unknown)
|
||||
|
||||
newtype FunHandle = FH Int
|
||||
deriving (Eq, Ord, Enum, Bounded, Show)
|
||||
@ -214,7 +216,6 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
|
||||
#else
|
||||
where path' = splitSearchPath path
|
||||
#endif
|
||||
loadPrelude
|
||||
funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle)
|
||||
let handle err = reply rep (RRInteractiveError err (show (pp err)))
|
||||
loop = do
|
||||
@ -241,7 +242,16 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
|
||||
(m, _) <- io $ readIORef funHandles
|
||||
case Map.lookup fh m of
|
||||
Nothing -> reply rep (RRBadMessage "invalid function handle" (show fh))
|
||||
Just f -> reply rep (RRValue (f arg))
|
||||
Just f -> do
|
||||
case f arg of
|
||||
E.VFun g -> do
|
||||
gh <- io $ atomicModifyIORef' funHandles $ \(m', gh) ->
|
||||
let m'' = Map.insert gh g m'
|
||||
gh' = succ gh
|
||||
in ((m'', gh'), gh)
|
||||
-- TODO: bookkeeping to track the type of this value
|
||||
reply rep (RRFunValue gh T.tZero)
|
||||
val -> reply rep (RRValue val)
|
||||
RCTypeOf txt -> do
|
||||
expr <- replParseExpr (T.unpack txt)
|
||||
(_expr, _def, sch) <- replCheckExpr expr
|
||||
@ -277,6 +287,9 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
|
||||
reply rep (RRProverError err)
|
||||
_ ->
|
||||
reply rep (RRProverError "unexpected prover result")
|
||||
RCLoadPrelude -> do
|
||||
loadPrelude
|
||||
reply rep RROk
|
||||
RCLoadModule fp -> do
|
||||
loadCmd fp
|
||||
reply rep RROk
|
||||
|
@ -33,10 +33,6 @@ flag relocatable
|
||||
default: True
|
||||
description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.
|
||||
|
||||
flag self-contained
|
||||
default: True
|
||||
description: Compile the text of the Cryptol Prelude into the library
|
||||
|
||||
flag server
|
||||
default: False
|
||||
description: Build with the ZeroMQ/JSON cryptol-server executable
|
||||
@ -56,6 +52,7 @@ library
|
||||
gitrev >= 1.0,
|
||||
generic-trie >= 0.3.0.1,
|
||||
GraphSCC >= 1.0.4,
|
||||
heredoc >= 0.2,
|
||||
monadLib >= 3.7.2,
|
||||
old-time >= 1.1,
|
||||
presburger >= 1.3,
|
||||
@ -176,10 +173,6 @@ library
|
||||
if flag(relocatable)
|
||||
cpp-options: -DRELOCATABLE
|
||||
|
||||
if flag(self-contained)
|
||||
build-depends: heredoc >= 0.2
|
||||
cpp-options: -DSELF_CONTAINED
|
||||
|
||||
executable cryptol
|
||||
Default-language:
|
||||
Haskell98
|
||||
|
@ -27,6 +27,7 @@ import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.Utils.PP (NameDisp)
|
||||
|
||||
import Control.Monad (guard)
|
||||
import qualified Control.Exception as X
|
||||
import Data.Foldable (fold)
|
||||
import Data.Function (on)
|
||||
import qualified Data.Map as Map
|
||||
@ -82,7 +83,11 @@ initialModuleEnv = do
|
||||
#endif
|
||||
binDir <- takeDirectory `fmap` getExecutablePath
|
||||
let instDir = normalise . joinPath . init . splitPath $ binDir
|
||||
userDir <- getAppUserDataDirectory "cryptol"
|
||||
-- looking up this directory can fail if no HOME is set, as in some
|
||||
-- CI settings
|
||||
let handle :: X.IOException -> IO String
|
||||
handle _e = return ""
|
||||
userDir <- X.catch (getAppUserDataDirectory "cryptol") handle
|
||||
return ModuleEnv
|
||||
{ meLoadedModules = mempty
|
||||
, meNameSeeds = T.nameSeeds
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
--
|
||||
-- Include the prelude when building with -fself-contained
|
||||
-- Compile the prelude into the executable as a last resort
|
||||
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
@ -16,8 +16,6 @@ module Cryptol.Prelude (writePreludeContents) where
|
||||
|
||||
import Cryptol.ModuleSystem.Monad
|
||||
|
||||
#ifdef SELF_CONTAINED
|
||||
|
||||
import System.Directory (getTemporaryDirectory)
|
||||
import System.IO (hClose, hPutStr, openTempFile)
|
||||
import Text.Heredoc (there)
|
||||
@ -33,14 +31,5 @@ writePreludeContents = io $ do
|
||||
(path, h) <- openTempFile tmpdir "Cryptol.cry"
|
||||
hPutStr h preludeContents
|
||||
hClose h
|
||||
print $ "Wrote Prelude to " ++ path
|
||||
return path
|
||||
|
||||
#else
|
||||
|
||||
import Cryptol.Utils.Ident (preludeName)
|
||||
|
||||
-- | If we're not self-contained, the Prelude is just missing
|
||||
writePreludeContents :: ModuleM FilePath
|
||||
writePreludeContents = moduleNotFound preludeName =<< getSearchPath
|
||||
|
||||
#endif
|
||||
|
Loading…
Reference in New Issue
Block a user