diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 1ae12eaf4..5d0f29fe2 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -24,6 +24,7 @@ import Libraries.Data.StringMap import Libraries.Text.Distance.Levenshtein import System +import System.Clock import System.Directory %default covering @@ -1114,6 +1115,9 @@ record Defs where -- again timings : StringMap (Bool, Integer) -- ^ record of timings from logTimeRecord + timer : Maybe (Integer, String) + -- ^ for timing and checking timeouts; the maximum time after which a + -- timeout should be thrown warnings : List Warning -- ^ as yet unreported warnings @@ -1159,6 +1163,7 @@ initDefs , userHoles = empty , peFailures = empty , timings = empty + , timer = Nothing , warnings = [] } @@ -2351,6 +2356,13 @@ setNFThreshold max = do defs <- get Ctxt put Ctxt (record { options->elabDirectives->nfThreshold = max } defs) +export +setSearchTimeout : {auto c : Ref Ctxt Defs} -> + Integer -> Core () +setSearchTimeout t + = do defs <- get Ctxt + put Ctxt (record { options->session->searchTimeout = t } defs) + export isLazyActive : {auto c : Ref Ctxt Defs} -> Core Bool @@ -2582,3 +2594,48 @@ recordWarning w = do defs <- get Ctxt session <- getSession put Ctxt $ record { warnings $= (w ::) } defs + +export +getTime : Core Integer +getTime + = do clock <- coreLift (clockTime Process) + pure (seconds clock * nano + nanoseconds clock) + where + nano : Integer + nano = 1000000000 + +-- A simple timeout mechanism. We can start a timer, clear it, or check +-- whether too much time has passed and throw an exception if so + +||| Initialise the timer, setting the time in milliseconds after which a +||| timeout should be thrown. +||| Note: It's important to clear the timer when the operation that might +||| timeout is complete, otherwise something else might throw a timeout +||| error! +export +startTimer : {auto c : Ref Ctxt Defs} -> + Integer -> String -> Core () +startTimer tmax action + = do t <- getTime + defs <- get Ctxt + put Ctxt $ record { timer = Just (t + tmax * 1000000, action) } defs + +||| Clear the timer +export +clearTimer : {auto c : Ref Ctxt Defs} -> Core () +clearTimer + = do defs <- get Ctxt + put Ctxt $ record { timer = Nothing } defs + +||| If the timer was started more than t milliseconds ago, throw an exception +export +checkTimer : {auto c : Ref Ctxt Defs} -> + Core () +checkTimer + = do defs <- get Ctxt + let Just (max, action) = timer defs + | Nothing => pure () + t <- getTime + if (t > max) + then throw (Timeout action) + else pure () diff --git a/src/Core/Core.idr b/src/Core/Core.idr index e8f6a349e..404d33566 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -157,6 +157,7 @@ data Error : Type where ||| Contains list of specifiers for which foreign call cannot be resolved NoForeignCC : FC -> List String -> Error BadMultiline : FC -> String -> Error + Timeout : String -> Error InType : FC -> Name -> Error -> Error InCon : FC -> Name -> Error -> Error @@ -332,6 +333,7 @@ Show Error where show (NoForeignCC fc specs) = show fc ++ ":The given specifier " ++ show specs ++ " was not accepted by any available backend." show (BadMultiline fc str) = "Invalid multiline string: " ++ str + show (Timeout str) = "Timeout in " ++ str show (InType fc n err) = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++ @@ -423,6 +425,7 @@ getErrorLoc (InternalError _) = Nothing getErrorLoc (UserError _) = Nothing getErrorLoc (NoForeignCC loc _) = Just loc getErrorLoc (BadMultiline loc _) = Just loc +getErrorLoc (Timeout _) = Nothing getErrorLoc (InType _ _ err) = getErrorLoc err getErrorLoc (InCon _ _ err) = getErrorLoc err getErrorLoc (InLHS _ _ err) = getErrorLoc err diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 66e0a4eb8..927dee909 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -291,6 +291,9 @@ parameters (defs : Defs, topopts : EvalOpts) -- want to shortcut that second check, if we're evaluating -- everything, so don't let bind unless we need that log! let redok = redok1 || redok2 + checkTimer -- If we're going to time out anywhere, it'll be + -- when evaluating something recursive, so this is a + -- good place to check unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n pure $ "Stuck function: " ++ show n' if redok diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 0b8177e20..dfcf6fca5 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -157,6 +157,8 @@ record Session where dumpanf : Maybe String -- file to output ANF definitions dumpvmcode : Maybe String -- file to output VM code definitions profile : Bool -- generate profiling information, if supported + searchTimeout : Integer -- maximum number of milliseconds to run + -- expression/program search -- Warnings warningsAsErrors : Bool showShadowingWarning : Bool @@ -210,7 +212,7 @@ export defaultSession : Session defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel False False False Nothing Nothing - Nothing Nothing False False True False + Nothing Nothing False 1000 False True False export defaultElab : ElabDirectives diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index ea31283a6..67eec1a99 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -1010,6 +1010,7 @@ mutual AmbigDepth n => pure [IPragma [] (\nest, env => setAmbigLimit n)] AutoImplicitDepth n => pure [IPragma [] (\nest, env => setAutoImplicitLimit n)] NFMetavarThreshold n => pure [IPragma [] (\nest, env => setNFThreshold n)] + SearchTimeout n => pure [IPragma [] (\nest, env => setSearchTimeout n)] PairNames ty f s => pure [IPragma [] (\nest, env => setPair fc ty f s)] RewriteName eq rw => pure [IPragma [] (\nest, env => setRewrite fc eq rw)] PrimInteger n => pure [IPragma [] (\nest, env => setFromInteger n)] diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 9bda55078..e01a71efe 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -467,6 +467,7 @@ perror (NoForeignCC fc specs) = do ] <+> line <+> !(ploc fc) pure res perror (BadMultiline fc str) = pure $ errorDesc (reflow "While processing multi-line string" <+> dot <++> pretty str <+> dot) <+> line <+> !(ploc fc) +perror (Timeout str) = pure $ errorDesc (reflow "Timeout in" <++> pretty str) perror (InType fc n err) = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index f4e4b26d1..3b8310fa7 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1166,6 +1166,10 @@ directive fname indents dpt <- decorate fname Keyword $ intLit atEnd indents pure (NFMetavarThreshold (fromInteger dpt)) + <|> do decorate fname Keyword $ pragma "search_timeout" + t <- decorate fname Keyword $ intLit + atEnd indents + pure (SearchTimeout t) <|> do decorate fname Keyword $ pragma "pair" ty <- name f <- name diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index de8d56255..86f05ddb5 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -451,7 +451,7 @@ processEdit (ExprSearch upd line name hints) case holeInfo pi of NotHole => pure $ EditError "Not a searchable hole" SolvedHole locs => - do let (_ ** (env, tm')) = dropLamsTm locs [] tm + do let (_ ** (env, tm')) = dropLamsTm locs [] !(normaliseHoles defs [] tm) itm <- resugar env tm' let itm' : PTerm = if brack then addBracket replFC itm else itm if upd diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index ffd2a176a..3fc1f93cb 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -267,6 +267,7 @@ mutual PrefixRecordProjections : Bool -> Directive AutoImplicitDepth : Nat -> Directive NFMetavarThreshold : Nat -> Directive + SearchTimeout : Integer -> Directive public export data PField : Type where diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 38048fc39..4c95199cb 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -18,6 +18,7 @@ import Core.Env import Core.LinearCheck import Core.Metadata import Core.Normalise +import Core.Options import Core.Unify import Core.TT import Core.Value @@ -91,11 +92,14 @@ searchN : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> Nat -> Core (Search a) -> Core (List a, Core (Search a)) searchN max s - = tryUnify - (do res <- s - xs <- count max res - pure xs) - (pure ([], pure NoMore)) + = do startTimer (searchTimeout !getSession) "expression search" + tryUnify + (do res <- s + xs <- count max res + clearTimer + pure xs) + (do clearTimer + pure ([], pure NoMore)) where count : Nat -> Search a -> Core (List a, Core (Search a)) count k NoMore = pure ([], pure NoMore) @@ -235,7 +239,12 @@ firstSuccess (elab :: elabs) catch (do Result res more <- elab | NoMore => continue ust defs elabs pure (Result res (continue ust defs (more :: elabs)))) - (\err => continue ust defs elabs) + (\err => + case err of + -- Give up on timeout, or we'll keep trying all the + -- other branches. + Timeout _ => noResult + _ => continue ust defs elabs) where continue : UState -> Defs -> List (Core (Search a)) -> Core (Search a) @@ -301,6 +310,7 @@ searchName : {vars : _} -> Core (Search (Term vars, ExprDefs)) searchName fc rigc opts env target topty (n, ndef) = do defs <- get Ctxt + checkTimer let True = visibleInAny (!getNS :: !getNestedNS) (fullname ndef) (visibility ndef) | _ => noResult @@ -371,6 +381,7 @@ searchNames fc rig opts env ty topty [] = noResult searchNames fc rig opts env ty topty (n :: ns) = do defs <- get Ctxt + checkTimer vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns) let visns = mapMaybe id vis nfty <- nf defs env ty @@ -470,6 +481,7 @@ searchLocalWith fc nofn rig opts env [] ty topty = noResult searchLocalWith {vars} fc nofn rig opts env ((p, pty) :: rest) ty topty = do defs <- get Ctxt + checkTimer nty <- nf defs env ty getSuccessful fc rig opts False env ty topty [findPos defs p id !(nf defs env pty) nty, @@ -792,6 +804,7 @@ searchHole : {auto c : Ref Ctxt Defs} -> searchHole fc rig opts n locs topty defs glob = do searchty <- normalise defs [] (type glob) logTerm "interaction.search" 10 "Normalised type" searchty + checkTimer searchType fc rig opts [] topty locs searchty -- Declared at the top @@ -864,6 +877,13 @@ exprSearchOpts opts fc n_in hints = do defs <- get Ctxt Just (n, idx, gdef) <- lookupHoleName n_in defs | Nothing => undefinedName fc n_in + -- the REPL does this step, but doing it here too because + -- expression search might be invoked some other way + let Hole _ _ = definition gdef + | PMDef pi [] (STerm _ tm) _ _ + => do raw <- unelab [] !(toFullNames !(normaliseHoles defs [] tm)) + one raw + | _ => throw (GenericMsg fc "Name is already defined") lhs <- findHoleLHS !(getFullName (Resolved idx)) log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs) opts' <- if getRecData opts @@ -881,13 +901,24 @@ exprSearchOpts opts fc n_in hints [res] => pure $ Just res _ => pure Nothing +exprSearch' : {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto u : Ref UST UState} -> + FC -> Name -> List Name -> + Core (Search RawImp) +exprSearch' = exprSearchOpts (initSearchOpts True 5) + export exprSearch : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> FC -> Name -> List Name -> Core (Search RawImp) -exprSearch = exprSearchOpts (initSearchOpts True 5) +exprSearch fc n hints + = do startTimer (searchTimeout !getSession) "expression search" + res <- exprSearch' fc n hints + clearTimer + pure res export exprSearchN : {auto c : Ref Ctxt Defs} -> diff --git a/tests/Main.idr b/tests/Main.idr index 0a39f3013..401a65966 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -79,7 +79,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing "interactive021", "interactive022", "interactive023", "interactive024", "interactive025", "interactive026", "interactive027", "interactive028", "interactive029", "interactive030", "interactive031", "interactive032", - "interactive033"] + "interactive033", "interactive034", "interactive035"] idrisTestsInterface : TestPool idrisTestsInterface = MkTestPool "Interface" [] Nothing diff --git a/tests/idris2/interactive034/expected b/tests/idris2/interactive034/expected new file mode 100644 index 000000000..6623df086 --- /dev/null +++ b/tests/idris2/interactive034/expected @@ -0,0 +1,3 @@ +1/1: Building timeout (timeout.idr) +Main> tailIsNotSound contra (ConsIsSound headIsSound tailIsSound) = contra tailIsSound +Main> Bye for now! diff --git a/tests/idris2/interactive034/input b/tests/idris2/interactive034/input new file mode 100644 index 000000000..7ca7416b2 --- /dev/null +++ b/tests/idris2/interactive034/input @@ -0,0 +1,2 @@ +:gd 54 tailIsNotSound +:q diff --git a/tests/idris2/interactive034/run b/tests/idris2/interactive034/run new file mode 100755 index 000000000..f86d318f2 --- /dev/null +++ b/tests/idris2/interactive034/run @@ -0,0 +1,3 @@ +$1 --no-color --console-width 0 --no-banner timeout.idr < input + +rm -rf build diff --git a/tests/idris2/interactive034/timeout.idr b/tests/idris2/interactive034/timeout.idr new file mode 100644 index 000000000..bf93ca69e --- /dev/null +++ b/tests/idris2/interactive034/timeout.idr @@ -0,0 +1,56 @@ +import Data.List +import Data.List.Elem + +%search_timeout 1000 + +||| A Place has an ID and a number of tokens +data Place : Type where + MkPlace : (i : Nat) -> (nTokens : Nat) -> Place + +||| A transition has a name +data Transition : Type where + MkTransition : String -> Transition + +||| An Input links a Place and a Transition... +data Input : Type where + MkInput : (from : Place) -> (to : Transition) -> Input + +-- Accessor functions for proof +0 inputFrom : Input -> Place +inputFrom (MkInput p t) = p + +0 inputTo : Input -> Transition +inputTo (MkInput p t) = t + +data SoundInputFrom : Input -> List Place -> Type where + MkSoundInputFrom : (i : Input) + -> (ps : List Place) + -> (prf : Elem (inputFrom i) ps) + -> SoundInputFrom i ps + +data SoundInputTo : Input -> List Transition -> Type where + MkSoundInputTo : (i : Input) + -> (ts : List Transition) + -> (prf : Elem (inputTo i) ts) + -> SoundInputTo i ts + +data SoundInput : Input -> List Place -> List Transition -> Type where + MkSoundInput : (i : Input) + -> (ps : List Place) + -> (ts : List Transition) + -> (fromOK : SoundInputFrom i ps) + -> (toOK : SoundInputTo i ts) + -> SoundInput i ps ts + +data AllInputsSound : List Input -> List Place -> List Transition -> Type where + NilInputsIsSound : AllInputsSound [] _ _ + ConsIsSound : (headIsSound : SoundInput i ps ts) + -> (tailIsSound : AllInputsSound is ps ts) + -> AllInputsSound (i :: is) ps ts + +-- Searching here finds the right answer immediately, but then if we don't +-- have a timeout, it takes ages to explore more non-solutions! So we cut off +-- after a second +tailIsNotSound : (contra : (AllInputsSound is ps ts -> Void)) + -> AllInputsSound (i :: is) ps ts + -> Void diff --git a/tests/idris2/interactive035/expected b/tests/idris2/interactive035/expected new file mode 100644 index 000000000..55e19a0b7 --- /dev/null +++ b/tests/idris2/interactive035/expected @@ -0,0 +1,3 @@ +1/1: Building unify (unify.idr) +Main> 4 +Main> Bye for now! diff --git a/tests/idris2/interactive035/input b/tests/idris2/interactive035/input new file mode 100644 index 000000000..07e35e2a3 --- /dev/null +++ b/tests/idris2/interactive035/input @@ -0,0 +1,2 @@ +:ps 7 vlength +:q diff --git a/tests/idris2/interactive035/run b/tests/idris2/interactive035/run new file mode 100755 index 000000000..b184b53e6 --- /dev/null +++ b/tests/idris2/interactive035/run @@ -0,0 +1,3 @@ +$1 --no-color --console-width 0 --no-banner unify.idr < input + +rm -rf build diff --git a/tests/idris2/interactive035/unify.idr b/tests/idris2/interactive035/unify.idr new file mode 100644 index 000000000..948cdceec --- /dev/null +++ b/tests/idris2/interactive035/unify.idr @@ -0,0 +1,7 @@ +import Data.Vect + +data VectN : Type -> Type where + MkVectN : (n : Nat) -> Vect n a -> VectN a + +doSearch : Nat -> VectN Int +doSearch n = MkVectN ?vlength [1,2,3,4]