packages feed

Agda 2.6.4.2 → 2.6.4.3

raw patch · 10 files changed

+76/−50 lines, 10 filesdep ~basedep ~containersdep ~filepathPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, containers, filepath, hashable, parallel, time

API changes (from Hackage documentation)

Files

Agda.cabal view
@@ -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 ---------------------------------------------------------------------------
CHANGELOG.md view
@@ -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
+ doc/release-notes/2.6.4.2.md view
@@ -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”
src/data/emacs-mode/agda2-mode-pkg.el view
@@ -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
src/data/emacs-mode/agda2-mode.el view
@@ -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.")
src/data/latex/agda.sty view
@@ -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}
src/full/Agda/TypeChecking/Rules/Def.hs view
@@ -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.
src/full/Agda/TypeChecking/Rules/Term.hs view
@@ -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!
stack-9.6.4.yaml view
@@ -1,3 +1,3 @@-resolver: lts-22.9+resolver: lts-22.12 compiler: ghc-9.6.4 compiler-check: match-exact
stack-9.8.1.yaml view
@@ -1,3 +1,3 @@-resolver: nightly-2024-02-09+resolver: nightly-2024-02-27 compiler: ghc-9.8.1 compiler-check: match-exact