Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Internal error if files cannot be written to the directory for temporary files #4516

Closed
oisdk opened this issue Mar 15, 2020 · 4 comments
Closed
Assignees
Labels
type: bug Issues and pull requests about actual bugs ux: highlighting Issues relating to syntax highlighting ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Milestone

Comments

@oisdk
Copy link

oisdk commented Mar 15, 2020

On typecheck I get the following error:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Monad/Base.hs:4124

However it only happens from within emacs, i.e. if I run agda Test.agda there is no problem.

@sattlerc
Copy link
Contributor

Please supply additional information:

  • a test case exhibiting the behaviour,
  • the version of Agda you are using (agda --version).

@sattlerc sattlerc added the status: info-needed More information is needed from the bug reporter to confirm the issue. label Mar 15, 2020
@oisdk
Copy link
Author

oisdk commented Mar 15, 2020

  • Agda --version: 2.6.1
  • Compiled from current commit (f7c0c35) with cabal v2-install
  • Test case: in Test.agda
module Test where

agda2-load

@oisdk
Copy link
Author

oisdk commented Mar 15, 2020

@oisdk oisdk closed this as completed Mar 15, 2020
@nad
Copy link
Contributor

nad commented Mar 15, 2020

Agda shouldn't raise an internal error if the problem is related to the file system.

Location of the error: src/full/Agda/TypeChecking/Monad/Base.hs:4124

-- | 'runSafeTCM' runs a safe 'TCM' action (a 'TCM' action which cannot fail)
-- in the initial environment.
runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
runSafeTCM m st = runTCM initEnv st m `E.catch` (\ (e :: TCErr) -> __IMPOSSIBLE__)

This definition is used once:

-- | Opposite of 'liftIO' for 'CommandM'.
-- Use only if main errors are already catched.
commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ci_i = revLift runStateT lift $ \ct -> revLiftTC runSafeTCM liftIO $ ci_i . (. ct)

This definition is also used once:

-- | Handle every possible kind of error (#637), except for
-- AsyncCancelled, which is used to abort Agda.
handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors m = commandMToIO $ \ toIO -> do
let handle e =
Right <$>
(toIO $ handleErr $ Exception noRange $ text $ show e)
asyncHandler e@AsyncCancelled = return (Left e)
generalHandler (e :: E.SomeException) = handle e
r <- ((Right <$> toIO m) `E.catch` asyncHandler)
`E.catch` generalHandler
case r of
Right x -> return x
Left e -> E.throwIO e

I'm wondering if the problem is that an error is raised in handleErr:

-- | Displays an error and instructs Emacs to jump to the site of the
-- error. Because this function may switch the focus to another file
-- the status information is also updated.
handleErr e = do
unsolvedNotOK <- lift $ not . optAllowUnsolved <$> pragmaOptions
meta <- lift $ computeUnsolvedMetaWarnings
constr <- lift $ computeUnsolvedConstraints
err <- lift $ errorHighlighting e
modFile <- lift $ useTC stModuleToSource
method <- lift $ viewTC eHighlightingMethod
let info = compress $ mconcat $
-- Errors take precedence over unsolved things.
err : if unsolvedNotOK then [meta, constr] else []
-- TODO: make a better predicate for this
noError <- lift $ null <$> prettyError e
x <- lift $ optShowImplicit <$> useTC stPragmaOptions
unless noError $ mapM_ putResponse $
[ Resp_DisplayInfo $ Info_Error $ Info_GenericError e ] ++
tellEmacsToJumpToError (getRange e) ++
[ Resp_HighlightingInfo info KeepHighlighting
method modFile ] ++
[ Resp_Status $ Status { sChecked = False
, sShowImplicitArguments = x
} ]

I guess that in this case putResponse failed because an attempt is made to write highlighting information to a file. Perhaps the method should always be Direct in this error handler.

I managed to recreate the error message:

$ echo "module Set where" > Test.agda
$ echo 'IOTCM "Test.agda" None Indirect (Cmd_load "Test.agda" [])' | agda --interaction --no-libraries
Agda2> (agda2-info-action "*Error*" "/tmp/Test.agda:1,8-8\n/tmp/Test.agda:1,8: Parse error\nSet<ERROR>\n where\n..." nil)
((last . 3) . (agda2-maybe-goto '("/tmp/Test.agda" . 8)))
(agda2-highlight-load-and-delete-action "/tmp/agda2-mode1875-0")
(agda2-status-action "")
Agda2> $ 
$ echo 'IOTCM "Test.agda" None Indirect (Cmd_load "Test.agda" [])' | TMPDIR=/non-existent agda --interaction --no-libraries
Agda2> (agda2-info-action "*Error*" "/tmp/Test.agda:1,8-8\n/tmp/Test.agda:1,8: Parse error\nSet<ERROR>\n where\n..." nil)
((last . 3) . (agda2-maybe-goto '("/tmp/Test.agda" . 8)))
(agda2-info-action "*Error*" "An internal error has occurred. Please report this as a bug.\nLocation of the error: src/full/Agda/TypeChecking/Monad/Base.hs:4124\n" nil)
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Monad/Base.hs:4124

Another way to make handleErr fail would be to set things up so that Agda cannot write to stdout, but in that case the "internal error" message is presumably not delivered to the user.

@nad nad reopened this Mar 15, 2020
@nad nad added type: bug Issues and pull requests about actual bugs and removed status: info-needed More information is needed from the bug reporter to confirm the issue. labels Mar 15, 2020
@nad nad added this to the 2.6.2 milestone Mar 15, 2020
@nad nad changed the title Internal error on interactive Internal error if files cannot be written to the directory for temporary files Mar 15, 2020
@nad nad closed this as completed in b05cb12 Mar 16, 2020
@andreasabel andreasabel added ux: highlighting Issues relating to syntax highlighting ux: interaction Issues to do with interactive development (holes, case splitting, etc) labels May 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
type: bug Issues and pull requests about actual bugs ux: highlighting Issues relating to syntax highlighting ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Projects
None yet
Development

No branches or pull requests

4 participants