From 75497b298c8459b13c83a6c2c5ba4bd0efb5e662 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Fri, 16 Aug 2024 14:47:38 +0200
Subject: [PATCH 01/30] CI deploy.yml: bump base tag for nightly to v2.7.0

---
 .github/workflows/deploy.yml    | 2 +-
 src/github/workflows/deploy.yml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
index 2b50732d990..b249f6a2535 100644
--- a/.github/workflows/deploy.yml
+++ b/.github/workflows/deploy.yml
@@ -240,7 +240,7 @@ jobs:
       run: |
         gh release delete 'nightly' --repo ${GITHUB_REPOSITORY} --cleanup-tag --yes || true
         ls -R artifacts
-        gh release create 'nightly' artifacts/**/* --repo ${GITHUB_REPOSITORY} --generate-notes --notes-start-tag v2.6.4.3 --prerelease --title "${{ needs.build.outputs.sha }}@master"
+        gh release create 'nightly' artifacts/**/* --repo ${GITHUB_REPOSITORY} --generate-notes --notes-start-tag v2.7.0 --prerelease --title "${{ needs.build.outputs.sha }}@master"
     - env:
         GITHUB_TOKEN: ${{ github.token }}
       if: startsWith(github.ref, 'refs/tags/v')
diff --git a/src/github/workflows/deploy.yml b/src/github/workflows/deploy.yml
index b411f0a8be7..88c5381e52d 100644
--- a/src/github/workflows/deploy.yml
+++ b/src/github/workflows/deploy.yml
@@ -308,7 +308,7 @@ jobs:
       run: |
         gh release delete 'nightly' --repo ${GITHUB_REPOSITORY} --cleanup-tag --yes || true
         ls -R artifacts
-        gh release create 'nightly' artifacts/**/* --repo ${GITHUB_REPOSITORY} --generate-notes --notes-start-tag v2.6.4.3 --prerelease --title "${{ needs.build.outputs.sha }}@master"
+        gh release create 'nightly' artifacts/**/* --repo ${GITHUB_REPOSITORY} --generate-notes --notes-start-tag v2.7.0 --prerelease --title "${{ needs.build.outputs.sha }}@master"
 
     - name: Create a release with the bindist as release assets
       if: startsWith(github.ref, 'refs/tags/v')

From 3fe6d1019e28200b61fa148ac1897d32e05a2cc0 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 12 Aug 2024 16:02:47 +0200
Subject: [PATCH 02/30] Fix internal error for `{-# COMPILE GHC Set1 #-}`

---
 src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs | 3 ++-
 test/Fail/ParseGHCPragma.agda                          | 1 +
 test/Fail/ParseGHCPragma.err                           | 4 ++++
 3 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test/Fail/ParseGHCPragma.agda
 create mode 100644 test/Fail/ParseGHCPragma.err

diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index 2c3e764c529..1407ca40565 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -2463,7 +2463,8 @@ instance ToAbstract C.Pragma where
       Just e  -> do
         let err what = genericError $ "Cannot COMPILE " ++ what ++ " " ++ prettyShow x
         y <- case e of
-          A.Def x             -> return x
+          A.Def' x NoSuffix   -> return x
+          A.Def' x Suffix{}   -> err "name with suffix"
           A.Proj _ p | Just x <- getUnambiguous p -> return x
           A.Proj _ x          -> err "ambiguous projection"
           A.Con c | Just x <- getUnambiguous c -> return x
