Agda 2.8.0.1 → 2.8.0.2
raw patch · 12 files changed
+61/−23 lines, 12 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- Agda.cabal +22/−5
- CHANGELOG.md +7/−2
- LICENSE +1/−1
- doc/release-notes/2.8.0.1.md +6/−0
- src/data/emacs-mode/agda2-mode-pkg.el +1/−1
- src/data/emacs-mode/agda2-mode.el +4/−4
- src/data/latex/agda.sty +1/−1
- src/full/Agda/Main.hs +10/−6
- src/setup/Agda/VersionCommit.hs +6/−0
- stack-9.10.3.yaml +1/−1
- stack-9.12.4.yaml +1/−1
- stack-9.14.1.yaml +1/−1
Agda.cabal view
@@ -1,10 +1,10 @@ cabal-version: 2.4 name: Agda-version: 2.8.0.1+version: 2.8.0.2 build-type: Simple license: MIT license-file: LICENSE-copyright: (c) 2005-2025 The Agda Team.+copyright: (c) 2005-2026 The Agda Team. author: The Agda Team, see https://agda.readthedocs.io/en/latest/team.html maintainer: The Agda Team homepage: https://wiki.portal.chalmers.se/agda/@@ -45,6 +45,7 @@ CHANGELOG.md README.md doc/user-manual/agda.svg+ doc/release-notes/2.8.0.1.md doc/release-notes/2.8.0.md doc/release-notes/2.7.0.1.md doc/release-notes/2.7.0.md@@ -224,7 +225,7 @@ source-repository this type: git location: https://github.com/agda/agda.git- tag: v2.8.0.1+ tag: v2.8.0.2 -- Build flags ---------------------------------------------------------------------------@@ -275,6 +276,12 @@ instead of the installation location defined by Cabal. This should not be enabled in declarative build environments like Nix or Guix. +flag version-with-git-hash+ default: False+ manual: True+ description:+ Suffix version information with the Git commit hash when available.+ -- Common stanzas --------------------------------------------------------------------------- @@ -291,6 +298,10 @@ cpp-options: -DUSE_XDG_DATA_HOME + if flag(version-with-git-hash)+ cpp-options:+ -DVERSION_WITH_GIT_HASH+ if flag(dump-core) ghc-options: -dsuppress-coercions -ddump-simpl -dsuppress-idinfo@@ -481,6 +492,10 @@ build-depends: text-icu >= 0.7.1.0 && < 0.9 + if flag(version-with-git-hash)+ build-depends:+ gitrev >= 1.3.1 && < 2+ if os(windows) build-depends: Win32 >= 2.6.1.0 && < 2.15@@ -524,7 +539,6 @@ , generic-data >= 0.9.2.0 && < 1.2 -- generic-data-0.9.2.0 adds instance of Bounded for FiniteEnumeration , ghc-compact == 0.1.*- , gitrev >= 1.3.1 && < 2 , hashable >= 1.3.0.0 && < 1.6 , haskeline >= 0.7.5.0 && < 0.9 , monad-control >= 1.0.2.3 && < 1.1@@ -1017,6 +1031,9 @@ , directory >= 1.3.6.0 && < 1.4 , filelock >= 0.1.1.5 && < 0.2 , filepath >= 1.4.2.1 && < 1.6- , gitrev >= 1.3.1 && < 2 , process >= 1.6.9.0 && < 1.7 , template-haskell >= 2.15.0.0 && < 2.25++ if flag(version-with-git-hash)+ build-depends:+ gitrev >= 1.3.1 && < 2
CHANGELOG.md view
@@ -1,6 +1,11 @@-Release notes for Agda version 2.8.0.1+Release notes for Agda version 2.8.0.2 ====================================== -* Added support for GHC 9.14.1+This version fixes two issues with the released binaries.+No non-installation related issues were fixed over 2.8.0 or 2.8.0.1.+So if you have installed 2.8.0 or 2.8.0.1 already there is no need to upgrade to 2.8.0.2.++* Fix problem with missing `zlib1.dll` in released Windows binary ([issue #8733](https://github.com/agda/agda/issues/8733))+* Remove commit hash from version number in released binaries ([issue #8716](https://github.com/agda/agda/issues/8716)) * Agda supports GHC versions 8.8.4 to 9.14.1.
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2005-2025 remains with the authors.+Copyright (c) 2005-2026 remains with the authors. Agda 2 was originally written by Ulf Norell, partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama, and from Agdalight by Ulf Norell and Andreas Abel.
+ doc/release-notes/2.8.0.1.md view
@@ -0,0 +1,6 @@+Release notes for Agda version 2.8.0.1+======================================++* Added support for GHC 9.14.1++* Agda supports GHC versions 8.8.4 to 9.14.1.
src/data/emacs-mode/agda2-mode-pkg.el view
@@ -1,3 +1,3 @@-(define-package "agda2-mode" "2.8.0.1"+(define-package "agda2-mode" "2.8.0.2" "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
@@ -29,7 +29,7 @@ ;;; Code: -(defvar agda2-version "2.8.0.1"+(defvar agda2-version "2.8.0.2" "The version of the Agda mode. Note that the same version of the Agda executable must be used.") @@ -2002,7 +2002,7 @@ If the version cannot be parsed, the answer is no. So e.g. agda-fast would be interpreted as not older than-agda-2.8.0.1"+agda-2.8.0.2" ;; If the given string does not have a numeric prefix, we answer no. (and (string-match "^[0-9][0-9.]*" version) (version< (match-string 0 version) "2.8")))@@ -2026,7 +2026,7 @@ If VERSION is empty or \"agda\", then agda is used. A prefix \"agda-\" is stripped from VERSION, so one can invoke this function e.g. with-\"agda-2.8.0.1\" instead of \"2.8.0.1\".+\"agda-2.8.0.2\" instead of \"2.8.0.2\". An attempt is made to preserve the default value of `agda2-mode-hook'." (interactive@@ -2047,7 +2047,7 @@ ;; * Replace version "agda" by just "". ;; ;; Rationale:- ;; The user might by accident enter "agda-2.8.0.1" instead of "2.8.0.1",+ ;; The user might by accident enter "agda-2.8.0.2" instead of "2.8.0.2", ;; or "agda" instead of "". (version (cond
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.8.0.1 Formatting LaTeX generated by Agda]+ [2021/07/14 version 2.8.0.2 Formatting LaTeX generated by Agda] \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, calc, environ, xparse, xkeyval}
src/full/Agda/Main.hs view
@@ -344,12 +344,7 @@ bullet = (" - " ++) -- Print cabal flags that were involved in compilation. flags =-#ifdef COUNT_CLUSTERS- "enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library" :-#endif-#ifdef OPTIMISE_HEAVILY- "optimise-heavily: extra optimisations" :-#endif+ -- Keep in alphabetical order! #ifdef DEBUG "debug: enable debug printing ('-v' verbosity flags)" : #endif@@ -359,6 +354,12 @@ #ifdef DEBUG_SERIALISATION "debug-serialisation: extra debug info during serialisation into '.agdai' files" : #endif+#ifdef COUNT_CLUSTERS+ "enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library" :+#endif+#ifdef OPTIMISE_HEAVILY+ "optimise-heavily: extra optimisations" :+#endif #ifdef USE_XDG_DATA_HOME concat [ "use-xdg-data-home: install and locate data files under $XDG_DATA_HOME/agda/"@@ -368,6 +369,9 @@ , " by default instead of the location defined by Cabal" ] :+#endif+#ifdef VERSION_WITH_GIT_HASH+ "version-with-git-hash: suffix version information with the Git commit hash" : #endif []
src/setup/Agda/VersionCommit.hs view
@@ -9,7 +9,9 @@ module Agda.VersionCommit where +#ifdef VERSION_WITH_GIT_HASH import Development.GitRev+#endif import Agda.Version @@ -19,6 +21,7 @@ -- | Information about current git commit, generated at compile time. commitInfo :: Maybe String+#ifdef VERSION_WITH_GIT_HASH commitInfo | hash == "UNKNOWN" = Nothing | otherwise = Just $ abbrev hash ++ dirty@@ -31,3 +34,6 @@ -- Abbreviate a commit hash while keeping it unambiguous abbrev = take 7+#else+commitInfo = Nothing+#endif
stack-9.10.3.yaml view
@@ -1,4 +1,4 @@-resolver: lts-24.55+resolver: lts-24.58 compiler: ghc-9.10.3 compiler-check: match-exact
stack-9.12.4.yaml view
@@ -1,4 +1,4 @@-resolver: nightly-2026-08-16+resolver: nightly-2026-09-12 compiler: ghc-9.12.4 compiler-check: match-exact
stack-9.14.1.yaml view
@@ -1,4 +1,4 @@-resolver: nightly-2026-08-16+resolver: nightly-2026-09-12 compiler: ghc-9.14.1 compiler-check: match-exact