diff --git a/.github/ci.sh b/.github/ci.sh index dd5bec3eb..af789c6c6 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -25,7 +25,7 @@ deps() { # Finds the cabal-built '$1' executable and copies it to the '$2' # directory. extract_exe() { - exe="$(cabal v2-exec which "$1$EXT")" + exe="$(cabal list-bin -v0 "$1")" name="$(basename "$exe")" echo "Copying $name to $2" mkdir -p "$2" @@ -53,10 +53,10 @@ retry() { } setup_dist_bins() { - extract_exe "cryptol" "dist/bin" - extract_exe "cryptol-html" "dist/bin" - extract_exe "cryptol-remote-api" "dist/bin" - extract_exe "cryptol-eval-server" "dist/bin" + extract_exe "exe:cryptol" "dist/bin" + extract_exe "exe:cryptol-html" "dist/bin" + extract_exe "exe:cryptol-remote-api" "dist/bin" + extract_exe "exe:cryptol-eval-server" "dist/bin" strip dist/bin/cryptol* || echo "Strip failed: Ignoring harmless error" } @@ -64,11 +64,12 @@ build() { ghc_ver="$(ghc --numeric-version)" cp cabal.GHC-"$ghc_ver".config cabal.project.freeze cabal v2-update - cabal v2-configure -j2 --minimize-conflict-set + cabal v2-configure -j2 --minimize-conflict-set --enable-tests git status --porcelain retry ./cry build exe:cryptol-html "$@" # retry due to flakiness with windows builds retry ./cry build exe:cryptol-remote-api "$@" retry ./cry build exe:cryptol-eval-server "$@" + retry ./cry build test:cryptol-api-tests "$@" } install_system_deps() { diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a5157c6ac..95143e4f7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -151,8 +151,13 @@ jobs: run: .github/ci.sh build - shell: bash + name: Extract Cryptol executables to dist/bin/ run: .github/ci.sh setup_dist_bins + - shell: bash + name: Extract Cryptol API test suite executable to bin/ + run: .github/ci.sh extract_exe "test:cryptol-api-tests" "bin" + - shell: bash run: .github/ci.sh check_docs if: runner.os != 'Windows' @@ -271,6 +276,10 @@ jobs: os: [ubuntu-22.04, macos-14, windows-2019] continue-on-error: [false] include: + - suite: api-tests + target: '' + os: ubuntu-22.04 + continue-on-error: false - suite: rpc target: '' os: ubuntu-22.04 @@ -358,6 +367,7 @@ jobs: chmod +x dist/bin/cryptol chmod +x dist/bin/cryptol-remote-api chmod +x dist/bin/cryptol-eval-server + chmod +x bin/cryptol-api-tests chmod +x bin/test-runner .github/ci.sh install_system_deps .github/ci.sh deps bin/abc* @@ -393,6 +403,13 @@ jobs: export PATH=$PWD/bin:$PWD/dist/bin:$PATH cryptol-remote-api/run_rpc_tests.sh + - if: matrix.suite == 'api-tests' + shell: bash + continue-on-error: ${{ matrix.continue-on-error }} + run: | + export PATH=$PWD/bin:$PWD/dist/bin:$PATH + ./bin/cryptol-api-tests + build-push-image: runs-on: ubuntu-22.04 needs: [config] diff --git a/CHANGES.md b/CHANGES.md index d752c6146..11ffd01cd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -21,6 +21,9 @@ invoked as `:dumptests - ` allowing for easier experimentation and testing. +* The REPL properly supports tab completion for the `:t` and `:check` commands. + ([#1780](https://github.com/GaloisInc/cryptol/issues/1780)) + # 3.2.0 -- 2024-08-20 ## Language changes diff --git a/api-tests/Main.hs b/api-tests/Main.hs new file mode 100644 index 000000000..8edec4880 --- /dev/null +++ b/api-tests/Main.hs @@ -0,0 +1,114 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Main (main) where + +import Data.Foldable (traverse_) +import System.Console.Haskeline.Completion (Completion(..)) +import Test.Tasty +import Test.Tasty.HUnit + +import qualified Cryptol.REPL.Command as REPL +import qualified Cryptol.REPL.Monad as REPL +import Cryptol.REPL.Monad (REPL) +import Cryptol.Utils.Logger (quietLogger) +import Cryptol.Utils.PP (pp) + +import REPL.Haskeline (cryptolCommand) + +main :: IO () +main = defaultMain $ + testGroup "Cryptol API tests" + [ testGroup "Tab completion tests" $ + map (uncurry replTabCompletionTestCase) + [ (":ch", ":check") + , (":check", ":check") + , (":check ", ":check ") + , (":check rev", ":check reverse") + , (":check-docstrings", ":check-docstrings ") + , (":check-docstrings ", ":check-docstrings ") + , (":t", ":t") + , (":t rev", ":t reverse") + , (":time", ":time ") + , (":time ", ":time ") + , (":time rev", ":time reverse") + , (":type", ":type ") + , (":type ", ":type ") + , (":type rev", ":type reverse") + ] + ] + +-- | Assert a property in the 'REPL' monad and turn it into a test case. +replTestCase :: TestName -> REPL () -> TestTree +replTestCase name replAssertion = + testCase name $ + REPL.runREPL + False -- Don't use batch mode + False -- Disable call stacks + quietLogger -- Ignore all log messages + replAssertion + +-- | Assert that the REPL will tab-complete the given input in one specific way. +replTabCompletionTestCase :: + -- | The input before the cursor just prior to hitting the tab key. + String -> + -- | The expected terminal input after hitting the tab key. Note that although + -- this is specified as a single 'String', this may actually correspond to + -- multiple Haskeline 'Completion's under the hood. See the comments below for + -- details on how multiple 'Completion's are resolved to a single 'String'. + String -> + TestTree +replTabCompletionTestCase beforeTab afterTabExpected = + replTestCase (show beforeTab ++ " --> " ++ show afterTabExpected) $ + do -- Load the prelude so that the REPL knows how to tab-complete prelude + -- definitions. + REPL.loadPrelude + -- Perform the actual tab completion. (Oddly, Haskeline requires that the + -- input to the left of the cursor should be reversed.) + (_input, completions) <- cryptolCommand (reverse beforeTab, "") + -- Check that the results match what is expected. We have to do a bit of + -- additional work that Haskeline does not do: + -- + -- 1. If there is exactly one Completion and its replacement value is + -- empty, then Haskeline will add a space character to the end of the + -- input on the terminal. Oddly, this space character is /not/ added in + -- the Completion itself. As such, we have to add this ourselves. + -- + -- 2. If there are multiple completions, then Haskeline will complete the + -- terminal input up to the longest common prefix of all the + -- completions' replacement strings. As such, we compute this longest + -- common prefix ourselves. + REPL.io $ + case completions of + [] -> assertFailure "Expected tab completions, but received none" + [completion] -> + do assertFinished completion + let replace = replacement completion + afterTabActual + | null replace = -- See (1) above + beforeTab ++ " " + | otherwise = beforeTab ++ replace + afterTabExpected @=? afterTabActual + _:_ -> + do traverse_ assertFinished completions + let replaceLcp = + -- See (2) above + longestCommonPrefix (map replacement completions) + afterTabActual = beforeTab ++ replaceLcp + afterTabExpected @=? afterTabActual + `REPL.catch` + -- If something goes wrong run running the REPL, report it as a test + -- failure. + \x -> REPL.io $ assertFailure $ show $ pp x + where + assertFinished :: Completion -> Assertion + assertFinished completion = + assertBool ("Tab completion for " ++ display completion ++ " finished") + (isFinished completion) + +-- | Compute the longest common prefix in a list of lists. +longestCommonPrefix :: forall a. Eq a => [[a]] -> [a] +longestCommonPrefix [] = [] +longestCommonPrefix s = foldr1 lcp s + where + lcp :: [a] -> [a] -> [a] + lcp xs ys = map fst $ takeWhile (uncurry (==)) + $ zip xs ys diff --git a/cryptol/REPL/Haskeline.hs b/cryptol-repl-internal/REPL/Haskeline.hs similarity index 88% rename from cryptol/REPL/Haskeline.hs rename to cryptol-repl-internal/REPL/Haskeline.hs index 98e597f4f..4d0bdc797 100644 --- a/cryptol/REPL/Haskeline.hs +++ b/cryptol-repl-internal/REPL/Haskeline.hs @@ -225,20 +225,52 @@ cryptolCommand cursor@(l,r) | ":" `isPrefixOf` l' , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of - [c] | null rest && not (any isSpace l') -> do + [c] | cursorRightAfterCmd rest -> return (l, cmdComp cmd c) - | otherwise -> do - (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r) - return (unwords [rest', reverse cmd],cs) - - cmds -> - return (l, concat [ cmdComp l' c | c <- cmds ]) + | otherwise -> + completeCmdArgument cmd rest c + + cmds + -- If the command name is a prefix of multiple commands, then as a + -- special case, check if (1) the name matches one command exactly, and + -- (2) there is already some input for an argument. If so, proceed to + -- tab-complete that argument. This ensures that something like + -- `:check rev` will complete to `:check reverse`, even though the + -- command name `:check` is a prefix for both the `:check` and + -- `:check-docstrings` commands (#1781). + | [c] <- nub (findCommandExact cmd) + , not (cursorRightAfterCmd rest) -> + completeCmdArgument cmd rest c + + | otherwise -> + return (l, concat [ cmdComp l' c | c <- cmds ]) -- Complete all : commands when the line is just a : | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ]) | otherwise = completeExpr cursor where l' = sanitize (reverse l) + -- Check if the cursor is positioned immediately after the input for the + -- command, without any command arguments typed in after the command's name. + cursorRightAfterCmd :: + String + {- The rest of the input after the command. -} -> + Bool + cursorRightAfterCmd rest = null rest && not (any isSpace l') + + -- Perform tab completion for a single argument to a command. + completeCmdArgument :: + String + {- The name of the command as a String. -} -> + String + {- The rest of the input after the command. -} -> + CommandDescr + {- The description of the command. -} -> + REPL (String, [Completion]) + completeCmdArgument cmd rest c = + do (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r) + return (unwords [rest', reverse cmd],cs) + -- | Generate completions from a REPL command definition. cmdComp :: String -> CommandDescr -> [Completion] cmdComp prefix c = do diff --git a/cryptol/REPL/Logo.hs b/cryptol-repl-internal/REPL/Logo.hs similarity index 100% rename from cryptol/REPL/Logo.hs rename to cryptol-repl-internal/REPL/Logo.hs diff --git a/cryptol.cabal b/cryptol.cabal index 872e8664e..f7a6b69e1 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -254,18 +254,22 @@ library if flag(relocatable) cpp-options: -DRELOCATABLE -executable cryptol - Default-language: - Haskell2010 - Main-is: Main.hs - hs-source-dirs: cryptol +-- The portions of the Cryptol REPL that are specific to the Cryptol executable. +-- We factor this out into a separate internal library because (1) it has some +-- dependencies (e.g., ansi-terminal and haskeline) that the Cryptol library +-- does not need to depend on, and (2) we want to be able to test this code in +-- the cryptol-api-tests test suite. +library cryptol-repl-internal + exposed-modules: REPL.Haskeline + REPL.Logo Autogen-modules: Paths_cryptol - - Other-modules: OptParser, - REPL.Haskeline, - REPL.Logo, - Paths_cryptol - + Other-modules: Paths_cryptol + hs-source-dirs: cryptol-repl-internal + default-language: Haskell2010 + GHC-options: -Wall -O2 + if os(linux) && flag(static) + ld-options: -static -pthread + ghc-options: -optl-fuse-ld=bfd build-depends: ansi-terminal , base , base-compat @@ -278,6 +282,19 @@ executable cryptol , monad-control , text , transformers + +executable cryptol + Default-language: + Haskell2010 + Main-is: Main.hs + hs-source-dirs: cryptol + Other-modules: OptParser + build-depends: base + , base-compat + , cryptol + , cryptol-repl-internal + , directory + , filepath GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2 if impl(ghc >= 8.0.1) ghc-options: -Wno-redundant-constraints @@ -315,6 +332,26 @@ executable check-exercises , temporary , text GHC-options: -Wall + +-- Test cases that require the use of the Cryptol API to test effectively. Most +-- other test cases should be added to the integration tests (which only require +-- the Cryptol executable and/or the REPL) under tests/. +test-suite cryptol-api-tests + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: api-tests + default-language: Haskell2010 + GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2 + if os(linux) && flag(static) + ld-options: -static -pthread + ghc-options: -optl-fuse-ld=bfd + build-depends: base + , cryptol + , cryptol-repl-internal + , haskeline + , tasty + , tasty-hunit + benchmark cryptol-bench type: exitcode-stdio-1.0 main-is: Main.hs