diff --git a/test/Fail/ParseGHCPragma.agda b/test/Fail/ParseGHCPragma.agda
new file mode 100644
index 00000000000..8cfe2a55d4b
--- /dev/null
+++ b/test/Fail/ParseGHCPragma.agda
@@ -0,0 +1 @@
+{-# COMPILE GHC Set1 #-}
diff --git a/test/Fail/ParseGHCPragma.err b/test/Fail/ParseGHCPragma.err
new file mode 100644
index 00000000000..0ccdbed32af
--- /dev/null
+++ b/test/Fail/ParseGHCPragma.err
@@ -0,0 +1,4 @@
+ParseGHCPragma.agda:1,1-25
+Cannot COMPILE name with suffix Set1
+when scope checking the declaration
+  {-# COMPILE GHC Set1  #-}

From aef9d12bc335c9b57dad080debf25b492d029122 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 12 Aug 2024 16:53:54 +0200
Subject: [PATCH 03/30] Fix internal error on {-# REWRITE Set1 #-}

---
 src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs | 3 ++-
 test/Fail/RewritePragmaSuffix.agda                     | 7 +++++++
 test/Fail/RewritePragmaSuffix.err                      | 4 ++++
 3 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test/Fail/RewritePragmaSuffix.agda
 create mode 100644 test/Fail/RewritePragmaSuffix.err

diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index 1407ca40565..06209b95118 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -2448,7 +2448,8 @@ instance ToAbstract C.Pragma where
    forM xs $ \ x -> do
     e <- toAbstract $ OldQName x Nothing
     case e of
-      A.Def x          -> return [ x ]
+      A.Def' x NoSuffix -> return [ x ]
+      A.Def' x Suffix{} -> genericError $ "REWRITE used on name with suffix"
       A.Proj _ p | Just x <- getUnambiguous p -> return [ x ]
       A.Proj _ x       -> genericError $ "REWRITE used on ambiguous name " ++ prettyShow x
       A.Con c | Just x <- getUnambiguous c -> return [ x ]
diff --git a/test/Fail/RewritePragmaSuffix.agda b/test/Fail/RewritePragmaSuffix.agda
new file mode 100644
index 00000000000..fc0276c97ec
--- /dev/null
+++ b/test/Fail/RewritePragmaSuffix.agda
@@ -0,0 +1,7 @@
+-- Andreas, 2024-08-12
+
+{-# REWRITE Set1 #-}
+
+-- Was: internal error
+-- Expected error:
+-- REWRITE used on name with suffix
diff --git a/test/Fail/RewritePragmaSuffix.err b/test/Fail/RewritePragmaSuffix.err
new file mode 100644
index 00000000000..b91e631f516
--- /dev/null
+++ b/test/Fail/RewritePragmaSuffix.err
@@ -0,0 +1,4 @@
+RewritePragmaSuffix.agda:3,1-21
+REWRITE used on name with suffix
+when scope checking the declaration
+  {-# REWRITE Set1 #-}

From 3822e96e5d1bd16f6573d22a6e6e0f80f142c194 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 12 Aug 2024 17:01:56 +0200
Subject: [PATCH 04/30] Fix internal error with REWRITE on pattern synonym

---
 .../Agda/Syntax/Translation/ConcreteToAbstract.hs   |  1 +
 test/Fail/RewritePragmaPatternSynonym.agda          | 13 +++++++++++++
 test/Fail/RewritePragmaPatternSynonym.err           |  4 ++++
 3 files changed, 18 insertions(+)
 create mode 100644 test/Fail/RewritePragmaPatternSynonym.agda
 create mode 100644 test/Fail/RewritePragmaPatternSynonym.err

diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index 06209b95118..83f578a0ac2 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -2455,6 +2455,7 @@ instance ToAbstract C.Pragma where
       A.Con c | Just x <- getUnambiguous c -> return [ x ]
       A.Con x          -> genericError $ "REWRITE used on ambiguous name " ++ prettyShow x
       A.Var x          -> genericError $ "REWRITE used on parameter " ++ prettyShow x ++ " instead of on a defined symbol"
+      A.PatternSyn{}   -> genericError $ "REWRITE used on pattern synonym"
       _       -> __IMPOSSIBLE__
   toAbstract (C.ForeignPragma _ rb s) = [] <$ addForeignCode (rangedThing rb) s
   toAbstract (C.CompilePragma _ rb x s) = do
diff --git a/test/Fail/RewritePragmaPatternSynonym.agda b/test/Fail/RewritePragmaPatternSynonym.agda
new file mode 100644
index 00000000000..1f9c6ef0a91
--- /dev/null
+++ b/test/Fail/RewritePragmaPatternSynonym.agda
@@ -0,0 +1,13 @@
+-- Andreas, 2024-08-12
+-- Test parsing REWRITE pragma with pattern synonym
+
+data D : Set where
+  c : D
+
+pattern p = c
+
+{-# REWRITE p #-}
+
+-- Was: internal error
+-- Expected error:
+-- REWRITE used on pattern synonym
diff --git a/test/Fail/RewritePragmaPatternSynonym.err b/test/Fail/RewritePragmaPatternSynonym.err
new file mode 100644
index 00000000000..fcd2fe3cbf3
--- /dev/null
+++ b/test/Fail/RewritePragmaPatternSynonym.err
@@ -0,0 +1,4 @@
+RewritePragmaPatternSynonym.agda:9,1-18
+REWRITE used on pattern synonym
+when scope checking the declaration
+  {-# REWRITE p #-}

From 1868da908e6b42d5f3afb7f72637c5b60820c275 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Fri, 16 Aug 2024 11:52:16 +0200
Subject: [PATCH 05/30] Makefile: fix fast-succeed target

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 38b4d881c2b..a6e40b9005e 100644
--- a/Makefile
+++ b/Makefile
@@ -501,7 +501,7 @@ succeed :
 fast-succeed :
 	@$(call decorate, "Suite of successful tests (using agda-fast)", \
 		echo $(shell which $(AGDA_FAST_BIN)) > test/Succeed/exec-tc/executables && \
-		AGDA_FAST_BIN=$(AGDA_FAST_BIN) $(AGDA_FAST_TESTS_BIN) $(AGDA_TESTS_OPTIONS) --regex-include all/Succeed ; \
+		AGDA_BIN=$(AGDA_FAST_BIN) $(AGDA_FAST_TESTS_BIN) $(AGDA_TESTS_OPTIONS) --regex-include all/Succeed ; \
 		rm test/Succeed/exec-tc/executables )
 
 .PHONY : fail ##

From cf5612d71aaeab5611bb18724cdf074b8586757a Mon Sep 17 00:00:00 2001
From: Ulf Norell <ulf.norell@gmail.com>
Date: Thu, 15 Aug 2024 09:27:22 +0200
Subject: [PATCH 06/30] fix #7402: mimer failing on already instantiated goal

---
 src/full/Agda/Mimer/Mimer.hs    | 5 +++--
 test/interaction/Issue7402.agda | 7 +++++++
 test/interaction/Issue7402.in   | 2 ++
 test/interaction/Issue7402.out  | 8 ++++++++
 4 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 test/interaction/Issue7402.agda
 create mode 100644 test/interaction/Issue7402.in
 create mode 100644 test/interaction/Issue7402.out

diff --git a/src/full/Agda/Mimer/Mimer.hs b/src/full/Agda/Mimer/Mimer.hs
index 545cc1359df..19e30394f0c 100644
--- a/src/full/Agda/Mimer/Mimer.hs
+++ b/src/full/Agda/Mimer/Mimer.hs
@@ -724,7 +724,9 @@ runSearch norm options ii rng = withInteractionId ii $ do
                                        , "with args" <+> pretty (instTel inst) ]
 
       -- ctx <- getContextTelescope
-      return metaIds
+      -- #7402: still solve the top-level meta, because we don't have the correct contexts for the
+      --        submetas
+      return [metaId | not $ null metaIds]
     OpenMeta UnificationMeta -> do
       reportSLn "mimer.init" 20 "Interaction point not instantiated."
       return [metaId]
@@ -1123,7 +1125,6 @@ tryLamAbs :: Goal -> Type -> SearchBranch -> SM (Either Expr (Goal, Type, Search
 tryLamAbs goal goalType branch =
   case unEl goalType of
     Pi dom abs -> do
-     e <- isEmptyType (unDom dom)
      isEmptyType (unDom dom) >>= \case -- TODO: Is this the correct way of checking if absurd lambda is applicable?
       True -> do
         let argInf = defaultArgInfo{argInfoOrigin = Inserted} -- domInfo dom
diff --git a/test/interaction/Issue7402.agda b/test/interaction/Issue7402.agda
new file mode 100644
index 00000000000..c95ff387ff0
--- /dev/null
+++ b/test/interaction/Issue7402.agda
@@ -0,0 +1,7 @@
+postulate
+  A : Set
+  x : A
+  f : (P : A → Set) → P x
+
+g : (P : ((A → A) → A) → Set) → P (λ h → h x)
+g P = f (λ y → P ?)
diff --git a/test/interaction/Issue7402.in b/test/interaction/Issue7402.in
new file mode 100644
index 00000000000..97e20f92665
--- /dev/null
+++ b/test/interaction/Issue7402.in
@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 (cmd_autoOne AsIs) ""
diff --git a/test/interaction/Issue7402.out b/test/interaction/Issue7402.out
new file mode 100644
index 00000000000..eec973be30d
--- /dev/null
+++ b/test/interaction/Issue7402.out
@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals, Errors*" "?0 : (A → A) → A _8 : (A → A) → A [ at Issue7402.agda:7,18-19 ] ———— Error ————————————————————————————————————————————————— Failed to solve the following constraints: _8 (y = x) h = h x : A (blocked on _8)" nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "λ z → y")
+((last . 1) . (agda2-goals-action '()))

From 44faba8f31b3d13aebf4213c1f3a053d08d03f20 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Wed, 21 Aug 2024 17:36:19 +0200
Subject: [PATCH 07/30] Remove disclaimer that Agda would not follow the
 Haskell PVP

We intend to do so now!
---
 Agda.cabal | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Agda.cabal b/Agda.cabal
index d2407c6d5c0..e1f9d292e70 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -29,10 +29,6 @@ description:
     This package includes both a command-line program (agda) and an
     Emacs mode. If you want to use the Emacs mode you can set it up by
     running @agda-mode setup@ (see the README).
-    .
-    Note that the Agda package does not follow the package versioning
-    policy, because it is not intended to be used by third-party
-    packages.
 
 tested-with:
     GHC == 9.10.1

From 250e6c51904fcb9926e5518a34092c7e7c58a666 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Thu, 22 Aug 2024 13:41:39 +0200
Subject: [PATCH 08/30] Makefile: increase heap max for GHC 9.10 compiler

---
 Makefile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Makefile b/Makefile
index a6e40b9005e..614b180f3d3 100644
--- a/Makefile
+++ b/Makefile
@@ -87,6 +87,8 @@ ifeq ($(GHC_RTS_OPTS),)
 #
 ifeq ("$(shell $(GHC) --info | grep 'target word size' | cut -d\" -f4)","4")
 GHC_RTS_OPTS := -M2.3G
+else ifeq ($(GHC_VERSION),9.10)
+GHC_RTS_OPTS := -M5G
 else ifeq ($(GHC_VERSION),9.6)
 GHC_RTS_OPTS := -M6G
 else ifeq ($(GHC_VERSION),9.0)

From 33f5dfd53811afe9841a62d71f0096adf15c63c6 Mon Sep 17 00:00:00 2001
From: Nils Anders Danielsson <nad@cse.gu.se>
Date: Mon, 26 Aug 2024 21:58:32 +0200
Subject: [PATCH 09/30] Fixed #7199.

---
 src/full/Agda/Interaction/Imports.hs | 70 +++++++++++++++-------------
 test/interaction/Issue7199.agda      |  3 ++
 test/interaction/Issue7199.hs        | 52 +++++++++++++++++++++
 test/interaction/Issue7199.out       |  8 ++++
 test/interaction/Issue7199/M.agda    |  1 +
 5 files changed, 101 insertions(+), 33 deletions(-)
 create mode 100644 test/interaction/Issue7199.agda
 create mode 100644 test/interaction/Issue7199.hs
 create mode 100644 test/interaction/Issue7199.out
 create mode 100644 test/interaction/Issue7199/M.agda

diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 0e8f16ccfc7..10b26a9bc69 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -635,39 +635,10 @@ getStoredInterface x file msrc = do
 
         reportSLn "import.iface" 5 $ concat ["  ", prettyShow x, " is up-to-date."]
 
-  -- Check if we have cached the module.
-  cachedE <- runExceptT $ maybeToExceptT "the interface has not been decoded" $ MaybeT $
-      lift $ getDecodedModule x
-
-  case cachedE of
-    -- If it's cached ignoreInterfaces has no effect;
-    -- to avoid typechecking a file more than once.
-    Right mi -> do
-      (ifile, hashes) <- getIFileHashesET
-
-      let ifp = filePath $ intFilePath ifile
-      let i = miInterface mi
-
-      -- Make sure the hashes match.
-      let cachedIfaceHash = iFullHash i
-      let fileIfaceHash = snd hashes
-      unless (cachedIfaceHash == fileIfaceHash) $ do
-        lift $ dropDecodedModule x
-        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash
-        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash
-        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp
-        throwError $ concat
-          [ "the cached interface hash (", show cachedIfaceHash, ")"
-          , " does not match interface file (", show fileIfaceHash, ")"
-          ]
-
-      Bench.billTo [Bench.Deserialization] $ do
-        checkSourceHashET (iSourceHash i)
-
-        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)
-        loadDecodedModule file mi
-
-    Left whyNotCached -> withExceptT (\e -> concat [whyNotCached, " and ", e]) $ do
+  let
+    -- Load or reload the interface file, if possible.
+    loadInterfaceFile whyNotCached =
+      withExceptT (\e -> concat [whyNotCached, " and ", e]) $ do
       whenM ignoreAllInterfaces $
         throwError "we're ignoring all interface files"
 
@@ -705,6 +676,39 @@ getStoredInterface x file msrc = do
           , miMode = ModuleTypeChecked
           }
 
+  -- Check if we have cached the module.
+  cachedE <- runExceptT $ maybeToExceptT "the interface has not been decoded" $ MaybeT $
+      lift $ getDecodedModule x
+
+  case cachedE of
+    Left whyNotCached -> loadInterfaceFile whyNotCached
+
+    -- If it's cached ignoreInterfaces has no effect;
+    -- to avoid typechecking a file more than once.
+    Right mi -> do
+      (ifile, hashes) <- getIFileHashesET
+
+      let ifp = filePath $ intFilePath ifile
+      let i = miInterface mi
+
+      -- Make sure the hashes match.
+      let cachedIfaceHash = iFullHash i
+      let fileIfaceHash = snd hashes
+      if cachedIfaceHash /= fileIfaceHash then do
+        lift $ dropDecodedModule x
+        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash
+        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash
+        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp
+        loadInterfaceFile $ concat
+          [ "the cached interface hash (", show cachedIfaceHash, ")"
+          , " does not match interface file (", show fileIfaceHash, ")"
+          ]
+       else Bench.billTo [Bench.Deserialization] $ do
+        checkSourceHashET (iSourceHash i)
+
+        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)
+        loadDecodedModule file mi
+
 -- | Report those given warnings that come from the given module.
 
 reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> [TCWarning] -> m ()
diff --git a/test/interaction/Issue7199.agda b/test/interaction/Issue7199.agda
new file mode 100644
index 00000000000..90dccddf7fe
--- /dev/null
+++ b/test/interaction/Issue7199.agda
@@ -0,0 +1,3 @@
+module Issue7199 where
+
+import Issue7199.M
diff --git a/test/interaction/Issue7199.hs b/test/interaction/Issue7199.hs
new file mode 100644
index 00000000000..9e482a23be2
--- /dev/null
+++ b/test/interaction/Issue7199.hs
@@ -0,0 +1,52 @@
+#!/usr/bin/env runhaskell
+
+{-# LANGUAGE RecordWildCards #-}
+
+import Data.List
+import System.Exit
+
+import RunAgda
+
+moduleM      = "module Issue7199.M where\n"
+moduleMExtra = "postulate A : Set\n"
+
+main :: IO ()
+main = runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
+
+  -- Discard the first prompt.
+  readUntilPrompt
+
+  -- Make sure that Issue7199.M has been defined correctly.
+  writeFile "Issue7199/M.agda" moduleM
+
+  -- Load Issue7199. Discard the output.
+  load "Issue7199.agda"
+  readUntilPrompt
+
+  -- Modify Issue7199.M.
+  writeFile "Issue7199/M.agda" (moduleM ++ moduleMExtra)
+
+  -- Load Issue7199.M in a separate process. Discard the output.
+  (runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
+     readUntilPrompt
+     load "Issue7199/M.agda"
+     readUntilPrompt)
+
+  -- Load Issue7199 again. Store the output.
+  output <- loadAndEcho "Issue7199.agda"
+
+  -- Restore Issue7199.M.
+  writeFile "Issue7199/M.agda" moduleM
+
+  -- Check the output.
+  if not ("(agda2-status-action \"Checked\")" `elem` output)
+  then do
+    putStrLn "The file Issue7199 was not successfully type-checked."
+    exitFailure
+  else if any ("Checking Issue7199.M" `isInfixOf`) output
+  then do
+    putStrLn "The file Issue7199.M was rechecked."
+    exitFailure
+  else do
+    putStrLn "The file Issue7199.M was not rechecked."
+    exitSuccess
diff --git a/test/interaction/Issue7199.out b/test/interaction/Issue7199.out
new file mode 100644
index 00000000000..88e7ca8b836
--- /dev/null
+++ b/test/interaction/Issue7199.out
@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-info-action "*Type-checking*" "Checking Issue7199 (Issue7199.agda). " t)
+(agda2-status-action "Checked")
+(agda2-info-action "*All Done*" "" nil)
+((last . 1) . (agda2-goals-action '()))
+The file Issue7199.M was not rechecked.
diff --git a/test/interaction/Issue7199/M.agda b/test/interaction/Issue7199/M.agda
new file mode 100644
index 00000000000..d837a383034
--- /dev/null
+++ b/test/interaction/Issue7199/M.agda
@@ -0,0 +1 @@
+module Issue7199.M where

From d2ee9e7835664b361959d9c5172e53aecc457fd9 Mon Sep 17 00:00:00 2001
From: AndrasKovacs <puttamalac@gmail.com>
Date: Wed, 21 Aug 2024 15:33:58 +0200
Subject: [PATCH 10/30] Fix #7436: make display forms of imported names
 DeadCode roots

PR 7248# erroneously removed them from the root set. Prior to that,
their scanning was also incomplete, because they were only scanned if
their head symbol was reachable from other roots.
---
 src/full/Agda/Interaction/Imports.hs   | 10 ++-------
 src/full/Agda/TypeChecking/DeadCode.hs | 28 +++++++++++++++++---------
 2 files changed, 20 insertions(+), 18 deletions(-)

diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 10b26a9bc69..6f0c9927d6e 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -1249,7 +1249,7 @@ buildInterface src topLevel = do
 
     let !scope = topLevelScope topLevel
 
-    (!solvedMetas, !definitions) <- eliminateDeadCode scope
+    (!solvedMetas, !definitions, !displayForms) <- eliminateDeadCode scope
     !sig <- set sigDefinitions definitions <$> getSignature
 
     -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
@@ -1257,12 +1257,6 @@ buildInterface src topLevel = do
     -- when expanding a pattern synonym.
     !patsyns <- killRange <$> getPatternSyns
 
-    -- Ulf, 2016-04-12:
-    -- Non-closed display forms are not applicable outside the module anyway,
-    -- and should be dead-code eliminated (#1928).
-    !importedDisplayForms <-
-        HMap.filter (not . null) . HMap.map (filter isClosed) <$> useTC stImportsDisplayForms
-
     !userwarns   <- useTC stLocalUserWarnings
     !importwarn  <- useTC stWarningOnImport
     !syntaxInfo  <- useTC stSyntaxInfo
@@ -1294,7 +1288,7 @@ buildInterface src topLevel = do
           , iInsideScope          = scope
           , iSignature            = sig
           , iMetaBindings         = solvedMetas
-          , iDisplayForms         = importedDisplayForms
+          , iDisplayForms         = displayForms
           , iUserWarnings         = userwarns
           , iImportWarning        = importwarn
           , iBuiltin              = builtin
diff --git a/src/full/Agda/TypeChecking/DeadCode.hs b/src/full/Agda/TypeChecking/DeadCode.hs
index 8d321e01010..ca5e1c4ef9f 100644
--- a/src/full/Agda/TypeChecking/DeadCode.hs
+++ b/src/full/Agda/TypeChecking/DeadCode.hs
@@ -2,7 +2,7 @@
 
 module Agda.TypeChecking.DeadCode (eliminateDeadCode) where
 
-import Control.Monad ((<$!>), filterM)
+import Control.Monad (filterM)
 import Control.Monad.Trans
 
 import Data.Maybe
@@ -30,20 +30,21 @@ import qualified Agda.Utils.HashTable as HT
 --   public interface. We do not compute reachable data precisely, because that
 --   would be very expensive, mainly because of rewrite rules. The following
 --   things are assumed to be "roots":
---     - public names (for definitions and pattern synonyms)
+--     - public definitions
 --     - definitions marked as primitive
 --     - definitions with COMPILE pragma
---     - all parameter sections (because all sections go into interfaces!)
+--     - all pattern synonyms (because currently all of them go into interfaces)
+--     - all parameter sections (because currently all of them go into interfaces)
 --       (see also issues #6931 and #7382)
 --     - local builtins
 --     - all rewrite rules
---   We only ever prune dead metavariables and definitions. The reachable ones
---   are returned from this function.
-eliminateDeadCode :: ScopeInfo -> TCM (RemoteMetaStore, Definitions)
+--     - closed display forms
+--   We only ever prune dead metavariables and definitions. We return the pruned metas,
+--   pruned definitions and closed display forms.
+eliminateDeadCode :: ScopeInfo -> TCM (RemoteMetaStore, Definitions, DisplayForms)
 eliminateDeadCode !scope = Bench.billTo [Bench.DeadCode] $ do
   !sig <- getSignature
   let !defs = sig ^. sigDefinitions
-  !psyns <- getPatternSyns
   !metas <- useR stSolvedMetaStore
 
   -- #2921: Eliminating definitions with attached COMPILE pragmas results in
@@ -63,12 +64,18 @@ eliminateDeadCode !scope = Bench.billTo [Bench.DeadCode] $ do
 
   let !pubModules = publicModules scope
 
+    -- Ulf, 2016-04-12:
+    -- Non-closed display forms are not applicable outside the module anyway,
+    -- and should be dead-code eliminated (#1928).
+  !rootDisplayForms <-
+      HMap.filter (not . null) . HMap.map (filter isClosed) <$> useTC stImportsDisplayForms
+
   let !rootPubNames  = map anameName $ publicNamesOfModules pubModules
   let !rootExtraDefs = mapMaybe extraRootsFilter $ HMap.toList defs
   let !rootRewrites  = sig ^. sigRewriteRules
-
   let !rootModSections = sig ^. sigSections
   !rootBuiltins <- useTC stLocalBuiltins
+  !rootPatSyns  <- getPatternSyns
 
   !seenNames <- liftIO HT.empty :: TCM (HashTable QName ())
   !seenMetas <- liftIO HT.empty :: TCM (HashTable MetaId ())
@@ -80,7 +87,6 @@ eliminateDeadCode !scope = Bench.billTo [Bench.DeadCode] $ do
         Nothing -> do
           HT.insert seenNames x ()
           go (HMap.lookup x defs)
-          go (PSyn <$!> MapS.lookup x psyns)
 
       goMeta :: MetaId -> IO ()
       goMeta !m = HT.lookup seenMetas m >>= \case
@@ -99,11 +105,13 @@ eliminateDeadCode !scope = Bench.billTo [Bench.DeadCode] $ do
       {-# INLINE go #-}
 
   Bench.billTo [Bench.DeadCode, Bench.DeadCodeReachable] $ liftIO $ do
+    go rootDisplayForms
     foldMap goName rootPubNames
     foldMap goName rootExtraDefs
     go rootRewrites
     go rootModSections
     go rootBuiltins
+    foldMap (go . PSyn) rootPatSyns
 
   let filterMeta :: (MetaId, MetaVariable) -> IO (Maybe (MetaId, RemoteMetaVariable))
       filterMeta (!i, !m) = HT.lookup seenMetas i >>= \case
@@ -117,7 +125,7 @@ eliminateDeadCode !scope = Bench.billTo [Bench.DeadCode] $ do
 
   !metas <- liftIO $ HMap.fromList <$> mapMaybeM filterMeta (MapS.toList metas)
   !defs  <- liftIO $ HMap.fromList <$> filterM filterDef (HMap.toList defs)
-  pure (metas, defs)
+  pure (metas, defs, rootDisplayForms)
 
 -- | Returns the instantiation.
 --   Precondition: The instantiation must be of the form @'InstV' inst@.

From 086971e2da2102aadb2521a20e6f3076f2acbcdd Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 2 Sep 2024 14:33:51 +0200
Subject: [PATCH 11/30] Reproducer for issue #7436

---
 test/interaction/Issue7436.agda        | 11 +++++++++++
 test/interaction/Issue7436.out         |  0
 test/interaction/Issue7436.sh          | 12 ++++++++++++
 test/interaction/Issue7436/Base.agda   | 11 +++++++++++
 test/interaction/Issue7436/Import.agda |  5 +++++
 5 files changed, 39 insertions(+)
 create mode 100644 test/interaction/Issue7436.agda
 create mode 100644 test/interaction/Issue7436.out
 create mode 100755 test/interaction/Issue7436.sh
 create mode 100644 test/interaction/Issue7436/Base.agda
 create mode 100644 test/interaction/Issue7436/Import.agda

diff --git a/test/interaction/Issue7436.agda b/test/interaction/Issue7436.agda
new file mode 100644
index 00000000000..b779fdad8de
--- /dev/null
+++ b/test/interaction/Issue7436.agda
@@ -0,0 +1,11 @@
+-- Andreas, 2024-09-02, regression #7436 in dead code removal.
+-- Shrank original reproducer by mechvel.
+
+{-# OPTIONS --no-main #-}
+
+open import Issue7436.Import Set
+
+-- WAS: Internal error (unbound identifier) during compilation,
+-- only reliably reproduceable from the command line.
+
+-- Should succeed.
diff --git a/test/interaction/Issue7436.out b/test/interaction/Issue7436.out
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/interaction/Issue7436.sh b/test/interaction/Issue7436.sh
new file mode 100755
index 00000000000..9ebfb1ddb33
--- /dev/null
+++ b/test/interaction/Issue7436.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+# Andreas, 2024-09-02, issue #7436
+
+AGDA=$1
+
+# First build the interface files:
+$AGDA Issue7436.agda --ignore-interfaces -v0
+
+# The second invocation of agda, asking to compile, crashed with internal error,
+# due to a dangling name that deadcode removal had introduced.
+$AGDA Issue7436.agda --ghc --ghc-dont-call-ghc -v0
diff --git a/test/interaction/Issue7436/Base.agda b/test/interaction/Issue7436/Base.agda
new file mode 100644
index 00000000000..6c066e1caaf
--- /dev/null
+++ b/test/interaction/Issue7436/Base.agda
@@ -0,0 +1,11 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Basic auxiliary definitions for magma-like structures
+------------------------------------------------------------------------
+-- Andreas, 2024-09-02, helper for Issue7436
+
+module Issue7436.Base where
+
+record R : Set where
+  constructor cons
diff --git a/test/interaction/Issue7436/Import.agda b/test/interaction/Issue7436/Import.agda
new file mode 100644
index 00000000000..71415f6dc07
--- /dev/null
+++ b/test/interaction/Issue7436/Import.agda
@@ -0,0 +1,5 @@
+-- Andreas, 2024-09-02, helper for Issue7436
+
+module Issue7436.Import (_ : Set1) where
+
+open import Issue7436.Base public using (cons)

From f51989f5c4afcc400acfb34269fadc9eb8a21897 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Wed, 28 Aug 2024 09:26:17 +0200
Subject: [PATCH 12/30] Revert default to `--no-save-metas`

Agda 2.7.0 defaulted to `--save-metas` which caused performance
regression
- #7452

Thus, we revert to `--no-save-metas` as default.
Closes #7452.
---
 doc/user-manual/tools/command-line-options.rst | 2 +-
 src/full/Agda/Interaction/Options/Base.hs      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/user-manual/tools/command-line-options.rst b/doc/user-manual/tools/command-line-options.rst
index 73b22019e56..c90b5e9b95f 100644
--- a/doc/user-manual/tools/command-line-options.rst
+++ b/doc/user-manual/tools/command-line-options.rst
@@ -1144,7 +1144,7 @@ Other features
      actually saved, and this option is more like an anticipation of possible
      future optimizations.
 
-     Default: :option:`--save-metas`.
+     Default: :option:`--no-save-metas`.
 
 Erasure
 ~~~~~~~
diff --git a/src/full/Agda/Interaction/Options/Base.hs b/src/full/Agda/Interaction/Options/Base.hs
index 429140a9127..a4245a53c4a 100644
--- a/src/full/Agda/Interaction/Options/Base.hs
+++ b/src/full/Agda/Interaction/Options/Base.hs
@@ -425,7 +425,7 @@ data PragmaOptions = PragmaOptions
       --   This is a stronger form of 'optImportSorts'.
   , _optAllowExec                 :: WithDefault 'False
       -- ^ Allow running external @executables@ from meta programs.
-  , _optSaveMetas                 :: WithDefault 'True
+  , _optSaveMetas                 :: WithDefault 'False
       -- ^ Save meta-variables to interface files.
   , _optShowIdentitySubstitutions :: WithDefault 'False
       -- ^ Show identity substitutions when pretty-printing terms

From 8e57b2e4b08e73820dc86bca23c8d0242019f5fe Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 2 Sep 2024 17:44:54 +0200
Subject: [PATCH 13/30] Setup.hs: Fix an error introduced by PR #6988

Wrong: `toIFile pd (ddir </> fp)`.
Correct: `ddir </> toIFile pd fp`.
---
 Setup.hs | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/Setup.hs b/Setup.hs
index 35a0404f4c2..38dda89e787 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -112,14 +112,12 @@ generateInterfaces pd lbi = do
   -- The Agda.Primitive* and Agda.Builtin* modules.
   let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd)
 
-  -- Remove all existing .agdai files.
-  forM_ builtins $ \fp -> do
-    let fullpathi = toIFile pd (ddir </> fp)
-
-        handleExists e | isDoesNotExistError e = return ()
-                       | otherwise             = throwIO e
+  -- The absolute filenames of their interfaces.
+  let interfaces = map ((ddir </>) . toIFile pd) builtins
 
-    removeFile fullpathi `catch` handleExists
+  -- Remove all existing .agdai files.
+  forM_ interfaces $ \ fp -> removeFile fp `catch` \ e ->
+    unless (isDoesNotExistError e) $ throwIO e
 
   -- Type-check all builtin modules (in a single Agda session to take
   -- advantage of caching).

From f4155d2b87a1bfd558bf82b4ec1b8742b84760bb Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 2 Sep 2024 17:48:14 +0200
Subject: [PATCH 14/30] Re #6988: more comments, refactor to allow partial
 application of toIFile

---
 Setup.hs | 35 ++++++++++++++++++++++++++---------
 1 file changed, 26 insertions(+), 9 deletions(-)

diff --git a/Setup.hs b/Setup.hs
index 38dda89e787..8cab6b26310 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -68,21 +68,38 @@ copyHook' pd lbi hooks flags = do
 
 -- Used to add .agdai files to data-files
 expandAgdaExt :: PackageDescription -> FilePath -> [FilePath]
-expandAgdaExt pd fp | takeExtension fp == ".agda" = [ fp, toIFile pd fp ]
-                    | otherwise                   = [ fp ]
+expandAgdaExt pd = \ fp ->
+    -- N.B. using lambda here so that @expandAgdaExt pd@ can be partially evaluated.
+    if takeExtension fp == ".agda" then [ fp, iFile fp ] else [ fp ]
+  where
+  iFile = toIFile pd
 
 version :: PackageDescription -> String
 version = intercalate "." . map show . versionNumbers . pkgVersion . package
 
+-- | This returns @lib/prim@.
+--
 projectRoot :: PackageDescription -> FilePath
-projectRoot pd = takeDirectory agdaLibFile where
+projectRoot pd = takeDirectory agdaLibFile
+  where
   [agdaLibFile] = filter ((".agda-lib" ==) . takeExtension) $ dataFiles pd
 
-toIFile :: PackageDescription -> FilePath -> FilePath
-toIFile pd file = buildDir </> fileName where
+-- | Turns e.g. @lib/prim/Agda/Primitive.agda@
+--   into @lib/prim/_build/2.7.0/agda/Agda/Primitive.agdai@.
+--
+--   An absolute path will be returned unchanged.
+toIFile ::
+     PackageDescription
+  -> FilePath            -- ^ Should be a relative path.
+  -> FilePath            -- ^ Then this is also a relative path.
+toIFile pd = (buildDir </>) . fileName
+  where
   root = projectRoot pd
+    -- e.g. root     = "lib/prim"
   buildDir = root </> "_build" </> version pd </> "agda"
-  fileName = makeRelative root $ replaceExtension file ".agdai"
+    -- e.g. buildDir = "lib/prim/_build/2.7.0/agda"
+  fileName file = makeRelative root $ replaceExtension file ".agdai"
+    -- e.g. fileName "lib/prim/Agda/Primitive.agda" = "Agda/Primitive.agdai"
 
 -- Andreas, 2019-10-21, issue #4151:
 -- skip the generation of interface files with program suffix "-quicker"
@@ -102,11 +119,11 @@ generateInterfaces pd lbi = do
   let bdir = buildDir lbi
       agda = bdir </> "agda" </> "agda" <.> agdaExeExtension
 
+  -- We should be in the current directory root of the cabal package
+  -- and data-files reside in src/data relative to this.
+  --
   ddir <- makeAbsolute $ "src" </> "data"
 
-  -- assuming we want to type check all .agda files in data-files
-  -- current directory root of the package.
-
   putStrLn "Generating Agda library interface files..."
 
   -- The Agda.Primitive* and Agda.Builtin* modules.

From 03f5abe8404c52f29020f75a877f68343801cf3f Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 2 Sep 2024 17:49:16 +0200
Subject: [PATCH 15/30] Re #7455: Setup.hs: catch when Agda did not produce all
 agdai files

The cause of #7455 is atm still unclear to me, but this patch adds a
check that all .agdai files we ask cabal to copy do actually exist.
If they do not, we skip the copy step.

Rationale: Unless the user does a sudo install, copying the interface files isn't
essential at the time of installation.
---
 Setup.hs | 42 ++++++++++++++++++++++++++++++++++--------
 1 file changed, 34 insertions(+), 8 deletions(-)

diff --git a/Setup.hs b/Setup.hs
index 8cab6b26310..10285cf7e1f 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,7 +1,10 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-import Data.List
-import Data.Maybe
+import Data.Functor ( (<&>) )
+import Data.List    ( intercalate )
+import Data.Maybe   ( catMaybes )
 
 import Distribution.Simple
 import Distribution.Simple.LocalBuildInfo
@@ -11,7 +14,7 @@ import Distribution.PackageDescription
 import Distribution.System ( buildPlatform )
 
 import System.FilePath
-import System.Directory (makeAbsolute, removeFile)
+import System.Directory (doesFileExist, makeAbsolute, removeFile)
 import System.Environment (getEnvironment)
 import System.Process
 import System.Exit
@@ -166,19 +169,19 @@ generateInterfaces pd lbi = do
         , [ "EOF" ]
         ]
   let onIOError (e :: IOException) = False <$ do
-        putStr $ unlines $ concat
-          [ [ "*** Warning!"
-            , "*** Could not generate Agda library interface files."
+        warn $ concat
+          [ [ "*** Could not generate Agda library interface files."
             , "*** Reason:"
             , show e
             , "*** The attempted call to Agda was:"
             ]
           , callLines
-          , [ "*** Ignoring error, continuing installation..." ]
           ]
   env <- getEnvironment
   handle onIOError $ do
-    True <$ readCreateProcess
+
+    -- Generate interface files via a call to Agda.
+    readCreateProcess
       (proc agda agdaArgs)
         { delegate_ctlc = True
                           -- Make Agda look for data files in a
@@ -187,6 +190,29 @@ generateInterfaces pd lbi = do
         }
       (unlines loadBuiltinCmds)
 
+    -- Check whether all interface files have been generated.
+    missing <- catMaybes <$> forM interfaces \ f ->
+      doesFileExist f <&> \case
+        True  -> Nothing
+        False -> Just f
+
+    -- Warn if not all interface files have been generated, but don't crash.
+    -- This might help with issue #7455.
+    let success = null missing
+    unless success $ warn $ concat
+      [ [ "*** Agda failed to generate the following library interface files:" ]
+      , missing
+      ]
+    return success
+
+warn :: [String] -> IO ()
+warn msgs = putStr $ unlines $ concat
+    [ [ "*** Warning!" ]
+    , msgs
+    , [ "*** Ignoring error, continuing installation..." ]
+    ]
+
+
 
 agdaExeExtension :: String
 agdaExeExtension = exeExtension buildPlatform

From a7e979986e7b7b531d82086f9bf059dec546532e Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 3 Sep 2024 11:35:48 +0200
Subject: [PATCH 16/30] Change Agda version to 2.7.0.1

---
 Agda.cabal                            | 4 ++--
 CITATION.cff                          | 4 ++--
 doc/user-manual/conf.py               | 2 +-
 mk/versions.mk                        | 2 +-
 src/data/emacs-mode/agda2-mode-pkg.el | 2 +-
 src/data/emacs-mode/agda2-mode.el     | 2 +-
 src/data/latex/agda.sty               | 2 +-
 src/size-solver/size-solver.cabal     | 2 +-
 test/Fail/Issue1963MagicWith.err      | 2 +-
 test/Fail/Issue206.err                | 2 +-
 test/Fail/Issue2763.err               | 2 +-
 test/Fail/Issue2771.err               | 2 +-
 test/Fail/Issue530.err                | 2 +-
 test/Fail/Issue5805.err               | 2 +-
 test/Fail/MagicWith.err               | 2 +-
 test/interaction/Debug.out            | 2 +-
 test/interaction/Issue1244a.out       | 2 +-
 test/interaction/Issue1244b.out       | 2 +-
 test/interaction/Issue6261.out        | 8 ++++----
 19 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/Agda.cabal b/Agda.cabal
index e1f9d292e70..409f44cf2cd 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,6 +1,6 @@
 cabal-version:   2.4
 name:            Agda
-version:         2.7.0
+version:         2.7.0.1
 build-type:      Custom
 license:         MIT
 license-file:    LICENSE
@@ -156,7 +156,7 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/agda/agda.git
-  tag:      v2.7.0
+  tag:      v2.7.0.1
 
 -- Build flags
 ---------------------------------------------------------------------------
diff --git a/CITATION.cff b/CITATION.cff
index 886b296f438..a449ea864e4 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
 authors:
 - name: "Agda Developers"
 title: "Agda"
-version: 2.7.0
-license-url: "https://agda.readthedocs.io/en/v2.7.0/team.html"
+version: 2.7.0.1
+license-url: "https://agda.readthedocs.io/en/v2.7.0.1/team.html"
 url: "https://agda.readthedocs.io/"
diff --git a/doc/user-manual/conf.py b/doc/user-manual/conf.py
index 8f7c2fb3124..a5c1c166f65 100644
--- a/doc/user-manual/conf.py
+++ b/doc/user-manual/conf.py
@@ -24,7 +24,7 @@
 author = u'Agda Developers'
 
 # The short X.Y version
-version = '2.7.0'
+version = '2.7.0.1'
 # The full version, including alpha/beta/rc tags
 release = version
 
diff --git a/mk/versions.mk b/mk/versions.mk
index c73f4dfa7f6..227b7cbcdf7 100644
--- a/mk/versions.mk
+++ b/mk/versions.mk
@@ -1,3 +1,3 @@
 # Agda version.
 # This is incremented via the script src/release-tools/change-version.bash
-VERSION=2.7.0
+VERSION=2.7.0.1
diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el
index 63623a6a2b3..ecc214dd676 100644
--- a/src/data/emacs-mode/agda2-mode-pkg.el
+++ b/src/data/emacs-mode/agda2-mode-pkg.el
@@ -1,3 +1,3 @@
-(define-package "agda2-mode" "2.7.0"
+(define-package "agda2-mode" "2.7.0.1"
   "interactive development for Agda, a dependently typed functional programming language"
   '((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index b40eb0831d5..5e8b9429a4a 100644
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -28,7 +28,7 @@
 
 ;;; Code:
 
-(defvar agda2-version "2.7.0"
+(defvar agda2-version "2.7.0.1"
   "The version of the Agda mode.
 Note that the same version of the Agda executable must be used.")
 
diff --git a/src/data/latex/agda.sty b/src/data/latex/agda.sty
index a5775e220c0..c8d5b7e3c85 100644
--- a/src/data/latex/agda.sty
+++ b/src/data/latex/agda.sty
@@ -6,7 +6,7 @@
 % !!! NOTE: when you make changes to this file, bump the date. !!!
 % !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
 \ProvidesPackage{agda}
-  [2021/07/14 version 2.7.0 Formatting LaTeX generated by Agda]
+  [2021/07/14 version 2.7.0.1 Formatting LaTeX generated by Agda]
 
 \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
                 calc, environ, xparse, xkeyval}
diff --git a/src/size-solver/size-solver.cabal b/src/size-solver/size-solver.cabal
index 2faaec9f0aa..17703e33c36 100644
--- a/src/size-solver/size-solver.cabal
+++ b/src/size-solver/size-solver.cabal
@@ -31,7 +31,7 @@ executable size-solver
   hs-source-dirs: .
   main-is:        Main.hs
   build-depends:
-    Agda == 2.7.0
+    Agda == 2.7.0.1
     , base       >= 4.12.0.0 && < 5
     , containers >= 0.5.7.1  && < 0.8
     , mtl        >= 2.2.1    && < 2.4
diff --git a/test/Fail/Issue1963MagicWith.err b/test/Fail/Issue1963MagicWith.err
index 515aff2f81f..0f408c1609d 100644
--- a/test/Fail/Issue1963MagicWith.err
+++ b/test/Fail/Issue1963MagicWith.err
@@ -3,4 +3,4 @@ p .proj₁ != w of type Nat
 when checking that the type
 (p : Σ Nat IsZero) (w : Nat) → F w (p .proj₂) of the generated with
 function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/Fail/Issue206.err b/test/Fail/Issue206.err
index 2cae9dbefce..73d53af5f5f 100644
--- a/test/Fail/Issue206.err
+++ b/test/Fail/Issue206.err
@@ -2,4 +2,4 @@ Issue206.agda:12,1-19
 w != i of type I
 when checking that the type (w : I) (p : P w) (q : Q p) → Set₁ of
 the generated with function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/Fail/Issue2763.err b/test/Fail/Issue2763.err
index c7434261c94..8c8a25e868f 100644
--- a/test/Fail/Issue2763.err
+++ b/test/Fail/Issue2763.err
@@ -2,4 +2,4 @@ Issue2763.agda:15,1-19
 a != w of type A
 when checking that the type ⊤ → (w : A) → G w b of the generated
 with function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/Fail/Issue2771.err b/test/Fail/Issue2771.err
index 0a9b242da5d..437c06c85e8 100644
--- a/test/Fail/Issue2771.err
+++ b/test/Fail/Issue2771.err
@@ -3,4 +3,4 @@ Issue2771.agda:15,1-19
 when checking that the type
 (ind : IndexL) → ⊤ → (w : IndexL) → ¬ord-morph w (pres-¬ord ind) of
 the generated with function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/Fail/Issue530.err b/test/Fail/Issue530.err
index e4acaf7fb13..b82f73030e4 100644
--- a/test/Fail/Issue530.err
+++ b/test/Fail/Issue530.err
@@ -2,4 +2,4 @@ Issue530.agda:20,1-10
 k a != w of type Unit
 when checking that the type (w : Unit) → F w p of the generated
 with function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/Fail/Issue5805.err b/test/Fail/Issue5805.err
index ed8d863e902..844e2adbe01 100644
--- a/test/Fail/Issue5805.err
+++ b/test/Fail/Issue5805.err
@@ -8,4 +8,4 @@ when checking that the type
 (ff≡f : (_53 ∘ _53) ≡ _53) →
 ?1 (ff≡f = ff≡f) (λ x → _53 (_53 x)) ≡ ?1 (ff≡f = ff≡f) _53 → Set
 of the generated with function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/Fail/MagicWith.err b/test/Fail/MagicWith.err
index a10b3d1a883..0b35c043818 100644
--- a/test/Fail/MagicWith.err
+++ b/test/Fail/MagicWith.err
@@ -3,4 +3,4 @@ fst p != w of type Nat
 when checking that the type
 (p : Nat × IsZero) (w : Nat) → F w (snd p) of the generated with
 function is well-formed
-(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions)
+(https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#ill-typed-with-abstractions)
diff --git a/test/interaction/Debug.out b/test/interaction/Debug.out
index ec17fafae23..f2e8c79a97b 100644
--- a/test/interaction/Debug.out
+++ b/test/interaction/Debug.out
@@ -3,7 +3,7 @@
 (agda2-highlight-clear)
 (agda2-verbose "Scope checking Agda.Primitive ")
 (agda2-verbose "Building interface... ")
-(agda2-verbose "Writing interface file _build/2.7.0/agda/Debug.agdai. ")
+(agda2-verbose "Writing interface file _build/2.7.0.1/agda/Debug.agdai. ")
 (agda2-verbose "Wrote interface file. ")
 (agda2-verbose "Accumulated statistics. ")
 (agda2-verbose "Finished Debug. ")
diff --git a/test/interaction/Issue1244a.out b/test/interaction/Issue1244a.out
index e3e0afb530a..f52116b8754 100644
--- a/test/interaction/Issue1244a.out
+++ b/test/interaction/Issue1244a.out
@@ -6,4 +6,4 @@
 (agda2-highlight-load-and-delete-action)
 (agda2-status-action "")
 (agda2-status-action "")
-(agda2-info-action "*Agda Version*" "Agda version 2.7.0" nil)
+(agda2-info-action "*Agda Version*" "Agda version 2.7.0.1" nil)
diff --git a/test/interaction/Issue1244b.out b/test/interaction/Issue1244b.out
index 4243a104289..677782882b1 100644
--- a/test/interaction/Issue1244b.out
+++ b/test/interaction/Issue1244b.out
@@ -1,2 +1,2 @@
 (agda2-status-action "")
-(agda2-info-action "*Agda Version*" "Agda version 2.7.0" nil)
+(agda2-info-action "*Agda Version*" "Agda version 2.7.0.1" nil)
diff --git a/test/interaction/Issue6261.out b/test/interaction/Issue6261.out
index 046fdd61c82..88124451228 100644
--- a/test/interaction/Issue6261.out
+++ b/test/interaction/Issue6261.out
@@ -15,10 +15,10 @@
 (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
-(agda2-info-action "*Type-checking*" "Loading Issue6261 (_build/2.7.0/agda/Issue6261.agdai). " t)
-(agda2-info-action "*Type-checking*" " Loading Issue6261b (_build/2.7.0/agda/Issue6261b.agdai). " t)
-(agda2-info-action "*Type-checking*" " Loading Issue6261c (_build/2.7.0/agda/Issue6261c.agdai). " t)
-(agda2-info-action "*Type-checking*" " Loading Issue6261a (_build/2.7.0/agda/Issue6261a.agdai). " t)
+(agda2-info-action "*Type-checking*" "Loading Issue6261 (_build/2.7.0.1/agda/Issue6261.agdai). " t)
+(agda2-info-action "*Type-checking*" " Loading Issue6261b (_build/2.7.0.1/agda/Issue6261b.agdai). " t)
+(agda2-info-action "*Type-checking*" " Loading Issue6261c (_build/2.7.0.1/agda/Issue6261c.agdai). " t)
+(agda2-info-action "*Type-checking*" " Loading Issue6261a (_build/2.7.0.1/agda/Issue6261a.agdai). " t)
 (agda2-status-action "Checked")
 (agda2-info-action "*All Done*" "" nil)
 ((last . 1) . (agda2-goals-action '()))

From d79313c9e3bb3c8eb5bb79360cbd39d2cde1363b Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 3 Sep 2024 11:44:15 +0200
Subject: [PATCH 17/30] Move CHANGELOG.md for 2.7.0 to
 doc/release-notes/2.7.0.md

---
 CHANGELOG.md => doc/release-notes/2.7.0.md | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename CHANGELOG.md => doc/release-notes/2.7.0.md (100%)

diff --git a/CHANGELOG.md b/doc/release-notes/2.7.0.md
similarity index 100%
rename from CHANGELOG.md
rename to doc/release-notes/2.7.0.md

From de0af8a9221d9388c8d3e2dbbe75ce0302131612 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 3 Sep 2024 12:11:19 +0200
Subject: [PATCH 18/30] Changelog for Agda 2.7.0.1

---
 CHANGELOG.md | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 CHANGELOG.md

diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 00000000000..d6ca9e363e8
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,60 @@
+Release notes for Agda version 2.7.0.1
+======================================
+
+This is a minor release of Agda fixing some bugs and regressions.
+
+Installation
+------------
+
+* During installation, Agda type-checks its built-in modules and installs the generated `.agdai` files.
+  Should the generation for (some of) these files fail, the names of the missing ones are now printed,
+  but installation continues nevertheless ([PR #7465](https://github.com/agda/agda/pull/7465)).
+  Rationale: installation of these files is only crucial when installing Agda in super-user mode.
+
+* Agda supports GHC versions 8.6.5 to 9.10.1.
+
+Pragmas and options
+-------------------
+
+* The release notes of 2.7.0 claimed that the option `--exact-split` was now on by default
+  ([Issue #7443](https://github.com/agda/agda/issues/7443)).
+  This is actually not the case, the documentation has been suitably reverted.
+
+* Default option `--save-metas` has been reverted to `--no-save-metas` because of performance regressions
+  ([Issue #7452](https://github.com/agda/agda/issues/7452)).
+
+Bug fixes
+---------
+
+* Fixed an internal error related to interface files
+  ([Issue #7436](https://github.com/agda/agda/issues/7436)).
+
+* Fixed an internal error in Mimer
+  ([Issue #7402](https://github.com/agda/agda/issues/7402)).
+
+* Fixed a regression causing needless re-checking of files
+  ([Issue #7199](https://github.com/agda/agda/issues/7199)).
+
+List of closed issues
+---------------------
+
+For 2.7.0.1, the following issues were
+[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.7.0.1+is%3Aclosed)
+(see [bug tracker](https://github.com/agda/agda/issues)):
+
+- [Issue #7199](https://github.com/agda/agda/issues/7199): Agda re-checks a file with an up-to-date interface file
+- [Issue #7402](https://github.com/agda/agda/issues/7402): Mimer internal error in hole with constraint
+- [Issue #7436](https://github.com/agda/agda/issues/7436): Code only reachable from display forms not serialised in Agda 2.7.0
+- [Issue #7443](https://github.com/agda/agda/issues/7443): `--exact-split` is not default in 2.7.0, contrary to claims
+- [Issue #7452](https://github.com/agda/agda/issues/7452): Performance regression caused by making `--save-metas` the default
+- [Issue #7455](https://github.com/agda/agda/issues/7455): Both stack and cabal fail to install Agda
+
+These pull requests were merged for 2.7.0.1:
+
+- [PR #7427](https://github.com/agda/agda/issues/7427): #7402: mimer failing on higher order goal
+- [PR #7444](https://github.com/agda/agda/issues/7444): Fix #7436: make display forms of imported names DeadCode roots
+- [PR #7445](https://github.com/agda/agda/issues/7445): Remove disclaimer that Agda would not follow the Haskell PVP
+- [PR #7454](https://github.com/agda/agda/issues/7454): Fixed #7199
+- [PR #7456](https://github.com/agda/agda/issues/7456): Actually, --exact-split is not really on by default
+- [PR #7457](https://github.com/agda/agda/issues/7457): Revert default to `--no-save-metas`
+- [PR #7465](https://github.com/agda/agda/issues/7465): Re #7455: Setup.hs: catch when Agda did not produce (all) agdai files

From 74fc953d0f3e0b66ffbf0131da9127aaa73d3cb8 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 3 Sep 2024 11:12:04 +0200
Subject: [PATCH 19/30] Bump standard and cubical library submodules

---
 cubical | 2 +-
 std-lib | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/cubical b/cubical
index ba0a56264b0..e2cf0ab7ced 160000
--- a/cubical
+++ b/cubical
@@ -1 +1 @@
-Subproject commit ba0a56264b0501eb02056d7fb860cb185e5c65f2
+Subproject commit e2cf0ab7ced7ea57685b138d28761eac245fd327
diff --git a/std-lib b/std-lib
index 96d44779bdd..561f5b9f90a 160000
--- a/std-lib
+++ b/std-lib
@@ -1 +1 @@
-Subproject commit 96d44779bdd34e61624c2fe5ae161df223748238
+Subproject commit 561f5b9f90a1103d45c849d11e41f24583ef4ca7

From e18f231ced78462c67eeba090c5574bbf27adf60 Mon Sep 17 00:00:00 2001
From: Rodrigo Mesquita <rodrigo.m.mesquita@gmail.com>
Date: Wed, 4 Sep 2024 15:42:42 +0100
Subject: [PATCH 20/30] setup: Don't assume exe is built on --lib

Cabal-3.12 introduces a breaking change which broke `cabal install --lib Agda`.

The reason is that previously, Cabal, for a Custom-build-type package,
would /always/ build the executable, even if only the library was
requested, and Agda's Setup.hs copyHook expects the executable to
/always/ be available to compile the Agda standard lib. Now, Cabal won't
build the executable if it is not required, so Agda's assumption will
cause a crash when the executable isn't built.

The fix is simple: don't try to compile the Agda standard library if
only the Agda Haskell library was requested, since only when installing
the executable does the agda standard library need to be installed.

Co-authored-by: @sheaf
Co-authored-by: @andreasabel
---
 Setup.hs | 23 ++++++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

diff --git a/Setup.hs b/Setup.hs
index 10285cf7e1f..7064a953891 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
@@ -45,11 +46,13 @@ copyHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> CopyFlags -> I
 copyHook' pd lbi hooks flags = do
   -- Copy library and executable etc.
   copyHook simpleUserHooks pd lbi hooks flags
-  unless (skipInterfaces lbi) $ do
+  if wantInterfaces flags && not (skipInterfaces lbi) then do
     -- Generate .agdai files.
     success <- generateInterfaces pd lbi
     -- Copy again, now including the .agdai files.
     when success $ copyHook simpleUserHooks pd' lbi hooks flags
+  else
+    putStrLn "Skipping generation of Agda core library interface files"
   where
   pd' = pd
     { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd
@@ -69,6 +72,20 @@ copyHook' pd lbi hooks flags = do
     -- , extraDocFiles = []
     }
 
+-- We only want to write interfaces if installing the executable.
+-- If we're installing *just* the library, the interface files are not needed
+-- and, most importantly, the executable will not be available to be run (cabal#10235)
+wantInterfaces :: CopyFlags -> Bool
+wantInterfaces _flags = do
+#if MIN_VERSION_Cabal(3,11,0)
+    any isAgdaExe (copyArgs _flags)
+      where
+        isAgdaExe "exe:agda" = True
+        isAgdaExe _ = False
+#else
+  True
+#endif
+
 -- Used to add .agdai files to data-files
 expandAgdaExt :: PackageDescription -> FilePath -> [FilePath]
 expandAgdaExt pd = \ fp ->
@@ -114,6 +131,8 @@ skipInterfaces lbi = fromPathTemplate (progSuffix lbi) == "-quicker"
 generateInterfaces :: PackageDescription -> LocalBuildInfo -> IO Bool
 generateInterfaces pd lbi = do
 
+  putStrLn "Generating Agda core library interface files..."
+
   -- for debugging, these are examples how you can inspect the flags...
   -- print $ flagAssignment lbi
   -- print $ fromPathTemplate $ progSuffix lbi
@@ -127,8 +146,6 @@ generateInterfaces pd lbi = do
   --
   ddir <- makeAbsolute $ "src" </> "data"
 
-  putStrLn "Generating Agda library interface files..."
-
   -- The Agda.Primitive* and Agda.Builtin* modules.
   let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd)
 

From 67d444a261c48b22b6c1c32e674c26225bf115d1 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Sat, 7 Sep 2024 14:09:26 +0200
Subject: [PATCH 21/30] [ fix #7442 ] Move check for erasure from
 isEtaRecordDef back to isEtaRecord

---
 src/full/Agda/TypeChecking/Empty.hs   |  2 +-
 src/full/Agda/TypeChecking/Records.hs | 19 ++++++++-----------
 test/Succeed/Issue7442-M.agda         |  8 ++++++++
 test/Succeed/Issue7442.agda           |  6 ++++++
 4 files changed, 23 insertions(+), 12 deletions(-)
 create mode 100644 test/Succeed/Issue7442-M.agda
 create mode 100644 test/Succeed/Issue7442.agda

diff --git a/src/full/Agda/TypeChecking/Empty.hs b/src/full/Agda/TypeChecking/Empty.hs
index 8b102b5757b..4e3d8c329f6 100644
--- a/src/full/Agda/TypeChecking/Empty.hs
+++ b/src/full/Agda/TypeChecking/Empty.hs
@@ -100,7 +100,7 @@ checkEmptyType range t = do
 
     -- If t is a record type, see if any of the field types is empty
     Right (r, pars, def) -> do
-      ifNotM (isEtaRecordDef def) (return $ Left Fail) $
+      if not (isEtaRecordDef def) then return $ Left Fail else
          void <$> do checkEmptyTel range $ _recTel def `apply` pars
 
 -- | Check whether one of the types in the given telescope is constructor-less
diff --git a/src/full/Agda/TypeChecking/Records.hs b/src/full/Agda/TypeChecking/Records.hs
index f0b8e2addf2..c29b1acf414 100644
--- a/src/full/Agda/TypeChecking/Records.hs
+++ b/src/full/Agda/TypeChecking/Records.hs
@@ -447,17 +447,14 @@ eliminateType' err hd t (e : es) = case e of
 isEtaRecord :: HasConstInfo m => QName -> m Bool
 isEtaRecord r = do
   isRecord r >>= \case
-    Nothing -> return False
-    Just r -> isEtaRecordDef r
-
-isEtaRecordDef :: HasConstInfo m => RecordData -> m Bool
-isEtaRecordDef r
-  | _recEtaEquality r /= YesEta = return False
-  | otherwise = do
+    Just r | isEtaRecordDef r -> do
      constructorQ <- getQuantity <$> getConstInfo (conName (_recConHead r))
      currentQ     <- viewTC eQuantity
      return $ constructorQ `moreQuantity` currentQ
+    _ -> return False
 
+isEtaRecordDef :: RecordData -> Bool
+isEtaRecordDef r = _recEtaEquality r == YesEta
 
 {-# SPECIALIZE isEtaCon :: QName -> TCM Bool #-}
 isEtaCon :: HasConstInfo m => QName -> m Bool
@@ -467,7 +464,7 @@ isEtaCon c = isJust <$> isEtaRecordConstructor c
 isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
 isEtaOrCoinductiveRecordConstructor c =
   caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) ->
-    isEtaRecordDef def `or2M`
+    pure (isEtaRecordDef def) `or2M`
       return (_recInduction def /= Just Inductive)
       -- If in doubt about coinductivity, then yes.
 
@@ -500,7 +497,7 @@ isRecordConstructor c = getConstInfo' c >>= \case
 isEtaRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, RecordData))
 isEtaRecordConstructor c = isRecordConstructor c >>= \case
   Nothing -> return Nothing
-  Just (d, def) -> ifM (isEtaRecordDef def) (return $ Just (d, def)) (return Nothing)
+  Just (d, def) -> if isEtaRecordDef def then return $ Just (d, def) else return Nothing
 
 -- | Turn off eta for unguarded recursive records.
 --   Projections do not preserve guardedness.
@@ -576,7 +573,7 @@ expandRecordVar i gamma0 = do
           " since its type " <+> prettyTCM a <+>
           " is not a record type"
         return Nothing
-  caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> isEtaRecordDef def >>= \case
+  caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> case isEtaRecordDef def of
     False -> return Nothing
     True  -> Just <$> do
       -- Get the record fields @Γ₁ ⊢ tel@ (@tel = Γ'@).
@@ -928,7 +925,7 @@ isSingletonType' regardIrrelevance t rs = do
         record :: m (Maybe Term)
         record = runMaybeT $ do
           (r, ps, def) <- MaybeT $ isRecordType t
-          guardM $ isEtaRecordDef def
+          guard $ isEtaRecordDef def
           abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)
 
         -- Slightly harder case: η for Sub {level} tA phi elt.
diff --git a/test/Succeed/Issue7442-M.agda b/test/Succeed/Issue7442-M.agda
new file mode 100644
index 00000000000..f781614e915
--- /dev/null
+++ b/test/Succeed/Issue7442-M.agda
@@ -0,0 +1,8 @@
+
+{-# OPTIONS --erasure --cubical #-}
+
+data ⊥ : Set where
+
+record R : Set where
+  field
+    f : ⊥
diff --git a/test/Succeed/Issue7442.agda b/test/Succeed/Issue7442.agda
new file mode 100644
index 00000000000..bac20901587
--- /dev/null
+++ b/test/Succeed/Issue7442.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --erasure --erased-cubical #-}
+
+open import Issue7442-M
+
+f : R → ⊥
+f ()

From a6fb97f24bf8536e70ff9dec9647bddc9cf69fb3 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Sun, 8 Sep 2024 11:40:36 +0200
Subject: [PATCH 22/30] Bump std-lib to latest (v2.1.1) and cubical to latest

---
 cubical | 2 +-
 std-lib | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/cubical b/cubical
index e2cf0ab7ced..760a894b127 160000
--- a/cubical
+++ b/cubical
@@ -1 +1 @@
-Subproject commit e2cf0ab7ced7ea57685b138d28761eac245fd327
+Subproject commit 760a894b127d0e0c4d62c82725840ebe3b388a0e
diff --git a/std-lib b/std-lib
index 561f5b9f90a..7069d03ecba 160000
--- a/std-lib
+++ b/std-lib
@@ -1 +1 @@
-Subproject commit 561f5b9f90a1103d45c849d11e41f24583ef4ca7
+Subproject commit 7069d03ecba300e321edfc3a8502608db0deb7ac

From 3a67df5cac97642a49702a783f52d05f4b2e0418 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Sun, 8 Sep 2024 15:14:47 +0200
Subject: [PATCH 23/30] Update Changelog for Agda 2.7.0.1

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d6ca9e363e8..7d4abff3f53 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,7 @@ Installation
 ------------
 
 * During installation, Agda type-checks its built-in modules and installs the generated `.agdai` files.
+  (This step is now skipped when the Agda executable is not installed, e.g. `cabal install --lib Agda`.)
   Should the generation for (some of) these files fail, the names of the missing ones are now printed,
   but installation continues nevertheless ([PR #7465](https://github.com/agda/agda/pull/7465)).
   Rationale: installation of these files is only crucial when installing Agda in super-user mode.
@@ -45,6 +46,7 @@ For 2.7.0.1, the following issues were
 - [Issue #7199](https://github.com/agda/agda/issues/7199): Agda re-checks a file with an up-to-date interface file
 - [Issue #7402](https://github.com/agda/agda/issues/7402): Mimer internal error in hole with constraint
 - [Issue #7436](https://github.com/agda/agda/issues/7436): Code only reachable from display forms not serialised in Agda 2.7.0
+- [Issue #7442](https://github.com/agda/agda/issues/7442): Regression: emptiness check fails when erased constructors are involved
 - [Issue #7443](https://github.com/agda/agda/issues/7443): `--exact-split` is not default in 2.7.0, contrary to claims
 - [Issue #7452](https://github.com/agda/agda/issues/7452): Performance regression caused by making `--save-metas` the default
 - [Issue #7455](https://github.com/agda/agda/issues/7455): Both stack and cabal fail to install Agda
@@ -58,3 +60,6 @@ These pull requests were merged for 2.7.0.1:
 - [PR #7456](https://github.com/agda/agda/issues/7456): Actually, --exact-split is not really on by default
 - [PR #7457](https://github.com/agda/agda/issues/7457): Revert default to `--no-save-metas`
 - [PR #7465](https://github.com/agda/agda/issues/7465): Re #7455: Setup.hs: catch when Agda did not produce (all) agdai files
+- [PR #7471](https://github.com/agda/agda/issues/7471): setup: Don't assume exe is built on --lib
+- [PR #7475](https://github.com/agda/agda/issues/7475): Hotfix for #7442
+- [PR #7476](https://github.com/agda/agda/issues/7476): Bump std-lib to latest (v2.1.1) and cubical to latest

From 794f5c9d06da6e60dc1ea2ee5f1ce00ca2f3c298 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia?= <me@amelia.how>
Date: Tue, 10 Sep 2024 07:13:11 -0300
Subject: [PATCH 24/30] Match display forms in the right context (#7480)

---
 src/full/Agda/TypeChecking/DisplayForm.hs | 27 ++++++++++++++++++-----
 test/Fail/LiftDisplayIntermediate.agda    | 26 ++++++++++++++++++++++
 test/Fail/LiftDisplayIntermediate.err     |  3 +++
 3 files changed, 50 insertions(+), 6 deletions(-)
 create mode 100644 test/Fail/LiftDisplayIntermediate.agda
 create mode 100644 test/Fail/LiftDisplayIntermediate.err

diff --git a/src/full/Agda/TypeChecking/DisplayForm.hs b/src/full/Agda/TypeChecking/DisplayForm.hs
index a6e68449408..011b5cfcd3c 100644
--- a/src/full/Agda/TypeChecking/DisplayForm.hs
+++ b/src/full/Agda/TypeChecking/DisplayForm.hs
@@ -114,13 +114,28 @@ matchDisplayForm d@(Display n ps v) es
   | length ps > length es = mzero
   | otherwise             = do
       let (es0, es1) = splitAt (length ps) es
-      mm <- match (Window 0 n) ps es0
+
+      -- The 'Display' constructor acts as though it binds the pattern
+      -- pattern variables up to 'n', so a match like
+      --
+      --   Display 1 [@1 @0] x =? [@0 _]
+      --
+      -- should work (it didn't; see LiftDisplayIntermediate). In
+      -- effect, this is because the LHS patterns are in some context
+      -- "Γ . @0", but the RHS term is only in context Γ.
+      --
+      -- Therefore, we should raise the RHS term by the number of
+      -- pattern variables, to bring it into the context of the
+      -- patterns.
+
+      mm <- match (Window 0 n) ps (raise n es0)
       us <- forM [0 .. n - 1] $ \ i -> do
-              -- #5294: Fail if we don't have bindings for all variables. This can
-              --        happen outside parameterised modules when some of the parameters
-              --        are not used in the lhs.
-              Just u <- return $ Map.lookup i mm
-              return u
+        -- #5294: Fail if we don't have bindings for all variables. This can
+        --        happen outside parameterised modules when some of the parameters
+        --        are not used in the lhs.
+        Just u <- return $ Map.lookup i mm
+        -- Note that the RHS terms are independent of the pattern variables.
+        return (applySubst (strengthenS __IMPOSSIBLE__ n) <$> u)
       return (d, substWithOrigin (parallelS $ map woThing us) us v `applyE` es1)
 
 type MatchResult = Map Int (WithOrigin Term)
diff --git a/test/Fail/LiftDisplayIntermediate.agda b/test/Fail/LiftDisplayIntermediate.agda
new file mode 100644
index 00000000000..2db1c39c079
--- /dev/null
+++ b/test/Fail/LiftDisplayIntermediate.agda
@@ -0,0 +1,26 @@
+module LiftDisplayIntermediate where
+
+open import Agda.Builtin.Equality
+open import Agda.Builtin.Nat
+open Agda.Primitive renaming (Set to Type)
+
+record Foo : Type where
+  field
+    f : Nat
+
+module _ (f : Nat → Foo) where
+  module _ n where
+    open Foo (f n) renaming (f to g) public
+    -- we get a display form [0] Foo.f (@1 @0) --> g @0
+
+  -- out here, we have [1] Foo.f (@1 @0) --> g @0, with the 'n' argument
+  -- of the inner module having become a pattern variable
+
+  _ : g zero ≡ zero
+  _ = refl
+
+  -- the nontrivial term above is Foo.f (@0 zero), and should display as g zero
+  -- previously, this would fail matching, since @1 (on the pattern) ≠ @0 (on the rhs).
+  -- however, note that the lhs of the display form has one more variable than the scope we're trying to use it in!
+  -- so really we should match [@1 @0] = [@1 zero], lifting the rhs by 1, which does succeed with @0 := zero
+  -- so the error printed should be g zero != zero of type Nat
diff --git a/test/Fail/LiftDisplayIntermediate.err b/test/Fail/LiftDisplayIntermediate.err
new file mode 100644
index 00000000000..f58bcf81250
--- /dev/null
+++ b/test/Fail/LiftDisplayIntermediate.err
@@ -0,0 +1,3 @@
+LiftDisplayIntermediate.agda:20,7-11
+g zero != zero of type Nat
+when checking that the expression refl has type g zero ≡ zero

From 7d4bac7a524d4d5fce86f49dbdd311f4bae5e0cd Mon Sep 17 00:00:00 2001
From: Ulf Norell <ulf.norell@gmail.com>
Date: Wed, 11 Sep 2024 10:15:13 +0200
Subject: [PATCH 25/30] add isExtendedLambda function

---
 src/full/Agda/TypeChecking/Monad/Base.hs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
index 3ccaf83ecc8..8efaeec3da9 100644
--- a/src/full/Agda/TypeChecking/Monad/Base.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -3092,6 +3092,12 @@ isEmptyFunction def =
     Function { funClauses = [] } -> True
     _ -> False
 
+isExtendedLambda :: Defn -> Bool
+isExtendedLambda def =
+  case def of
+    Function { funExtLam = Just{} } -> True
+    _ -> False
+
 isCopatternLHS :: [Clause] -> Bool
 isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats)
 

From 6fbf41208e95d762509bcaae9adb31cb24c11868 Mon Sep 17 00:00:00 2001
From: Ulf Norell <ulf.norell@gmail.com>
Date: Wed, 11 Sep 2024 10:17:37 +0200
Subject: [PATCH 26/30] Mimer: don't try to use extended lambdas (fixes #7484)

---
 src/full/Agda/Mimer/Mimer.hs    | 100 ++++++++++++++++----------------
 test/interaction/Issue7484.agda |  21 +++++++
 test/interaction/Issue7484.in   |   2 +
 test/interaction/Issue7484.out  |   8 +++
 4 files changed, 82 insertions(+), 49 deletions(-)
 create mode 100644 test/interaction/Issue7484.agda
 create mode 100644 test/interaction/Issue7484.in
 create mode 100644 test/interaction/Issue7484.out

diff --git a/src/full/Agda/Mimer/Mimer.hs b/src/full/Agda/Mimer/Mimer.hs
index 19e30394f0c..1f4a8e3590d 100644
--- a/src/full/Agda/Mimer/Mimer.hs
+++ b/src/full/Agda/Mimer/Mimer.hs
@@ -469,55 +469,58 @@ collectComponents opts costs ii mDefName whereNames metaId = do
       Nothing -> True
       Just defName -> defName /= qname && fmap ((defName `elem`)) (funMutual f) /= Just True
 
-    go comps qname = do
-      info <- getConstInfo qname
-      typ <- typeOfConst qname
-      scope <- getScope
-      let addLevel  = qnameToComponent (costLevel   costs) qname <&> \ comp -> comps{hintLevel     = comp : hintLevel  comps}
-          addAxiom  = qnameToComponent (costAxiom   costs) qname <&> \ comp -> comps{hintAxioms    = comp : hintAxioms comps}
-          addThisFn = qnameToComponent (costRecCall costs) qname <&> \ comp -> comps{hintThisFn    = Just comp{ compRec = True }}
-          addFn     = qnameToComponent (costFn      costs) qname <&> \ comp -> comps{hintFns       = comp : hintFns comps}
-          addData   = qnameToComponent (costSet     costs) qname <&> \ comp -> comps{hintDataTypes = comp : hintDataTypes comps}
-      case theDef info of
-        Axiom{} | isToLevel typ    -> addLevel
-                | shouldKeep scope -> addAxiom
-                | otherwise        -> return comps
-        -- TODO: Check if we want to use these
-        DataOrRecSig{}   -> return comps
-        GeneralizableVar -> return comps
-        AbstractDefn{}   -> return comps
-        -- If the function is in the same mutual block, do not include it.
-        f@Function{}
-          | Just qname == mDefName                  -> addThisFn
-          | isToLevel typ && isNotMutual qname f    -> addLevel
-          | isNotMutual qname f && shouldKeep scope -> addFn
-          | otherwise                               -> return comps
-        Datatype{} -> addData
-        Record{} -> do
-          projections <- mapM (qnameToComponent (costSpeculateProj costs)) =<< getRecordFields qname
-          comp <- qnameToComponent (costSet costs) qname
-          return comps{ hintRecordTypes = comp : hintRecordTypes comps
-                      , hintProjections = projections ++ hintProjections comps }
-        -- We look up constructors when we need them
-        Constructor{} -> return comps
-        -- TODO: special treatment for primitives?
-        Primitive{} | isToLevel typ    -> addLevel
-                    | shouldKeep scope -> addFn
-                    | otherwise        -> return comps
-        PrimitiveSort{} -> return comps
-      where
-        shouldKeep scope = or
-          [ qname `elem` explicitHints
-          , qname `elem` whereNames
-          , case hintMode of
-              Unqualified -> Scope.isNameInScopeUnqualified qname scope
-              AllModules  -> True
-              Module      -> Just (qnameModule qname) == mThisModule
-              NoHints     -> False
-          ]
+    go comps qname = go' comps qname =<< getConstInfo qname
+
+    go' comps qname info
+      | isExtendedLambda (theDef info) = return comps    -- We can't use pattern lambdas as components
+      | otherwise = do
+        typ <- typeOfConst qname
+        scope <- getScope
+        let addLevel  = qnameToComponent (costLevel   costs) qname <&> \ comp -> comps{hintLevel     = comp : hintLevel  comps}
+            addAxiom  = qnameToComponent (costAxiom   costs) qname <&> \ comp -> comps{hintAxioms    = comp : hintAxioms comps}
+            addThisFn = qnameToComponent (costRecCall costs) qname <&> \ comp -> comps{hintThisFn    = Just comp{ compRec = True }}
+            addFn     = qnameToComponent (costFn      costs) qname <&> \ comp -> comps{hintFns       = comp : hintFns comps}
+            addData   = qnameToComponent (costSet     costs) qname <&> \ comp -> comps{hintDataTypes = comp : hintDataTypes comps}
+        case theDef info of
+          Axiom{} | isToLevel typ    -> addLevel
+                  | shouldKeep scope -> addAxiom
+                  | otherwise        -> return comps
+          -- TODO: Check if we want to use these
+          DataOrRecSig{}   -> return comps
+          GeneralizableVar -> return comps
+          AbstractDefn{}   -> return comps
+          -- If the function is in the same mutual block, do not include it.
+          f@Function{}
+            | Just qname == mDefName                  -> addThisFn
+            | isToLevel typ && isNotMutual qname f    -> addLevel
+            | isNotMutual qname f && shouldKeep scope -> addFn
+            | otherwise                               -> return comps
+          Datatype{} -> addData
+          Record{} -> do
+            projections <- mapM (qnameToComponent (costSpeculateProj costs)) =<< getRecordFields qname
+            comp <- qnameToComponent (costSet costs) qname
+            return comps{ hintRecordTypes = comp : hintRecordTypes comps
+                        , hintProjections = projections ++ hintProjections comps }
+          -- We look up constructors when we need them
+          Constructor{} -> return comps
+          -- TODO: special treatment for primitives?
+          Primitive{} | isToLevel typ    -> addLevel
+                      | shouldKeep scope -> addFn
+                      | otherwise        -> return comps
+          PrimitiveSort{} -> return comps
+        where
+          shouldKeep scope = or
+            [ qname `elem` explicitHints
+            , qname `elem` whereNames
+            , case hintMode of
+                Unqualified -> Scope.isNameInScopeUnqualified qname scope
+                AllModules  -> True
+                Module      -> Just (qnameModule qname) == mThisModule
+                NoHints     -> False
+            ]
 
-        -- TODO: There is probably a better way of finding the module name
-        mThisModule = qnameModule <$> mDefName
+          -- TODO: There is probably a better way of finding the module name
+          mThisModule = qnameModule <$> mDefName
 
     -- NOTE: We do not reduce the type before checking, so some user definitions
     -- will not be included here.
@@ -614,7 +617,6 @@ collectLHSVars ii = do
     IPNoClause -> makeOpen []
     IPClause{ipcQName = fnName, ipcClauseNo = clauseNr} -> do
       info <- getConstInfo fnName
-      typ <- typeOfConst fnName
       parCount <- liftTCM getCurrentModuleFreeVars
       case theDef info of
         fnDef@Function{} -> do
diff --git a/test/interaction/Issue7484.agda b/test/interaction/Issue7484.agda
new file mode 100644
index 00000000000..971ac7feb3b
--- /dev/null
+++ b/test/interaction/Issue7484.agda
@@ -0,0 +1,21 @@
+open import Agda.Builtin.Equality
+
+postulate
+  A : Set
+  eq : (a b : A) → a ≡ b
+
+case_of_ : {A B : Set} → A → (A → B) → B
+case x of f = f x
+
+foo : (a b c d : A) → a ≡ d
+foo a b c d = bar
+  where
+  bar : a ≡ d
+  bar =
+    case eq a b of λ where
+      refl →
+        case eq b c of λ where
+          refl →
+            case eq c d of λ where
+              refl →
+                {!!}
diff --git a/test/interaction/Issue7484.in b/test/interaction/Issue7484.in
new file mode 100644
index 00000000000..97e20f92665
--- /dev/null
+++ b/test/interaction/Issue7484.in
@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 (cmd_autoOne AsIs) ""
diff --git a/test/interaction/Issue7484.out b/test/interaction/Issue7484.out
new file mode 100644
index 00000000000..963842c6ff0
--- /dev/null
+++ b/test/interaction/Issue7484.out
@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : a ≡ a " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "refl")
+((last . 1) . (agda2-goals-action '()))

From 58d920a717ff5da7ccb692042f4dede6cf46fe1d Mon Sep 17 00:00:00 2001
From: Ulf Norell <ulf.norell@gmail.com>
Date: Wed, 11 Sep 2024 14:51:52 +0200
Subject: [PATCH 27/30] Mimer: also don't use with functions in solutions

---
 src/full/Agda/Mimer/Mimer.hs             | 1 +
 src/full/Agda/TypeChecking/Monad/Base.hs | 6 ++++++
 test/interaction/Issue7484.agda          | 9 +++++++++
 test/interaction/Issue7484.in            | 1 +
 test/interaction/Issue7484.out           | 6 ++++--
 5 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/full/Agda/Mimer/Mimer.hs b/src/full/Agda/Mimer/Mimer.hs
index 1f4a8e3590d..4bccdf68c47 100644
--- a/src/full/Agda/Mimer/Mimer.hs
+++ b/src/full/Agda/Mimer/Mimer.hs
@@ -473,6 +473,7 @@ collectComponents opts costs ii mDefName whereNames metaId = do
 
     go' comps qname info
       | isExtendedLambda (theDef info) = return comps    -- We can't use pattern lambdas as components
+      | isWithFunction   (theDef info) = return comps    -- or with functions
       | otherwise = do
         typ <- typeOfConst qname
         scope <- getScope
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
index 8efaeec3da9..038ffc80e49 100644
--- a/src/full/Agda/TypeChecking/Monad/Base.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -3098,6 +3098,12 @@ isExtendedLambda def =
     Function { funExtLam = Just{} } -> True
     _ -> False
 
+isWithFunction :: Defn -> Bool
+isWithFunction def =
+  case def of
+    Function { funWith = Just{} } -> True
+    _ -> False
+
 isCopatternLHS :: [Clause] -> Bool
 isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats)
 
diff --git a/test/interaction/Issue7484.agda b/test/interaction/Issue7484.agda
index 971ac7feb3b..9c14e1b5f3a 100644
--- a/test/interaction/Issue7484.agda
+++ b/test/interaction/Issue7484.agda
@@ -19,3 +19,12 @@ foo a b c d = bar
             case eq c d of λ where
               refl →
                 {!!}
+
+foo' : (a b c d : A) → a ≡ d
+foo' a b c d = bar
+  where
+  bar : a ≡ d
+  bar with eq a b
+  ... | refl with eq b c
+  ... | refl with eq c d
+  ... | refl = ?
diff --git a/test/interaction/Issue7484.in b/test/interaction/Issue7484.in
index 97e20f92665..7ff2f1ae5de 100644
--- a/test/interaction/Issue7484.in
+++ b/test/interaction/Issue7484.in
@@ -1,2 +1,3 @@
 top_command (cmd_load currentFile [])
 goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""
diff --git a/test/interaction/Issue7484.out b/test/interaction/Issue7484.out
index 963842c6ff0..198552cec64 100644
--- a/test/interaction/Issue7484.out
+++ b/test/interaction/Issue7484.out
@@ -2,7 +2,9 @@
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-status-action "")
-(agda2-info-action "*All Goals*" "?0 : a ≡ a " nil)
-((last . 1) . (agda2-goals-action '(0)))
+(agda2-info-action "*All Goals*" "?0 : a ≡ a ?1 : a ≡ a " nil)
+((last . 1) . (agda2-goals-action '(0 1)))
 (agda2-give-action 0 "refl")
+((last . 1) . (agda2-goals-action '(1)))
+(agda2-give-action 1 "refl")
 ((last . 1) . (agda2-goals-action '()))

From 2555b5de42aea018465b1c2aad8c73f5aaab989a Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Thu, 12 Sep 2024 19:12:57 +0200
Subject: [PATCH 28/30] Update Changelog for Agda 2.7.0.1 (two more bug fixes)

---
 CHANGELOG.md | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7d4abff3f53..e20d866cb23 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,12 +30,16 @@ Bug fixes
 * Fixed an internal error related to interface files
   ([Issue #7436](https://github.com/agda/agda/issues/7436)).
 
-* Fixed an internal error in Mimer
-  ([Issue #7402](https://github.com/agda/agda/issues/7402)).
+* Fixed two internal errors in Mimer:
+  ([Issue #7402](https://github.com/agda/agda/issues/7402) and
+  [Issue #7484](https://github.com/agda/agda/issues/7484)).
 
 * Fixed a regression causing needless re-checking of files
   ([Issue #7199](https://github.com/agda/agda/issues/7199)).
 
+* Improved printing of terms by fixing a display form bug
+  ([PR #7480](https://github.com/agda/agda/issues/7480)).
+
 List of closed issues
 ---------------------
 
@@ -50,6 +54,7 @@ For 2.7.0.1, the following issues were
 - [Issue #7443](https://github.com/agda/agda/issues/7443): `--exact-split` is not default in 2.7.0, contrary to claims
 - [Issue #7452](https://github.com/agda/agda/issues/7452): Performance regression caused by making `--save-metas` the default
 - [Issue #7455](https://github.com/agda/agda/issues/7455): Both stack and cabal fail to install Agda
+- [Issue #7484](https://github.com/agda/agda/issues/7484): Internal error using Mimer in where block
 
 These pull requests were merged for 2.7.0.1:
 
@@ -63,3 +68,5 @@ These pull requests were merged for 2.7.0.1:
 - [PR #7471](https://github.com/agda/agda/issues/7471): setup: Don't assume exe is built on --lib
 - [PR #7475](https://github.com/agda/agda/issues/7475): Hotfix for #7442
 - [PR #7476](https://github.com/agda/agda/issues/7476): Bump std-lib to latest (v2.1.1) and cubical to latest
+- [PR #7480](https://github.com/agda/agda/issues/7480): Match display forms in the right context
+- [PR #7487](https://github.com/agda/agda/issues/7487): Mimer shouldn't try to use existing pattern lambdas in solutions

From bf0b355f5e7ec4c902edd1ff87b44d6ee9b6058f Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Sun, 14 Jul 2024 17:23:58 +0200
Subject: [PATCH 29/30] [release 2.7.0] replace -Werror by -Wwarn

---
 Agda.cabal | 104 ++++++++++++++++++++++++++---------------------------
 1 file changed, 52 insertions(+), 52 deletions(-)

diff --git a/Agda.cabal b/Agda.cabal
index 409f44cf2cd..f49f1cfd1ac 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -219,46 +219,46 @@ common language
 
   ghc-options:
       -- ASR (2022-05-31). Workaround to Issue #5932.
-      -Werror
-      -Werror=cpp-undef
-      -Werror=deprecated-flags
-      -Werror=deriving-typeable
-      -Werror=dodgy-exports
-      -Werror=dodgy-foreign-imports
-      -Werror=dodgy-imports
-      -Werror=duplicate-exports
-      -Werror=empty-enumerations
-      -Werror=identities
-      -Werror=inaccessible-code
-      -Werror=inline-rule-shadowing
-      -Werror=missing-fields
-      -Werror=missing-home-modules
-      -Werror=missing-methods
-      -Werror=missing-pattern-synonym-signatures
-      -Werror=missing-signatures
-      -Werror=noncanonical-monad-instances
-      -Werror=noncanonical-monoid-instances
-      -Werror=overflowed-literals
-      -Werror=overlapping-patterns
---      -Werror=redundant-constraints
-      -Werror=simplifiable-class-constraints
-      -Werror=star-binder
-      -Werror=star-is-type
-      -Werror=tabs
-      -Werror=typed-holes
-      -Werror=unbanged-strict-patterns
-      -Werror=unrecognised-pragmas
-      -Werror=unrecognised-warning-flags
-      -Werror=unticked-promoted-constructors
-      -Werror=unused-do-bind
-      -Werror=unused-foralls
-      -Werror=warnings-deprecations
-      -Werror=wrong-do-bind
+      -Wwarn
+      -Wwarn=cpp-undef
+      -Wwarn=deprecated-flags
+      -Wwarn=deriving-typeable
+      -Wwarn=dodgy-exports
+      -Wwarn=dodgy-foreign-imports
+      -Wwarn=dodgy-imports
+      -Wwarn=duplicate-exports
+      -Wwarn=empty-enumerations
+      -Wwarn=identities
+      -Wwarn=inaccessible-code
+      -Wwarn=inline-rule-shadowing
+      -Wwarn=missing-fields
+      -Wwarn=missing-home-modules
+      -Wwarn=missing-methods
+      -Wwarn=missing-pattern-synonym-signatures
+      -Wwarn=missing-signatures
+      -Wwarn=noncanonical-monad-instances
+      -Wwarn=noncanonical-monoid-instances
+      -Wwarn=overflowed-literals
+      -Wwarn=overlapping-patterns
+--      -Wwarn=redundant-constraints
+      -Wwarn=simplifiable-class-constraints
+      -Wwarn=star-binder
+      -Wwarn=star-is-type
+      -Wwarn=tabs
+      -Wwarn=typed-holes
+      -Wwarn=unbanged-strict-patterns
+      -Wwarn=unrecognised-pragmas
+      -Wwarn=unrecognised-warning-flags
+      -Wwarn=unticked-promoted-constructors
+      -Wwarn=unused-do-bind
+      -Wwarn=unused-foralls
+      -Wwarn=warnings-deprecations
+      -Wwarn=wrong-do-bind
 
   -- The following warning is an error in GHC >= 8.10.
   if impl(ghc < 8.10)
     ghc-options:
-      -Werror=implicit-kind-vars
+      -Wwarn=implicit-kind-vars
       -- #6623: Turn off this (nameless) warning:
       -- "Pattern match checker exceeded (2000000) iterations in a case alternative."
       -- See: https://gitlab.haskell.org/ghc/ghc/-/issues/13464
@@ -267,47 +267,47 @@ common language
 
   if impl(ghc < 9.10)
     ghc-options:
-      -Werror=semigroup
+      -Wwarn=semigroup
         -- The semigroup warning is deprecated in GHC 9.10
 
   if impl(ghc >= 8.8)
     ghc-options:
-      -Werror=missed-extra-shared-lib
+      -Wwarn=missed-extra-shared-lib
 
   if impl(ghc >= 8.10)
     ghc-options:
-      -Werror=compat-unqualified-imports
-      -Werror=deriving-defaults
-      -Werror=redundant-record-wildcards
-      -Werror=unused-packages
-      -Werror=unused-record-wildcards
+      -Wwarn=compat-unqualified-imports
+      -Wwarn=deriving-defaults
+      -Wwarn=redundant-record-wildcards
+      -Wwarn=unused-packages
+      -Wwarn=unused-record-wildcards
 
   if impl(ghc >= 9.0)
     ghc-options:
-      -Werror=invalid-haddock
+      -Wwarn=invalid-haddock
       -- #6137: coverage checker works only sufficiently well from GHC 9.0
-      -Werror=incomplete-patterns
-      -Werror=incomplete-record-updates
-      -Werror=overlapping-patterns
+      -Wwarn=incomplete-patterns
+      -Wwarn=incomplete-record-updates
+      -Wwarn=overlapping-patterns
 
   -- ASR (2022-04-27). This warning was added in GHC 9.0.2, removed
   -- from 9.2.1 and added back in 9.2.2.
   if impl(ghc == 9.0.2 || >= 9.2.2)
     ghc-options:
-      -Werror=unicode-bidirectional-format-characters
+      -Wwarn=unicode-bidirectional-format-characters
 
   if impl(ghc >= 9.2)
     ghc-options:
-      -Werror=operator-whitespace
-      -Werror=redundant-bang-patterns
+      -Wwarn=operator-whitespace
+      -Wwarn=redundant-bang-patterns
 
   if impl(ghc >= 9.4)
     ghc-options:
-      -Werror=type-equality-out-of-scope
+      -Wwarn=type-equality-out-of-scope
 
   if impl(ghc >= 9.4 && < 9.10)
     ghc-options:
-      -Werror=forall-identifier
+      -Wwarn=forall-identifier
         -- The forall-identifier warning is deprecated in GHC 9.10
 
   default-language: Haskell2010

From a6fc20c27ae953149b53a8997ba4a1c8b17d628a Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Sun, 14 Jul 2024 18:02:19 +0200
Subject: [PATCH 30/30] [release 2.7.0.1] remove testsuite but not deploy.yml

---
 .github/workflows/test.yml | 399 -------------------------------------
 Agda.cabal                 | 122 ------------
 stack-8.10.7.yaml          |   5 -
 stack-8.8.4.yaml           |   8 -
 stack-9.0.2.yaml           |   5 -
 stack-9.10.1.yaml          |   5 -
 stack-9.2.8.yaml           |   5 -
 stack-9.4.8.yaml           |   5 -
 stack-9.6.6.yaml           |   5 -
 stack-9.8.2.yaml           |   5 -
 10 files changed, 564 deletions(-)
 delete mode 100644 .github/workflows/test.yml

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
deleted file mode 100644
index c82be5e411c..00000000000
--- a/.github/workflows/test.yml
+++ /dev/null
@@ -1,399 +0,0 @@
-######################################################
-##                                                  ##
-##  !!!! Autogenerated YAML file, do not edit !!!!  ##
-##                                                  ##
-##  Edit source in /src/github/workflows/ instead!  ##
-##                                                  ##
-######################################################
-env:
-  AGDA_TESTS_OPTIONS: -j${PARALLEL_TESTS} --hide-successes
-  BUILD_DIR: dist
-  GHC_VER: 9.10.1
-  PARALLEL_TESTS: 2
-  STACK: stack --system-ghc
-  TASTY_ANSI_TRICKS: 'false'
-jobs:
-  build:
-    if: |
-      !contains(github.event.head_commit.message, '[skip ci]')
-      && !contains(github.event.head_commit.message, '[ci skip]')
-      && !contains(github.event.head_commit.message, '[github skip]')
-      && !contains(github.event.head_commit.message, '[skip github]')
-    runs-on: ubuntu-24.04
-    steps:
-    - name: Info about the context
-      run: |
-        echo "github.base_ref   = ${{ github.base_ref   }}"
-        echo "github.head_ref   = ${{ github.head_ref   }}"
-        echo "github.event_name = ${{ github.event_name }}"
-        echo "github.ref        = ${{ github.ref        }}"
-        echo "github.ref_name   = ${{ github.ref_name   }}"
-        echo "github.ref_type   = ${{ github.ref_type   }}"
-    - if: github.ref != 'refs/heads/master'
-      uses: styfle/cancel-workflow-action@0.12.1
-      with:
-        access_token: ${{ github.token }}
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - id: setup-haskell
-      uses: haskell-actions/setup@v2
-      with:
-        enable-stack: true
-        ghc-version: ${{ env.GHC_VER }}
-        stack-version: latest
-    - name: Copy stack-${{ env.GHC_VER}}.yaml to stack.yaml
-      run: cp stack-${{ env.GHC_VER }}.yaml stack.yaml
-    - name: Determine the ICU version
-      run: |
-        ICU_VER=$(pkg-config --modversion icu-i18n)
-        echo "ICU_VER=${ICU_VER}"
-        echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}"
-    - id: cache
-      name: Restore cache from approximate key
-      uses: actions/cache/restore@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-        restore-keys: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-
-    - name: Install dependencies for Agda and its test suites
-      run: make install-deps
-    - name: Build Agda
-      run: make BUILD_DIR="${BUILD_DIR}" install-bin
-    - name: Pack artifacts
-      run: |
-        strip "${BUILD_DIR}"/build/agda-tests/agda-tests \
-          "${BUILD_DIR}"/build/agda/agda \
-          "${BUILD_DIR}"/build/agda-mode/agda-mode
-
-        tar --use-compress-program zstd -cvf dist.tzst \
-          "${BUILD_DIR}"/build/agda-tests/agda-tests \
-          "${BUILD_DIR}"/build/agda/agda \
-          "${BUILD_DIR}"/build/agda-mode/agda-mode
-
-        tar --use-compress-program zstd -cvf stack-work.tzst .stack-work stack.yaml stack.yaml.lock
-    - name: Upload artifacts
-      uses: actions/upload-artifact@v4
-      with:
-        if-no-files-found: error
-        name: agda-${{ runner.os }}-${{ github.sha }}
-        path: |
-          dist.tzst
-          stack-work.tzst
-        retention-days: 1
-    - if: always() && steps.cache.outputs.cache-hit != 'true'
-      name: Save cache
-      uses: actions/cache/save@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-  cubical:
-    needs: build
-    runs-on: ubuntu-24.04
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - id: setup-haskell
-      uses: haskell-actions/setup@v2
-      with:
-        enable-stack: true
-        ghc-version: ${{ env.GHC_VER }}
-        stack-version: latest
-    - uses: actions/download-artifact@v4
-      with:
-        name: agda-${{ runner.os }}-${{ github.sha }}
-    - name: Unpack artifacts
-      run: |
-        tar --use-compress-program zstd -xvf dist.tzst
-        tar --use-compress-program zstd -xvf stack-work.tzst
-    - name: Determine the ICU version
-      run: |
-        ICU_VER=$(pkg-config --modversion icu-i18n)
-        echo "ICU_VER=${ICU_VER}"
-        echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}"
-    - id: cache
-      name: Restore cache from exact key
-      uses: actions/cache/restore@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-    - name: Cubical library test
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" cubical-test
-    - name: Successful tests using the cubical library
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" cubical-succeed
-  interaction-latex-html:
-    needs: build
-    runs-on: ubuntu-24.04
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - id: setup-haskell
-      uses: haskell-actions/setup@v2
-      with:
-        enable-stack: true
-        ghc-version: ${{ env.GHC_VER }}
-        stack-version: latest
-    - uses: actions/download-artifact@v4
-      with:
-        name: agda-${{ runner.os }}-${{ github.sha }}
-    - name: Unpack artifacts
-      run: |
-        tar --use-compress-program zstd -xvf dist.tzst
-        tar --use-compress-program zstd -xvf stack-work.tzst
-    - name: Determine the ICU version
-      run: |
-        ICU_VER=$(pkg-config --modversion icu-i18n)
-        echo "ICU_VER=${ICU_VER}"
-        echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}"
-    - id: cache
-      name: Restore cache from exact key
-      uses: actions/cache/restore@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-    - name: Install Tex Live and Emacs
-      run: |
-        sudo apt-get update
-        sudo apt-get install texlive-binaries ${APT_GET_OPTS}
-        sudo apt-get install emacs-nox ${APT_GET_OPTS}
-    - name: Suite of tests for the LaTeX and HTML backends
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" DONT_RUN_LATEX=Y latex-html-test
-    - if: always()
-      name: Testing the Emacs mode
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" testing-emacs-mode
-    - if: always()
-      name: User manual (test)
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" user-manual-test
-    - if: always()
-      name: User manual covers all options
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" user-manual-covers-options
-    - if: always()
-      name: User manual covers all warnings
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" user-manual-covers-warnings
-    - if: always()
-      name: Suite of interaction tests
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" interaction
-  size-solver-test:
-    needs: build
-    runs-on: ubuntu-24.04
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - id: setup-haskell
-      uses: haskell-actions/setup@v2
-      with:
-        enable-stack: true
-        ghc-version: ${{ env.GHC_VER }}
-        stack-version: latest
-    - uses: actions/download-artifact@v4
-      with:
-        name: agda-${{ runner.os }}-${{ github.sha }}
-    - name: Unpack artifacts
-      run: |
-        tar --use-compress-program zstd -xvf dist.tzst
-        tar --use-compress-program zstd -xvf stack-work.tzst
-    - name: Determine the ICU version
-      run: |
-        ICU_VER=$(pkg-config --modversion icu-i18n)
-        echo "ICU_VER=${ICU_VER}"
-        echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}"
-    - id: cache
-      name: Restore cache from exact key
-      uses: actions/cache/restore@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-    - name: Run tests for the size solver
-      run: |
-        export PATH=${HOME}/.local/bin:${PATH}
-        make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" size-solver-test
-  stdlib-test:
-    needs: build
-    runs-on: ubuntu-24.04
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - id: setup-haskell
-      uses: haskell-actions/setup@v2
-      with:
-        enable-stack: true
-        ghc-version: ${{ env.GHC_VER }}
-        stack-version: latest
-    - uses: actions/download-artifact@v4
-      with:
-        name: agda-${{ runner.os }}-${{ github.sha }}
-    - name: Unpack artifacts
-      run: |
-        tar --use-compress-program zstd -xvf dist.tzst
-        tar --use-compress-program zstd -xvf stack-work.tzst
-    - name: Determine the ICU version
-      run: |
-        ICU_VER=$(pkg-config --modversion icu-i18n)
-        echo "ICU_VER=${ICU_VER}"
-        echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}"
-    - id: cache
-      name: Restore cache from exact key
-      uses: actions/cache/restore@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-    - name: Standard library test
-      run: |
-        # ASR (2021-01-17). `cabal update` is required due to #5138.
-        # We should also use `stack` in this test.
-        cabal update
-        make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" std-lib-test
-    - if: always()
-      name: Benchmark
-      run: |
-        make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" benchmark-without-logs
-        make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" benchmark-summary
-    - name: Standard library compiler tests
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" std-lib-compiler-test
-    - name: Successful tests using the standard library
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" std-lib-succeed
-    - name: Interaction tests using the standard library
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" std-lib-interaction
-  test:
-    needs: build
-    runs-on: ubuntu-24.04
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - id: setup-haskell
-      uses: haskell-actions/setup@v2
-      with:
-        enable-stack: true
-        ghc-version: ${{ env.GHC_VER }}
-        stack-version: latest
-    - uses: actions/download-artifact@v4
-      with:
-        name: agda-${{ runner.os }}-${{ github.sha }}
-    - name: Unpack artifacts
-      run: |
-        tar --use-compress-program zstd -xvf dist.tzst
-        tar --use-compress-program zstd -xvf stack-work.tzst
-    - name: Determine the ICU version
-      run: |
-        ICU_VER=$(pkg-config --modversion icu-i18n)
-        echo "ICU_VER=${ICU_VER}"
-        echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}"
-    - id: cache
-      name: Restore cache from exact key
-      uses: actions/cache/restore@v4
-      with:
-        key: test.yml-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{
-          steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{
-          hashFiles('Agda.cabal','stack.yaml') }}
-        path: ${{ steps.setup-haskell.outputs.stack-root }}
-    - name: Suite of tests for bugs
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" bugs
-    - if: always()
-      name: 'Suite of successful tests: mini-library Common'
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" common
-    - if: always()
-      name: Suite of successful tests
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" succeed
-    - if: always()
-      name: Suite of failing tests
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" fail
-    - if: always()
-      name: Suite of examples
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" examples
-    - if: always()
-      name: Suite of interactive tests
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" interactive
-    - if: always()
-      name: Successful tests using Agda as a Haskell library
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" api-test
-    - if: always()
-      name: Internal test suite
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" internal-tests
-    - if: always()
-      name: Compiler tests
-      run: make BUILD_DIR="${GITHUB_WORKSPACE}/${BUILD_DIR}" compiler-test
-name: Build, Test, and Benchmark
-'on':
-  pull_request:
-    paths:
-    - '**'
-    - '!.github/**'
-    - .github/workflows/test.yml
-    - '!src/github/**'
-    - src/github/workflows/test.yml
-    - '!doc/**'
-    - doc/user-manual/**/*.lagda.rst
-    - '!src/agda-bisect/**'
-    - '!src/fix-whitespace/**'
-    - '!src/hs-tags/**'
-    - '!src/release-tools/**'
-    - '!.travis'
-    - '!macros/**'
-    - '!notes/**'
-    - '!.mailmap'
-    - '!.gitignore'
-    - '!.hlint.yaml'
-    - '!.readthedocs.yaml'
-    - '!.travis.yml'
-    - '!CHANGELOG.md'
-    - '!HACKING.md'
-    - '!LICENSE'
-    - '!README.md'
-    - '!fix-whitespace.yaml'
-    - '!hie*.yaml'
-    - '!stack-*.yaml'
-    - '!touchup.sh'
-    - '!CITATION.cff'
-  push:
-    branches:
-    - master
-    - ci-*
-    - release*
-    paths:
-    - '**'
-    - '!.github/**'
-    - .github/workflows/test.yml
-    - '!src/github/**'
-    - src/github/workflows/test.yml
-    - '!doc/**'
-    - doc/user-manual/**/*.lagda.rst
-    - '!src/agda-bisect/**'
-    - '!src/fix-whitespace/**'
-    - '!src/hs-tags/**'
-    - '!src/release-tools/**'
-    - '!.travis'
-    - '!macros/**'
-    - '!notes/**'
-    - '!.mailmap'
-    - '!.gitignore'
-    - '!.hlint.yaml'
-    - '!.readthedocs.yaml'
-    - '!.travis.yml'
-    - '!CHANGELOG.md'
-    - '!HACKING.md'
-    - '!LICENSE'
-    - '!README.md'
-    - '!fix-whitespace.yaml'
-    - '!hie*.yaml'
-    - '!stack-*.yaml'
-    - '!touchup.sh'
-    - '!CITATION.cff'
-  workflow_dispatch: null
diff --git a/Agda.cabal b/Agda.cabal
index f49f1cfd1ac..9a0863c886d 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -894,125 +894,3 @@ executable agda-mode
     , filepath  >= 1.4.2.1  && < 1.6
     , process   >= 1.6.3.0  && < 1.7
   default-language: Haskell2010
-
--- Cabal testsuite integration has some serious bugs, but we
--- can still make it work. See also:
--- https://github.com/haskell/cabal/issues/1938
--- https://github.com/haskell/cabal/issues/2214
--- https://github.com/haskell/cabal/issues/1953
---
--- This test suite should only be run using the Makefile.
--- The Makefile sets up the required environment,
--- executing the tests using cabal directly is almost
--- guaranteed to fail. See also Issue 1490.
---
-test-suite agda-tests
-  import:           language
-
-  type:             exitcode-stdio-1.0
-  hs-source-dirs:   test/
-  main-is:          Main.hs
-  other-modules:
-      Bugs.Tests
-      Compiler.Tests
-      CubicalSucceed.Tests
-      Fail.Tests
-      Interactive.Tests
-      Internal.Compiler.MAlonzo.Encode
-      Internal.Helpers
-      Internal.Interaction.Highlighting.Precise
-      Internal.Interaction.Highlighting.Range
-      Internal.Interaction.Library
-      Internal.Interaction.Options
-      Internal.Syntax.Abstract.Name
-      Internal.Syntax.Common
-      Internal.Syntax.Concrete.Name
-      Internal.Syntax.Internal
-      Internal.Syntax.Internal.Univ
-      Internal.Syntax.Position
-      Internal.Termination.CallGraph
-      Internal.Termination.CallMatrix
-      Internal.Termination.Order
-      Internal.Termination.Semiring
-      Internal.Termination.SparseMatrix
-      Internal.Termination.Termination
-      Internal.Tests
-      Internal.TypeChecking
-      Internal.TypeChecking.Free
-      Internal.TypeChecking.Free.Lazy
-      Internal.TypeChecking.Generators
-      Internal.TypeChecking.Irrelevance
-      Internal.TypeChecking.Monad.Base
-      Internal.TypeChecking.Positivity
-      Internal.TypeChecking.Positivity.Occurrence
-      Internal.TypeChecking.Rules.LHS.Problem
-      Internal.TypeChecking.SizedTypes
-      Internal.TypeChecking.SizedTypes.Syntax
-      Internal.TypeChecking.SizedTypes.WarshallSolver
-      Internal.TypeChecking.Substitute
-      Internal.Utils.AssocList
-      Internal.Utils.Bag
-      Internal.Utils.BiMap
-      Internal.Utils.Cluster
-      Internal.Utils.Either
-      Internal.Utils.Favorites
-      Internal.Utils.FileName
-      Internal.Utils.Graph.AdjacencyMap.Unidirectional
-      Internal.Utils.IntSet
-      Internal.Utils.List
-      Internal.Utils.List1
-      Internal.Utils.List2
-      Internal.Utils.ListT
-      Internal.Utils.Maybe.Strict
-      Internal.Utils.Monad
-      Internal.Utils.Monoid
-      Internal.Utils.PartialOrd
-      Internal.Utils.Permutation
-      Internal.Utils.RangeMap
-      Internal.Utils.SmallSet
-      Internal.Utils.Three
-      Internal.Utils.Trie
-      Internal.Utils.Warshall
-      LaTeXAndHTML.Tests
-      LibSucceed.Tests
-      Succeed.Tests
-      UserManual.Tests
-      Utils
-
-  -- Andreas, 2021-08-26, see https://github.com/haskell/cabal/issues/7577
-  -- Since 'agda-tests' wants to call 'agda', we have to add it here,
-  -- should we want to run 'cabal test'.
-  build-tool-depends: Agda:agda
-
-  build-depends:
-    , Agda
-    , array
-    , base
-    , bytestring
-    , containers
-    , directory
-    , filepath
-    , filemanip        >= 0.3.6.3 && < 0.4
-    , mtl
-    , process
-    , process-extras   >= 0.3.0   && < 0.3.4 || >= 0.4.1.3 && < 0.5 || >= 0.7.1 && < 0.8
-    , QuickCheck       >= 2.14.1  && < 2.16
-    , regex-tdfa
-    , split
-    , strict
-    , tasty            >= 1.1.0.4 && < 1.6
-    , tasty-hunit      >= 0.9.2   && < 0.11
-    , tasty-quickcheck >= 0.9.2   && < 0.12
-    -- tasty-silver 3.1.13 has option --ansi-tricks=false
-    -- NB: tasty-silver 3.2 requires tasty-1.4 at least
-    -- tasty-silver < 3.3 does not work interactively under Windows
-    , tasty-silver     >= 3.1.13  && < 3.4
-    , temporary        >= 1.2.0.3 && < 1.4
-    , text
-    , unix-compat      >= 0.4.3.1 && < 0.8
-    , unordered-containers
-    , uri-encode
-
-  -- Andreas (2021-10-11): tasty-silver < 3.3 does not work interactively under Windows
-  if os(windows)
-    build-depends: tasty-silver >= 3.3
diff --git a/stack-8.10.7.yaml b/stack-8.10.7.yaml
index bfb618fbafc..f63cfa6f41e 100644
--- a/stack-8.10.7.yaml
+++ b/stack-8.10.7.yaml
@@ -2,11 +2,6 @@ resolver: lts-18.28
 compiler: ghc-8.10.7
 compiler-check: match-exact
 
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'
-
 extra-deps:
 - pqueue-1.5.0.0
 - text-icu-0.8.0.2
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index 635034809ed..7f45572e949 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -2,17 +2,9 @@ resolver: lts-16.31
 compiler: ghc-8.8.4
 compiler-check: match-exact
 
-# Local packages specified by relative directory name.
-packages:
-  - '.'
-  - 'src/size-solver'
-
 extra-deps:
-- QuickCheck-2.14.2
 - pqueue-1.4.1.2
 - primitive-0.7.4.0
-- random-1.2.0
-- splitmix-0.1.0.3
 - strict-0.4.0.1
 - text-icu-0.8.0.2
 - vector-hashtables-0.1.1.1
diff --git a/stack-9.0.2.yaml b/stack-9.0.2.yaml
index e3fc54cc86c..9bd86c2d7b1 100644
--- a/stack-9.0.2.yaml
+++ b/stack-9.0.2.yaml
@@ -2,11 +2,6 @@ resolver: lts-19.33
 compiler: ghc-9.0.2
 compiler-check: match-exact
 
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'
-
 extra-deps:
 - pqueue-1.5.0.0
 - text-icu-0.8.0.2
diff --git a/stack-9.10.1.yaml b/stack-9.10.1.yaml
index a74b0a82685..a5f10754db3 100644
--- a/stack-9.10.1.yaml
+++ b/stack-9.10.1.yaml
@@ -2,11 +2,6 @@ resolver: nightly-2024-07-13
 compiler: ghc-9.10.1
 compiler-check: match-exact
 
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'
-
 # Libraries shipped with GHC 9.10.1:
 extra-deps:
 - Cabal-3.12.0.0
diff --git a/stack-9.2.8.yaml b/stack-9.2.8.yaml
index 22b9d3eec5a..c23db0894c9 100644
--- a/stack-9.2.8.yaml
+++ b/stack-9.2.8.yaml
@@ -2,10 +2,5 @@ resolver: lts-20.26
 compiler: ghc-9.2.8
 compiler-check: match-exact
 
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'
-
 extra-deps:
 - pqueue-1.5.0.0
diff --git a/stack-9.4.8.yaml b/stack-9.4.8.yaml
index b9f741d867e..ed57ebcdeb6 100644
--- a/stack-9.4.8.yaml
+++ b/stack-9.4.8.yaml
@@ -2,11 +2,6 @@ resolver: lts-21.25
 compiler: ghc-9.4.8
 compiler-check: match-exact
 
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'
-
 flags:
   mintty:
     win32-2-13-1: false
diff --git a/stack-9.6.6.yaml b/stack-9.6.6.yaml
index 82fc338b868..f125248c522 100644
--- a/stack-9.6.6.yaml
+++ b/stack-9.6.6.yaml
@@ -1,8 +1,3 @@
 resolver: lts-22.28
 compiler: ghc-9.6.6
 compiler-check: match-exact
-
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'
diff --git a/stack-9.8.2.yaml b/stack-9.8.2.yaml
index e23b4f5c655..59ca71df512 100644
--- a/stack-9.8.2.yaml
+++ b/stack-9.8.2.yaml
@@ -1,8 +1,3 @@
 resolver: nightly-2024-07-13
 compiler: ghc-9.8.2
 compiler-check: match-exact
-
-# Local packages specified by relative directory name.
-packages:
-- '.'
-- 'src/size-solver'