diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: Agda -version: 2.6.4.2 +version: 2.6.4.3 build-type: Custom license: MIT license-file: LICENSE @@ -48,6 +48,7 @@ CHANGELOG.md README.md doc/user-manual/agda.svg + doc/release-notes/2.6.4.2.md doc/release-notes/2.6.4.1.md doc/release-notes/2.6.4.md doc/release-notes/2.6.3.md @@ -157,7 +158,7 @@ source-repository this type: git location: https://github.com/agda/agda.git - tag: v2.6.4.2 + tag: v2.6.4.3 -- Build flags --------------------------------------------------------------------------- diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,47 +1,17 @@ -Release notes for Agda version 2.6.4.2 +Release notes for Agda version 2.6.4.3 ====================================== -This is a bug-fix release. It aims to be API-compatible with 2.6.4.1. -Agda 2.6.4.2 supports GHC versions 8.6.5 to 9.8.1. - -Highlights ----------- +This release fixes a regression in 2.6.4.3 and one in 2.6.4. +It aims to be API-compatible with 2.6.4.1 and 2.6.4.2. -- Fix an inconsistency in Cubical Agda related to catch-all clauses: [Issue #7033](https://github.com/agda/agda/issues/7033) -- Fix a regression in instance search introduced in 2.6.4.2: [Issue #7113](https://github.com/agda/agda/issues/7113) -- Fix a bug related to `opaque`: [Issue #6972](https://github.com/agda/agda/issues/6972) -- Fix some internal errors: - * [Issue #7029](https://github.com/agda/agda/issues/7029) - * [Issue #7034](https://github.com/agda/agda/issues/7034) - * [Issue #7044](https://github.com/agda/agda/issues/7044) -- Fix building with cabal flag `-f debug-serialisation`: [Issue #7081](https://github.com/agda/agda/issues/7081) +Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1. -List of closed issues ---------------------- +Closed issues +------------- -For 2.6.4.2, the following issues were -[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4.2+is%3Aclosed) +For 2.6.4.3, the following issues were +[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4.3+is%3Aclosed) (see [bug tracker](https://github.com/agda/agda/issues)): -- [Issue #6972](https://github.com/agda/agda/issues/6972): Unfolding fails when code is split up into multiple files -- [Issue #6999](https://github.com/agda/agda/issues/6999): Unification failure for function type with erased argument -- [Issue #7020](https://github.com/agda/agda/issues/7020): question: haskell backend extraction of `Data.Nat.DivMod.DivMod`? -- [Issue #7029](https://github.com/agda/agda/issues/7029): Internal error on confluence check when rewriting a defined symbol with a hole -- [Issue #7033](https://github.com/agda/agda/issues/7033): transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥ -- [Issue #7034](https://github.com/agda/agda/issues/7034): Internal error with --two-level due to blocking on solved meta -- [Issue #7044](https://github.com/agda/agda/issues/7044): Serializer crashes on blocked definitions when using --allow-unsolved-metas -- [Issue #7048](https://github.com/agda/agda/issues/7048): hcomp symbols in interface not hidden under --cubical-compatible -- [Issue #7059](https://github.com/agda/agda/issues/7059): Don't recompile if --keep-pattern-variables option changes -- [Issue #7070](https://github.com/agda/agda/issues/7070): Don't set a default maximum heapsize for Agda runs -- [Issue #7081](https://github.com/agda/agda/issues/7081): Missing `IsString` instance with debug flags enabled -- [Issue #7095](https://github.com/agda/agda/issues/7095): Agda build flags appear as "automatic", but they are all "manual" -- [Issue #7104](https://github.com/agda/agda/issues/7104): Warning "there are two interface files" should not be serialized -- [Issue #7105](https://github.com/agda/agda/issues/7105): Internal error in generate-helper (C-c C-h) -- [Issue #7113](https://github.com/agda/agda/issues/7113): Instance resolution runs too late, leads to `with`-abstraction failure - -These PRs not corresponding to issues were merged: - -- [PR #6988](https://github.com/agda/agda/issues/6988): Provide a `.agda-lib` for Agda builtins -- [PR #7065](https://github.com/agda/agda/issues/7065): Some documentation fixes -- [PR #7072](https://github.com/agda/agda/issues/7072): Add 'Inference in Agda' to the list of tutorials -- [PR #7091](https://github.com/agda/agda/issues/7091): Add course to “Courses using Agda” +- [Issue #7148](https://github.com/agda/agda/issues/7148): Regression in 2.6.4.2 concerning `with` +- [Issue #7150](https://github.com/agda/agda/issues/7150): Regression in 2.6.4 in `rewrite` with instances diff --git a/doc/release-notes/2.6.4.2.md b/doc/release-notes/2.6.4.2.md new file mode 100644 --- /dev/null +++ b/doc/release-notes/2.6.4.2.md @@ -0,0 +1,47 @@ +Release notes for Agda version 2.6.4.2 +====================================== + +This is a bug-fix release. It aims to be API-compatible with 2.6.4.1. +Agda 2.6.4.2 supports GHC versions 8.6.5 to 9.8.1. + +Highlights +---------- + +- Fix an inconsistency in Cubical Agda related to catch-all clauses: [Issue #7033](https://github.com/agda/agda/issues/7033) +- Fix a regression in instance search introduced in 2.6.4.2: [Issue #7113](https://github.com/agda/agda/issues/7113) +- Fix a bug related to `opaque`: [Issue #6972](https://github.com/agda/agda/issues/6972) +- Fix some internal errors: + * [Issue #7029](https://github.com/agda/agda/issues/7029) + * [Issue #7034](https://github.com/agda/agda/issues/7034) + * [Issue #7044](https://github.com/agda/agda/issues/7044) +- Fix building with cabal flag `-f debug-serialisation`: [Issue #7081](https://github.com/agda/agda/issues/7081) + +List of closed issues +--------------------- + +For 2.6.4.2, the following issues were +[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4.2+is%3Aclosed) +(see [bug tracker](https://github.com/agda/agda/issues)): + +- [Issue #6972](https://github.com/agda/agda/issues/6972): Unfolding fails when code is split up into multiple files +- [Issue #6999](https://github.com/agda/agda/issues/6999): Unification failure for function type with erased argument +- [Issue #7020](https://github.com/agda/agda/issues/7020): question: haskell backend extraction of `Data.Nat.DivMod.DivMod`? +- [Issue #7029](https://github.com/agda/agda/issues/7029): Internal error on confluence check when rewriting a defined symbol with a hole +- [Issue #7033](https://github.com/agda/agda/issues/7033): transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥ +- [Issue #7034](https://github.com/agda/agda/issues/7034): Internal error with --two-level due to blocking on solved meta +- [Issue #7044](https://github.com/agda/agda/issues/7044): Serializer crashes on blocked definitions when using --allow-unsolved-metas +- [Issue #7048](https://github.com/agda/agda/issues/7048): hcomp symbols in interface not hidden under --cubical-compatible +- [Issue #7059](https://github.com/agda/agda/issues/7059): Don't recompile if --keep-pattern-variables option changes +- [Issue #7070](https://github.com/agda/agda/issues/7070): Don't set a default maximum heapsize for Agda runs +- [Issue #7081](https://github.com/agda/agda/issues/7081): Missing `IsString` instance with debug flags enabled +- [Issue #7095](https://github.com/agda/agda/issues/7095): Agda build flags appear as "automatic", but they are all "manual" +- [Issue #7104](https://github.com/agda/agda/issues/7104): Warning "there are two interface files" should not be serialized +- [Issue #7105](https://github.com/agda/agda/issues/7105): Internal error in generate-helper (C-c C-h) +- [Issue #7113](https://github.com/agda/agda/issues/7113): Instance resolution runs too late, leads to `with`-abstraction failure + +These PRs not corresponding to issues were merged: + +- [PR #6988](https://github.com/agda/agda/issues/6988): Provide a `.agda-lib` for Agda builtins +- [PR #7065](https://github.com/agda/agda/issues/7065): Some documentation fixes +- [PR #7072](https://github.com/agda/agda/issues/7072): Add 'Inference in Agda' to the list of tutorials +- [PR #7091](https://github.com/agda/agda/issues/7091): Add course to “Courses using Agda” diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el --- 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.6.4.2" +(define-package "agda2-mode" "2.6.4.3" "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 --- 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.6.4.2" +(defvar agda2-version "2.6.4.3" "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 --- 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.6.4.2 Formatting LaTeX generated by Agda] + [2021/07/14 version 2.6.4.3 Formatting LaTeX generated by Agda] \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, calc, environ, xparse, xkeyval} diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs --- a/src/full/Agda/TypeChecking/Rules/Def.hs +++ b/src/full/Agda/TypeChecking/Rules/Def.hs @@ -979,6 +979,10 @@ (proof, eqt) <- inferExpr eq + -- Andreas, 2024-02-27, issue #7150 + -- trigger instance search to resolve instances in rewrite-expression + solveAwakeConstraints + -- Andreas, 2016-04-14, see also Issue #1796 -- Run the size constraint solver to improve with-abstraction -- in case the with-expression contains size metas. diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs --- a/src/full/Agda/TypeChecking/Rules/Term.hs +++ b/src/full/Agda/TypeChecking/Rules/Term.hs @@ -1555,10 +1555,14 @@ inferExprForWith :: Arg A.Expr -> TCM (Term, Type) inferExprForWith (Arg info e) = verboseBracket "tc.with.infer" 20 "inferExprForWith" $ applyRelevanceToContext (getRelevance info) $ do - reportSDoc "tc.with.infer" 20 $ "inferExprforWith " <+> prettyTCM e - reportSLn "tc.with.infer" 80 $ "inferExprforWith " ++ show (deepUnscope e) + reportSDoc "tc.with.infer" 20 $ "inferExprForWith " <+> prettyTCM e + reportSLn "tc.with.infer" 80 $ "inferExprForWith " ++ show (deepUnscope e) traceCall (InferExpr e) $ do - (v, t) <- inferExpr e + -- Andreas, 2024-02-26, issue #7148: + -- The 'instantiateFull' here performs necessary eta-contraction, + -- both for future with-abstraction, + -- and for testing whether v is a variable modulo eta. + (v, t) <- instantiateFull =<< inferExpr e v <- reduce v -- Andreas 2014-11-06, issue 1342. -- Check that we do not `with` on a module parameter! diff --git a/stack-9.6.4.yaml b/stack-9.6.4.yaml --- a/stack-9.6.4.yaml +++ b/stack-9.6.4.yaml @@ -1,3 +1,3 @@ -resolver: lts-22.9 +resolver: lts-22.12 compiler: ghc-9.6.4 compiler-check: match-exact diff --git a/stack-9.8.1.yaml b/stack-9.8.1.yaml --- a/stack-9.8.1.yaml +++ b/stack-9.8.1.yaml @@ -1,3 +1,3 @@ -resolver: nightly-2024-02-09 +resolver: nightly-2024-02-27 compiler: ghc-9.8.1 compiler-check: match-exact