8000 Agda re-checks a file with an up-to-date interface file · Issue #7199 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Agda re-checks a file with an up-to-date interface file #7199

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.

Sign up for GitHub

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

Jump to bottom
Closed
nad opened this issue Mar 21, 2024 · 0 comments · Fixed by #7454
Closed

Agda re-checks a file with an up-to-date interface file #7199

nad opened this issue Mar 21, 2024 · 0 comments · Fixed by #7454
Assignees
@nad
Labels
performance Slow type checking, interaction, compilation or execution of Agda programs regression in 2.6.2 Regression that first appeared in Agda 2.6.2 type: bug Issues and pull requests about actual bugs
Milestone
2.7.0.1

Comments

@nad
Copy link
Contributor
nad commented Mar 21, 2024

Consider the following workflow:

  • 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 7119290 ("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
@nad nad added type: bug Issues and pull requests about actual bugs performance Slow type checking, interaction, compilation or execution of Agda programs regression in 2.6.2 Regression that first appeared in Agda 2.6.2 labels Mar 21, 2024
@nad nad added this to the 2.7.0 milestone Mar 21, 2024
@andreasabel andreasabel changed the title Agda type-checks a file with an up-to-date interface file Agda re-checks a file with an up-to-date interface file Mar 21, 2024
@andreasabel andreasabel modified the milestones: 2.7.0, icebox Jul 10, 2024
@nad nad self-assigned this Aug 26, 2024
@nad nad modified the milestones: icebox, 2.7.0.1 Aug 26, 2024
nad added a commit that referenced this issue Aug 26, 2024
@nad
Fixed #7199.
43db35e
@andreasabel andreasabel mentioned this issue Aug 27, 2024
Merged
nad added a commit that referenced this issue Aug 29, 2024
@nad
Fixed #7199.
c6ad583
@nad nad closed this as completed in #7454 Aug 29, 2024
@nad nad closed this as completed in fde357c Aug 29, 2024
andreasabel pushed a commit that referenced this issue Sep 3, 2024
@nad @andreasabel
Fixed #7199.
86eacca
@andreasabel andreasabel mentioned this issue Sep 3, 2024
Merged
andreasabel pushed a commit that referenced this issue Sep 3, 2024
@nad @andreasabel
Fixed #7199.
33f5dfd
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@nad @fredins
Fixed agda#7199.
05f9ddd
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nad nad

Labels
performance Slow type checking, interaction, compilation or execution of Agda programs regression in 2.6.2 Regression that first appeared in Agda 2.6.2 type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.7.0.1
Development

Successfully merging a pull request may close this issue.

Fixed #7199 agda/agda
2 participants
@nad @andreasabel
0