diff --git a/Agda.cabal b/Agda.cabal index 3e5b0a2c33d..607fe12b666 100644 --- a/Agda.cabal +++ b/Agda.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: Agda -version: 2.6.5 +version: 2.7.0 build-type: Custom license: MIT license-file: LICENSE @@ -158,7 +158,7 @@ source-repository head source-repository this type: git location: https://github.com/agda/agda.git - tag: v2.6.5 + tag: v2.7.0 -- Build flags --------------------------------------------------------------------------- diff --git a/CITATION.cff b/CITATION.cff index 6843f8d7c5d..886b296f438 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.6.5 -license-url: "https://agda.readthedocs.io/en/v2.6.5/team.html" +version: 2.7.0 +license-url: "https://agda.readthedocs.io/en/v2.7.0/team.html" url: "https://agda.readthedocs.io/" diff --git a/doc/user-manual/conf.py b/doc/user-manual/conf.py index 4eb65c9bc0e..8f7c2fb3124 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.6.5' +version = '2.7.0' # The full version, including alpha/beta/rc tags release = version diff --git a/mk/versions.mk b/mk/versions.mk index 7255e8c89fa..c73f4dfa7f6 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.6.5 +VERSION=2.7.0 diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el index 35eb8741f31..63623a6a2b3 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.6.5" +(define-package "agda2-mode" "2.7.0" "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 e4dd4744639..4ee76e8f4cf 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.6.5" +(defvar agda2-version "2.7.0" "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 a4e224195bd..a5775e220c0 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.6.5 Formatting LaTeX generated by Agda] + [2021/07/14 version 2.7.0 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 4b12c6660aa..7d3b582f539 100644 --- a/src/size-solver/size-solver.cabal +++ b/src/size-solver/size-solver.cabal @@ -30,7 +30,7 @@ executable size-solver hs-source-dirs: . main-is: Main.hs build-depends: - Agda == 2.6.5 + Agda == 2.7.0 , 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 30f574fb166..515aff2f81f 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.6.5/language/with-abstraction.html#ill-typed-with-abstractions) +(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions) diff --git a/test/Fail/Issue206.err b/test/Fail/Issue206.err index 5252b7e2e1a..2cae9dbefce 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.6.5/language/with-abstraction.html#ill-typed-with-abstractions) +(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions) diff --git a/test/Fail/Issue2763.err b/test/Fail/Issue2763.err index 731f4112ca3..c7434261c94 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.6.5/language/with-abstraction.html#ill-typed-with-abstractions) +(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions) diff --git a/test/Fail/Issue2771.err b/test/Fail/Issue2771.err index 8981a0e0e44..0a9b242da5d 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.6.5/language/with-abstraction.html#ill-typed-with-abstractions) +(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions) diff --git a/test/Fail/Issue530.err b/test/Fail/Issue530.err index 09ebaf148e0..e4acaf7fb13 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.6.5/language/with-abstraction.html#ill-typed-with-abstractions) +(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions) diff --git a/test/Fail/MagicWith.err b/test/Fail/MagicWith.err index 900ac4c8175..a10b3d1a883 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.6.5/language/with-abstraction.html#ill-typed-with-abstractions) +(https://agda.readthedocs.io/en/v2.7.0/language/with-abstraction.html#ill-typed-with-abstractions) diff --git a/test/interaction/Debug.out b/test/interaction/Debug.out index bd7f568692d..ef078245f78 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.6.5/agda/Debug.agdai. ") +(agda2-verbose "Writing interface file _build/2.7.0/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 9394fe4ccd8..e3e0afb530a 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.6.5" nil) +(agda2-info-action "*Agda Version*" "Agda version 2.7.0" nil) diff --git a/test/interaction/Issue1244b.out b/test/interaction/Issue1244b.out index d0f9f43045b..4243a104289 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.6.5" nil) +(agda2-info-action "*Agda Version*" "Agda version 2.7.0" nil) diff --git a/test/interaction/Issue6261.out b/test/interaction/Issue6261.out index 45b8b3463b2..046fdd61c82 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.6.5/agda/Issue6261.agdai). " t) -(agda2-info-action "*Type-checking*" " Loading Issue6261b (_build/2.6.5/agda/Issue6261b.agdai). " t) -(agda2-info-action "*Type-checking*" " Loading Issue6261c (_build/2.6.5/agda/Issue6261c.agdai). " t) -(agda2-info-action "*Type-checking*" " Loading Issue6261a (_build/2.6.5/agda/Issue6261a.agdai). " t) +(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-status-action "Checked") (agda2-info-action "*All Done*" "" nil) ((last . 1) . (agda2-goals-action '()))