You load the module B.agda, which imports A.agda, in (say) Emacs.
You edit A.agda and type-check it by invoking Agda using a shell command.
You reload B.agda in Emacs.
In this case you might hope that A.agda should not be type-checked again (if the same options are in effect). However, I have observed that, in at least some cases, Agda does type-check the file again instead of loading the interface file.
This is a regression, Agda 2.6.1.2 does not have this bug, but Agda 2.6.2 does. Bisection points towards @rwe's commit 7119290686e02c11eff7695bf37c27582577663f ("imports/refact: Combine more conditions in getStoredInterface").
Here is a script that can be used to demonstrate the bug:
#!/usr/bin/env runhaskell
{-# LANGUAGE RecordWildCards #-}
import Data.List
import System.Exit
import RunAgda
moduleA = "module A where\n"
moduleAExtra = "postulate A : Set\n"
moduleB = "module B where\nimport A\n"
main :: IO ()
main = runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
-- Discard the first prompt.
echoUntilPrompt
-- Write A and B.
writeFile "A.agda" moduleA
writeFile "B.agda" moduleB
-- Load B.
loadAndEcho "B.agda"
-- Modify A.
writeFile "A.agda" (moduleA ++ moduleAExtra)
-- Load A in a separate process.
(runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
echoUntilPrompt
loadAndEcho "A.agda")
-- Load B again.
output <- loadAndEcho "B.agda"
-- Restore A.
writeFile "A.agda" moduleA
-- Check the output.
if not ("(agda2-status-action \"Checked\")" `elem` output) ||
any ("Checking A" `isInfixOf`) output
then exitFailure
else exitSuccess
Consider the following workflow:
B.agda
, which importsA.agda
, in (say) Emacs.A.agda
and type-check it by invoking Agda using a shell command.B.agda
in Emacs.In this case you might hope that
A.agda
should not be type-checked again (if the same options are in effect). However, I have observed that, in at least some cases, Agda does type-check the file again instead of loading the interface file.This is a regression, Agda 2.6.1.2 does not have this bug, but Agda 2.6.2 does. Bisection points towards @rwe's commit 7119290686e02c11eff7695bf37c27582577663f ("imports/refact: Combine more conditions in getStoredInterface").
Here is a script that can be used to demonstrate the bug: