Fixes #172

There's now a more sensible hierarchy of locations that Cryptol uses to
look for modules. By default, in order it looks for libraries in:

1. The directories specified in the CRYPTOLPATH environment variable
2. The current directory
3. The user data directory (something like `$HOME/.cryptol`)
4. Relative to the executable's install directory
5. The static path used when building the executable (cabal's data-dir)

There is also a new command-line flag for the interpreter:
`--cryptolpath-only` which makes the interpreter ignore locations 2-5.

This commit also reworks the Makefile and build/release process. These
are bunched together because they play off each other quite a bit; the
build/release process determines the location of the `Cryptol.cry`,
which must be found when looking for modules.

Rather than leaning on `cabal install`, we now use a combination of
`cabal configure`, `cabal build`, and `cabal copy`. A couple of upshots
to this:

- More of the release staging is handled by cabal -- we don't have to go
  in and manually copy things out of the sandbox. In fact, the `cryptol`
  executable never goes into the sandbox.

- The testing infrastructure runs on executables that are in place in
  the staging directory, rather than in the sandbox. This should be more
  hygienic and realistic.

- The `Cryptol.cry` prelude file is now in `/share/cryptol` in order to
  better reflect the common POSIX structure. This means Cryptol will
  play nicer in global installs, and mirrors what other interpreted
  languages do.

- The default build settings use a prefix of `/usr/local` rather than
  using the sandbox directory. This makes them more relocatable for
  binary distributions. Set PREFIX= before making to change this.

Makefile

@@ -4,12 +4,14 @@ ARCH    := $(shell uname -m)
 TESTS ?= issues regression renamer mono-binds
 TEST_DIFF ?= meld
 
-CABAL_FLAGS ?= -j
+CABAL_BUILD_FLAGS   ?= -j
+CABAL_INSTALL_FLAGS ?= $(CABAL_BUILD_FLAGS)
 
-CABAL_EXE   := cabal
-CABAL       := $(CABAL_EXE) $(CABAL_FLAGS)
-CS          := ./.cabal-sandbox
-CS_BIN      := $(CS)/bin
+CABAL         := cabal
+CABAL_BUILD   := $(CABAL) build $(CABAL_BUILD_FLAGS)
+CABAL_INSTALL := $(CABAL) install $(CABAL_INSTALL_FLAGS)
+CS            := ./.cabal-sandbox
+CS_BIN        := $(CS)/bin
 
 # Used only for windows, to find the right Program Files.
 PROGRAM_FILES = Program\ Files\ \(x86\)
@@ -29,14 +31,35 @@ ifneq (,$(findstring _NT,${UNAME}))
   DIST := ${PKG}.msi
   EXE_EXT := .exe
   adjust-path = '$(shell cygpath -w $1)'
+  PREFIX ?= ${PROGRAM_FILES}/Galois/Cryptol\ ${VERSION}
+  # split this up because `cabal copy` strips drive letters
+  PREFIX_ABS    := /cygdrive/c/${PREFIX}
+  # since Windows installs aren't overlapping like /usr/local, we
+  # don't need this extra prefix
+  PREFIX_SHARE  :=
+  # goes under the share prefix
+  PREFIX_DOC    := /doc
+  PKG_PREFIX    := ${PKG}/${PREFIX}
 else
   DIST := ${PKG}.tar.gz ${PKG}.zip
   EXE_EXT :=
   adjust-path = '$1'
+  PREFIX ?= /usr/local
+  PREFIX_ABS := ${PREFIX}
+  PREFIX_SHARE := /share
+  # goes under the share prefix
+  PREFIX_DOC   := /doc/cryptol
+  PKG_PREFIX    := ${PKG}${PREFIX}
 endif
 
+CRYPTOL_EXE := ./dist/build/cryptol/cryptol${EXE_EXT}
+
 .PHONY: all
-all: ${CS_BIN}/cryptol
+all: ${CRYPTOL_EXE}
+
+.PHONY: run
+run: ${CRYPTOL_EXE}
+	CRYPTOLPATH=$(call adjust-path,$(CURDIR)/lib) ${CRYPTOL_EXE}
 
 .PHONY: docs
 docs:
@@ -54,56 +77,79 @@ zip: ${PKG}.zip
 .PHONY: msi
 msi: ${PKG}.msi
 
+# TODO: piece this apart a bit more; if right now if something fails
+# during initial setup, you have to invoke this target again manually
 ${CS}:
-	$(CABAL_EXE) sandbox init
+	$(CABAL) sandbox init
 
-# order-only dependency: we just want the sandbox to exist
 ${CS_BIN}/alex: | ${CS}
-	$(CABAL) install alex
+	$(CABAL_INSTALL) alex
 
-# order-only dependency: we just want the sandbox to exist. Dependency
-# on alex so that `make -j` doesn't try running simultaneous installs
-# in the same sandbox
 ${CS_BIN}/happy: | ${CS} ${CS_BIN}/alex
-	$(CABAL) install happy
+	$(CABAL_INSTALL) happy
 
-src/GitRev.hs:
-	sh configure
-
-
-CRYPTOL_DEPS := \
-  $(shell find src cryptol \( -name \*.hs -or -name \*.x -or -name \*.y \) -and \( -not -name \*\#\* \) -print) \
+CRYPTOL_SRC := \
+  $(shell find src cryptol \
+            \( -name \*.hs -or -name \*.x -or -name \*.y \) \
+            -and \( -not -name \*\#\* \) -print) \
   $(shell find lib -name \*.cry)
 
+src/GitRev.hs: .git/index
+	sh configure
+
 print-%:
 	@echo $* = $($*)
 
-${CS_BIN}/cryptol: ${CS_BIN}/alex ${CS_BIN}/happy $(CRYPTOL_DEPS) | ${CS}
-	$(CABAL) install .
+# /usr/share/cryptol on POSIX, installdir/cryptol on Windows
+DATADIR := ${PREFIX_ABS}${PREFIX_SHARE}
 
-${CS_BIN}/cryptolnb: ${CS_BIN}/alex ${CS_BIN}/happy | ${CS}
-	$(CABAL) install . -fnotebook
+dist/setup-config: | ${CS_BIN}/alex ${CS_BIN}/happy
+	$(CABAL_INSTALL) --only-dependencies
+	$(CABAL) configure                            \
+          --prefix=$(call adjust-path,${PREFIX_ABS})  \
+          --datasubdir=cryptol
 
-${PKG}: ${CS_BIN}/cryptol
-	mkdir -p ${PKG}/bin
-	mkdir -p ${PKG}/lib
-	mkdir -p ${PKG}/doc/examples/contrib
-	cp ${CS_BIN}/cryptol ${PKG}/bin/cryptol
-	cp -R docs/*.md ${PKG}/doc
-	cp -R docs/*.pdf ${PKG}/doc
-	cp -R lib/* ${PKG}/lib
-	cp docs/ProgrammingCryptol/aes/AES.cry ${PKG}/doc/examples
-	cp docs/ProgrammingCryptol/enigma/Enigma.cry ${PKG}/doc/examples
-	cp examples/DES.cry ${PKG}/doc/examples
-	cp examples/Cipher.cry ${PKG}/doc/examples
-	cp examples/DEStest.cry ${PKG}/doc/examples
-	cp examples/Test.cry ${PKG}/doc/examples
-	cp examples/SHA1.cry ${PKG}/doc/examples
-	cp examples/contrib/mkrand.cry ${PKG}/doc/examples/contrib
-	cp examples/contrib/RC4.cry ${PKG}/doc/examples/contrib
-	cp examples/contrib/simon.cry ${PKG}/doc/examples/contrib
-	cp examples/contrib/speck.cry ${PKG}/doc/examples/contrib
-	cp LICENSE ${PKG}/doc
+${CRYPTOL_EXE}: $(CRYPTOL_SRC) src/GitRev.hs dist/setup-config
+	$(CABAL_BUILD)
+
+# ${CS_BIN}/cryptolnb: ${CS_BIN}/alex ${CS_BIN}/happy | ${CS}
+# 	$(CABAL) install . -fnotebook
+
+PKG_BIN       := ${PKG_PREFIX}/bin
+PKG_SHARE     := ${PKG_PREFIX}${PREFIX_SHARE}
+PKG_CRY       := ${PKG_SHARE}/cryptol
+PKG_DOC       := ${PKG_SHARE}${PREFIX_DOC}
+PKG_EXAMPLES  := ${PKG_DOC}/examples
+PKG_EXCONTRIB := ${PKG_EXAMPLES}/contrib
+
+PKG_EXAMPLE_FILES := docs/ProgrammingCryptol/aes/AES.cry       \
+                     docs/ProgrammingCryptol/enigma/Enigma.cry \
+                     examples/DES.cry                          \
+                     examples/Cipher.cry                       \
+                     examples/DEStest.cry                      \
+                     examples/Test.cry                         \
+                     examples/SHA1.cry
+
+PKG_EXCONTRIB_FILES := examples/contrib/mkrand.cry \
+                       examples/contrib/RC4.cry    \
+                       examples/contrib/simon.cry  \
+                       examples/contrib/speck.cry
+
+${PKG}: ${CRYPTOL_EXE}
+	$(CABAL) copy --destdir=${PKG}
+# don't want to bundle the cryptol library in the binary distribution
+	rm -rf ${PKG_PREFIX}/lib
+	mkdir -p ${PKG_CRY}
+	mkdir -p ${PKG_DOC}
+	mkdir -p ${PKG_EXAMPLES}
+	mkdir -p ${PKG_EXCONTRIB}
+	cp docs/*.md ${PKG_DOC}
+	cp docs/*.pdf ${PKG_DOC}
+	cp LICENSE ${PKG_DOC}
+	for EXAMPLE in ${PKG_EXAMPLE_FILES}; do \
+          cp $$EXAMPLE ${PKG_EXAMPLES}; done
+	for EXAMPLE in ${PKG_EXCONTRIB_FILES}; do \
+          cp $$EXAMPLE ${PKG_EXCONTRIB}; done
 
 ${PKG}.tar.gz: ${PKG}
 	tar -czvf $@ $<
@@ -112,19 +158,23 @@ ${PKG}.zip: ${PKG}
 	zip -r $@ $<
 
 ${PKG}.msi: ${PKG} win32/cryptol.wxs
-	${HEAT} dir ${PKG} -o allfiles.wxs -nologo -var var.pkg -ag -wixvar -cg ALLFILES -srd -dr INSTALLDIR -sfrag
-	${CANDLE} -ext WixUIExtension -ext WixUtilExtension -dversion=${VERSION} -dpkg=${PKG} win32/cryptol.wxs
-	${CANDLE} -ext WixUIExtension -ext WixUtilExtension -dversion=${VERSION} -dpkg=${PKG} allfiles.wxs
-	${LIGHT} -ext WixUIExtension -ext WixUtilExtension -sval -o $@ cryptol.wixobj allfiles.wixobj
+	${HEAT} dir ${PKG_PREFIX} -o allfiles.wxs -nologo -var var.pkg \
+          -ag -wixvar -cg ALLFILES -srd -dr INSTALLDIR -sfrag
+	${CANDLE} -ext WixUIExtension -ext WixUtilExtension            \
+          -dversion=${VERSION} -dpkg=${PKG_PREFIX} win32/cryptol.wxs
+	${CANDLE} -ext WixUIExtension -ext WixUtilExtension            \
+          -dversion=${VERSION} -dpkg=${PKG_PREFIX} allfiles.wxs
+	${LIGHT} -ext WixUIExtension -ext WixUtilExtension             \
+	  -sval -o $@ cryptol.wixobj allfiles.wixobj
 	rm -f allfiles.wxs
 	rm -f *.wixobj
 	rm -f *.wixpdb
 
 ${CS_BIN}/cryptol-test-runner: \
-  $(CS_BIN)/cryptol            \
+  ${PKG}                       \
   $(CURDIR)/tests/Main.hs      \
   $(CURDIR)/tests/cryptol-test-runner.cabal
-	$(CABAL) install ./tests
+	$(CABAL_INSTALL) ./tests
 
 .PHONY: test
 test: ${CS_BIN}/cryptol-test-runner
@@ -132,25 +182,22 @@ test: ${CS_BIN}/cryptol-test-runner
 	echo "Testing on $(UNAME)-$(ARCH)" &&                              \
 	$(realpath $(CS_BIN)/cryptol-test-runner)                          \
 	  $(foreach t,$(TESTS),-d $t)                                      \
-	  -c $(call adjust-path,$(realpath $(CS_BIN)/cryptol$(EXE_EXT))) \
+	  -c $(call adjust-path,${CURDIR}/${PKG_BIN}/cryptol${EXE_EXT})    \
 	  -r output                                                        \
 	  -T --hide-successes                                              \
 	  -T --jxml=$(call adjust-path,$(CURDIR)/results.xml)              \
 	  $(if $(TEST_DIFF),-p $(TEST_DIFF),)                              \
 	)
 
-.PHONY: notebook
-notebook: ${CS_BIN}/cryptolnb
-	cd notebook && ./notebook.sh
-
+# .PHONY: notebook
+# notebook: ${CS_BIN}/cryptolnb
+# 	cd notebook && ./notebook.sh
 
 .PHONY: clean
 clean:
 	cabal clean
 	rm -f src/GitRev.hs
-	rm -f $(CS_BIN)/cryptol
 	rm -f $(CS_BIN)/cryptol-test-suite
-	rm -f $(CS_BIN)/cryptolnb
 	rm -rf cryptol-${VERSION}*/
 	rm -rf cryptol-${VERSION}*.tar.gz
 	rm -rf cryptol-${VERSION}*.zip
@@ -158,7 +205,7 @@ clean:
 
 .PHONY: squeaky
 squeaky: clean
-	-$(CABAL_EXE) sandbox delete
+	-$(CABAL) sandbox delete
 	(cd docs; make clean)
 	rm -rf dist
 	rm -rf tests/dist

cryptol.cabal

@@ -9,7 +9,8 @@ Category:            Language
 Build-type:          Configure
 Cabal-version:       >= 1.18
 
-data-files:          lib/Cryptol.cry
+data-files:          *.cry
+data-dir:            lib
 
 flag static
   default: False

cryptol/Main.hs

@@ -6,6 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 module Main where
@@ -13,7 +14,8 @@ module Main where
 import OptParser
 import REPL.Command (loadCmd,loadPrelude)
 import REPL.Haskeline
-import REPL.Monad (REPL,setREPLTitle,io,DotCryptol(..))
+import REPL.Monad (REPL,setREPLTitle,io,DotCryptol(..),
+                   prependSearchPath,setSearchPath)
 import REPL.Logo
 import qualified REPL.Monad as REPL
 import Paths_cryptol (version)
@@ -22,26 +24,29 @@ import Cryptol.Version (commitHash, commitBranch, commitDirty)
 import Data.Version (showVersion)
 import Cryptol.Utils.PP(pp)
 import Data.Monoid (mconcat)
-import System.Environment (getArgs,getProgName)
+import System.Environment (getArgs, getProgName, lookupEnv)
 import System.Exit (exitFailure)
+import System.FilePath (splitSearchPath)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
 
 data Options = Options
-  { optLoad       :: [FilePath]
-  , optVersion    :: Bool
-  , optHelp       :: Bool
-  , optBatch      :: Maybe FilePath
-  , optDotCryptol :: DotCryptol
+  { optLoad            :: [FilePath]
+  , optVersion         :: Bool
+  , optHelp            :: Bool
+  , optBatch           :: Maybe FilePath
+  , optDotCryptol      :: DotCryptol
+  , optCryptolPathOnly :: Bool
   } deriving (Show)
 
 defaultOptions :: Options
 defaultOptions  = Options
-  { optLoad       = []
-  , optVersion    = False
-  , optHelp       = False
-  , optBatch      = Nothing
-  , optDotCryptol = DotCDefault
+  { optLoad            = []
+  , optVersion         = False
+  , optHelp            = False
+  , optBatch           = Nothing
+  , optDotCryptol      = DotCDefault
+  , optCryptolPathOnly = False
   }
 
 options :: [OptDescr (OptParser Options)]
@@ -60,6 +65,9 @@ options  =
 
   , Option ""  ["cryptol-script"] (ReqArg addDotC "FILE")
     "read additional .cryptol files"
+
+  , Option ""  ["cryptolpath-only"] (NoArg setCryptolPathOnly)
+    "only look for .cry files in CRYPTOLPATH; don't use built-in locations"
   ]
 
 -- | Set a single file to be loaded.  This should be extended in the future, if
@@ -92,6 +100,9 @@ addDotC path = modify $ \ opts ->
     DotCDisabled -> opts
     DotCFiles xs -> opts { optDotCryptol = DotCFiles (path:xs) }
 
+setCryptolPathOnly :: OptParser Options
+setCryptolPathOnly  = modify $ \opts -> opts { optCryptolPathOnly = True }
+
 -- | Parse arguments.
 parseArgs :: [String] -> Either [String] Options
 parseArgs args = case getOpt (ReturnInOrder addFile) options args of
@@ -134,6 +145,17 @@ setupREPL :: Options -> REPL ()
 setupREPL opts = do
   displayLogo True
   setREPLTitle
+  mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
+  case mCryptolPath of
+    Nothing -> return ()
+    Just path | optCryptolPathOnly opts -> setSearchPath path'
+              | otherwise               -> prependSearchPath path'
+#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
+      -- Windows paths search from end to beginning
+      where path' = reverse (splitSearchPath path)
+#else
+      where path' = splitSearchPath path
+#endif
   case optLoad opts of
     []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
     [l] -> loadCmd l `REPL.catch` \x -> io $ print $ pp x

cryptol/REPL/Monad.hs

@@ -33,6 +33,7 @@ module REPL.Monad (
   , getTypeNames
   , getPropertyNames
   , LoadedModule(..), getLoadedMod, setLoadedMod
+  , setSearchPath, prependSearchPath
   , builtIns
   , getPrompt
   , shouldContinue
@@ -237,6 +238,16 @@ setLoadedMod n = do
 getLoadedMod :: REPL (Maybe LoadedModule)
 getLoadedMod  = eLoadedMod `fmap` getRW
 
+setSearchPath :: [FilePath] -> REPL ()
+setSearchPath path = do
+  me <- getModuleEnv
+  setModuleEnv $ me { M.meSearchPath = path }
+
+prependSearchPath :: [FilePath] -> REPL ()
+prependSearchPath path = do
+  me <- getModuleEnv
+  setModuleEnv $ me { M.meSearchPath = path ++ M.meSearchPath me }
+
 shouldContinue :: REPL Bool
 shouldContinue  = eContinue `fmap` getRW
 

src/Cryptol/ModuleSystem/Base.hs

@@ -183,8 +183,6 @@ moduleFile :: ModName -> String -> FilePath
 moduleFile (ModName ns) = addExtension (joinPath ns)
 
 -- | Discover a module.
---
--- TODO: extend this with a search path.
 findModule :: ModName -> ModuleM FilePath
 findModule n = do
   paths <- getSearchPath

src/Cryptol/ModuleSystem/Env.hs

@@ -6,6 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE PatternGuards #-}
 
 module Cryptol.ModuleSystem.Env where
@@ -24,6 +25,7 @@ import Data.Foldable (fold)
 import Data.Function (on)
 import qualified Data.Map as Map
 import Data.Monoid ((<>), Monoid(..))
+import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
 import System.Environment.Executable(splitExecutablePath)
 import System.FilePath ((</>), normalise, joinPath, splitPath)
 import qualified Data.List as List
@@ -51,20 +53,33 @@ resetModuleEnv env = env
 
 initialModuleEnv :: IO ModuleEnv
 initialModuleEnv  = do
+  curDir <- getCurrentDirectory
   dataDir <- getDataDir
   (binDir, _) <- splitExecutablePath
-  -- XXX Ugh. The first of these seems to work on unix-like systems,
-  -- the second seems to work on Windows. The results from
-  -- System.Environment.Executable must be inconsistent between
-  -- platforms, so for now we'll just try both. See #113
-  let instDir1 = normalise . joinPath . init . init . splitPath $ binDir
-      instDir2 = normalise . joinPath . init . splitPath $ binDir
+  let instDir = normalise . joinPath . init . splitPath $ binDir
+  userDir <- getAppUserDataDirectory "cryptol"
   return ModuleEnv
     { meLoadedModules = mempty
     , meNameSeeds     = T.nameSeeds
     , meEvalEnv       = mempty
     , meFocusedModule = Nothing
-    , meSearchPath    = [dataDir </> "lib", instDir1 </> "lib", instDir2 </> "lib", "."]
+      -- we search these in order, taking the first match
+    , meSearchPath    = [ curDir
+                          -- something like $HOME/.cryptol
+                        , userDir
+#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
+                          -- ../cryptol on win32
+                        , instDir </> "cryptol"
+#else
+                          -- ../share/cryptol on others
+                        , instDir </> "share" </> "cryptol"
+#endif
+                          -- Cabal-defined data directory. Since this
+                          -- is usually a global location like
+                          -- /usr/local, search this one last in case
+                          -- someone has multiple Cryptols
+                        , dataDir
+                        ]
     , meDynEnv        = mempty
     , meMonoBinds     = True
     }

src/Cryptol/ModuleSystem/Monad.hs

@@ -80,9 +80,12 @@ data ModuleError
 instance PP ModuleError where
   ppPrec _ e = case e of
 
-    ModuleNotFound src _path ->
+    ModuleNotFound src path ->
       text "[error]" <+>
       text "Could not find module" <+> pp src
+      $$
+      hang (text "Searched paths:")
+         4 (vcat (map text path))
 
     CantFindFile path ->
       text "[error]" <+>