Change version to 2.7.0

agda · May 12, 2024 · 561a453 · 561a453
1 parent 838b622
commit 561a453
Show file tree

Hide file tree

Showing 18 changed files with 23 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 '()))