Skip to content

Commit 381b996

Browse files
shhyoujamesmckinnaandreasabelMatthewDaggittgallais
authored
Fast-forward v2.0-release (branch) to v2.0 (tag) (#2856)
* Spellcheck CHANGELOG (#2167) * spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality` * Fixed Agda version typo in README (#2176) * Fixed in deprecation warning for `<-transˡ` (#2173) * Bump Haskell CI (original!) to latest minor GHC versions (#2187) * [fixes #2175] Documentation misc. typos etc. for RC1 (#2183) * missing comma! * corrected reference to `README.Design.Decidability` * typo: capitalisation * updated `installation-guide` * added word to `NonZero` section heading * Run workflows on any PR * Add merge-group trigger to workflows --------- Co-authored-by: MatthewDaggitt <[email protected]> * [fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185) * regularise and specify/systematise, the conventions for symbol usage * typos/revisions * Move `T?` to `Relation.Nullary.Decidable.Core` (#2189) * Move `T?` to `Relation.Nullary.Decidable.Core` * Var name fix * Some refactoring * Fix failing tests and address remaining comments * Fix style-guide * Make decidable versions of sublist functions the default (#2186) * Make decdable versions of sublist functions the default * Remove imports Bool.Properties * Address comments * [ fix #1743 ] move README to `doc/` directory (#2184) * [ admin ] dev playground * [ fix #1743 ] move README to doc/ directory * [ fix ] whitespace violations * [ ci ] update to cope with new doc/ directory * [ cleanup ] remove stale reference to travis.yml * [ admin ] update README-related instructions * [ admin ] fix build badges * [ fix ] `make test` build * Moved contents of notes/ to doc/ * Added CHANGELOG entry --------- Co-authored-by: MatthewDaggitt <[email protected]> * documentation: fix link to `installation-guide`, `README.agda`, `README.md`... (#2197) * fix link to `installation-guide` * catching another reference to `notes/` * note on instance brackets * `HACKING` guide * added Gurmeet Singh's changes * [ fix ] links in README.md --------- Co-authored-by: Guillaume Allais <[email protected]> * easy deprecation; leftover from `v1.6` perhaps? (#2203) * fix Connex comment (#2204) Connex allows both relations to hold, so the old comment was wrong. * Add `Function.Consequences.Setoid` (#2191) * Add Function.Consequences.Setoid * Fix comment * Fix re-export bug * Finally fixed bug I hope * Removed rogue comment * More tidying up * Deprecating `Relation.Binary.PropositionalEquality.isPropositional` (#2205) * deprecating `isPropositional` * tighten `import`s * bumped Agda version number in comment * definition of `Irreducible` and `Rough`; refactoring of `Prime` and `Composite` cf. #2180 (#2181) * definition of `Irreducible`; refactoring of `Prime` and `Composite` * tidying up old cruft * knock-on consequences: `Coprimality` * considerable refactoring of `Primality` * knock-on consequences: `Coprimality` * refactoring: no appeal to `Data.Nat.Induction` * refactoring: renamed `SmoothAt` and its constructor; added pattern synonym; proved `Decidable Irreducible`; misc. tweaks * knock-on consequences: `Coprimality` * refactoring: removed `NonZero` analysis; misc. tweaks * knock-on consequences: `Coprimality`; tightened `import`s * knock-on consequences: `Coprimality`; tightened `import`s * refactoring: every number is `1-rough` * knock-on consequences: `Coprimality`; use of smart constructor * refactoring: every number is `0-rough`; streamlining; inverse to `prime`; documentation * attempt to optimise for a nearly-common case pseudo-constructor * fiddling now * refactoring: better use of `primality` API * `Rough` is bounded * removed unnecessary implicits * comment * refactoring: comprehensive shift over to `NonTrivial` instances * refactoring: oops! * tidying up: removed infixes * tidying up: restored `rough⇒≤` * further refinements; added `NonTrivial` proofs * tidying up * moving definitions to `Data.Nat.Base` * propagated changes; many more explicit s required? * `NonTrivial` is `Recomputable` * all instances of `NonTrivial` now irrelevant; weird to need `NonTrivial 2` explicitly * tidying up `Coprimality`, eg with `variable`s * `NonTrivial` is `Decidable` * systematise proofs of `Decidable` properties via the `UpTo` predicates * explicit quantifier now in `composite≢` * Nathan's simplification * interaction of `NonZero` and `NonTrivial` instances * divisor now a record field; final lemmas: closure under divisibility; plus partial `CHANGELOG` entries * '(non-)instances' become '(counter-)examples' * stylistics * removed `k` as a variable/parameter * renamed fields and smart constructors * moved smart constructors; made a local definition * tidying up * refactoring per review comments: equivalence of `UpTo` predicates; making more things `private` * tidying up: names congruent to ordering relation * removed variable `k`; removed old proof in favour of new one with `NonZero` instance * removed `recomputable` in favour of a private lemma * regularised use of instance brackets * made instances more explicit * made instances more explicit * blank line * made `nonTrivial⇒nonZero` take an explicit argument in lieu of being able to make it an `instance` * regularised use of instance brackets * regularised use of instance brackets * trimming * tidied up `Coprimality` entries * Make HasBoundedNonTrivialDivisor infix * Make NonTrivial into a record to fix instance resolution bug * Move HasNonTrivialDivisor to Divisibility.Core and hide UpTo lemmas * Rearrange file to follow standard ordering of lemmas in the rest of the library * Move UpTo predicates into decidability proofs * No-op refactoring to curb excessively long lines * Make a couple of names consistent with style-guide * new definition of `Prime` * renamed fundamental definition * one last reference in `CHANGELOG` * more better words; one fewer definition * tidied up `Definitions` section; rejigged order of proofs of properties to reflect definitional order * refactored proof of `prime⇒irreducible` * finishing touches * missing lemma from irrelevant instance list * regularised final proof to use `contradiction` * added fixity `infix 10` * added fixity `infix 10`; made `composite` a pattern synonym; knock-on improvements * comprehensive `CHNAGELOG` entry; whitespace fixes * Rename 1<2+ to sz<ss * Rename hasNonTrivialDivisor relation * Updated CHANGELOG --------- Co-authored-by: MatthewDaggitt <[email protected]> * [fixes #2168] Change names in `Algebra.Consequences.*` to reflect `style-guide` conventions (#2206) * fixes issue #2168 * added more names for deprecation, plus `hiding` them in `Propositional` * Add biased versions of Function structures (#2210) * Fixes #2166 by fixing names in `IsSemilattice` (#2211) * Fix names in IsSemilattice * Add reference to changes to Semilattice to CHANGELOG * remove final references to `Category.*` (#2214) * Fix #2195 by removing redundant zero from IsRing (#2209) * Fix #2195 by removing redundant zero from IsRing * Moved proofs eariler to IsSemiringWithoutOne * Updated CHANGELOG * Fix bug * Refactored Properties.Ring * Fix renaming * Fix #2216 by making divisibility definitions records (#2217) * Fix #2216 by making divisibility definitions records * remove spurious/ambiguous `import` --------- Co-authored-by: jamesmckinna <[email protected]> * Fix deprecated modules (#2224) * Fix deprecated modules * [ ci ] Also build deprecated modules * [ ci ] ignore user warnings in test * [ ci ] fix filtering logic Deprecation and safety are not the same thing --------- Co-authored-by: Guillaume Allais <[email protected]> * Final admin changes for v2.0 release (#2225) * Final admin changes for v2.0 release * Fix Agda versions --------- Co-authored-by: jamesmckinna <[email protected]> Co-authored-by: Andreas Abel <[email protected]> Co-authored-by: MatthewDaggitt <[email protected]> Co-authored-by: G. Allais <[email protected]> Co-authored-by: Jesin <[email protected]> Co-authored-by: jamesmckinna <[email protected]> Co-authored-by: Alex Rice <[email protected]>
1 parent a7d2302 commit 381b996

File tree

133 files changed

+2147
-1227
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

133 files changed

+2147
-1227
lines changed
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.

.github/workflows/ci-ubuntu.yml

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ on:
88
branches:
99
- master
1010
- experimental
11+
merge_group:
1112

1213
########################################################################
1314
## CONFIGURATION
@@ -50,7 +51,7 @@ env:
5051
CABAL_VERSION: 3.6.2.0
5152
CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
5253
# CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
53-
AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/
54+
AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -isrc -idoc
5455

5556
jobs:
5657
test-stdlib:
@@ -71,16 +72,15 @@ jobs:
7172

7273
- name: Initialise variables
7374
run: |
74-
if [[ '${{ github.ref }}' == 'refs/heads/master' \
75-
|| '${{ github.base_ref }}' == 'master' ]]; then
76-
# Pick Agda version for master
77-
echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV;
78-
echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
79-
elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
80-
|| '${{ github.base_ref }}' == 'experimental' ]]; then
75+
if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
76+
|| '${{ github.base_ref }}' == 'experimental' ]]; then
8177
# Pick Agda version for experimental
8278
echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV;
8379
echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV
80+
else
81+
# Pick Agda version for master
82+
echo "AGDA_COMMIT=tags/v2.6.4.1" >> $GITHUB_ENV;
83+
echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
8484
fi
8585
8686
if [[ '${{ github.ref }}' == 'refs/heads/master' \
@@ -151,10 +151,19 @@ jobs:
151151

152152
- name: Test stdlib
153153
run: |
154+
# Including deprecated modules purely for testing
155+
cabal run GenerateEverything -- --include-deprecated
156+
${{ env.AGDA }} -WnoUserWarning --safe EverythingSafe.agda
157+
${{ env.AGDA }} -WnoUserWarning Everything.agda
158+
159+
- name: Prepare HTML index
160+
run: |
161+
# Regenerating the Everything files without the deprecated modules
154162
cabal run GenerateEverything
155-
cp travis/* .
163+
cp .github/tooling/* .
156164
./index.sh
157165
${{ env.AGDA }} --safe EverythingSafe.agda
166+
${{ env.AGDA }} Everything.agda
158167
${{ env.AGDA }} index.agda
159168
160169
- name: Golden testing
@@ -177,8 +186,7 @@ jobs:
177186
rm -f '${{ env.AGDA_HTML_DIR }}'/*.html
178187
rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
179188
${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
180-
181-
cp travis/* .
189+
cp .github/tooling/* .
182190
./landing.sh
183191
184192
- name: Deploy HTML

.github/workflows/haskell-ci.yml

Lines changed: 11 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@
88
#
99
# For more information, see https://github.com/haskell-CI/haskell-ci
1010
#
11-
# version: 0.17.20230824
11+
# version: 0.17.20231010
1212
#
13-
# REGENDATA ("0.17.20230824",["github","--no-cabal-check","agda-stdlib-utils.cabal"])
13+
# REGENDATA ("0.17.20231010",["github","--no-cabal-check","agda-stdlib-utils.cabal"])
1414
#
1515
name: Haskell-CI
1616
on:
@@ -32,6 +32,7 @@ on:
3232
- agda-stdlib-utils.cabal
3333
- cabal.haskell-ci
3434
- "*.hs"
35+
merge_group:
3536
jobs:
3637
linux:
3738
name: Haskell-CI - Linux - ${{ matrix.compiler }}
@@ -44,19 +45,19 @@ jobs:
4445
strategy:
4546
matrix:
4647
include:
47-
- compiler: ghc-9.8.0.20230822
48+
- compiler: ghc-9.8.1
4849
compilerKind: ghc
49-
compilerVersion: 9.8.0.20230822
50+
compilerVersion: 9.8.1
5051
setup-method: ghcup
51-
allow-failure: true
52-
- compiler: ghc-9.6.2
52+
allow-failure: false
53+
- compiler: ghc-9.6.3
5354
compilerKind: ghc
54-
compilerVersion: 9.6.2
55+
compilerVersion: 9.6.3
5556
setup-method: ghcup
5657
allow-failure: false
57-
- compiler: ghc-9.4.6
58+
- compiler: ghc-9.4.7
5859
compilerKind: ghc
59-
compilerVersion: 9.4.6
60+
compilerVersion: 9.4.7
6061
setup-method: ghcup
6162
allow-failure: false
6263
- compiler: ghc-9.2.8
@@ -94,7 +95,6 @@ jobs:
9495
mkdir -p "$HOME/.ghcup/bin"
9596
curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup"
9697
chmod a+x "$HOME/.ghcup/bin/ghcup"
97-
"$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml;
9898
"$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false)
9999
"$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
100100
else
@@ -104,7 +104,6 @@ jobs:
104104
mkdir -p "$HOME/.ghcup/bin"
105105
curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup"
106106
chmod a+x "$HOME/.ghcup/bin/ghcup"
107-
"$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml;
108107
"$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
109108
fi
110109
env:
@@ -138,7 +137,7 @@ jobs:
138137
echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
139138
echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"
140139
echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV"
141-
if [ $((HCNUMVER >= 90800)) -ne 0 ] ; then echo "HEADHACKAGE=true" >> "$GITHUB_ENV" ; else echo "HEADHACKAGE=false" >> "$GITHUB_ENV" ; fi
140+
echo "HEADHACKAGE=false" >> "$GITHUB_ENV"
142141
echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV"
143142
echo "GHCJSARITH=0" >> "$GITHUB_ENV"
144143
env:
@@ -167,18 +166,6 @@ jobs:
167166
repository hackage.haskell.org
168167
url: http://hackage.haskell.org/
169168
EOF
170-
if $HEADHACKAGE; then
171-
cat >> $CABAL_CONFIG <<EOF
172-
repository head.hackage.ghc.haskell.org
173-
url: https://ghc.gitlab.haskell.org/head.hackage/
174-
secure: True
175-
root-keys: 7541f32a4ccca4f97aea3b22f5e593ba2c0267546016b992dfadcd2fe944e55d
176-
26021a13b401500c8eb2761ca95c61f2d625bfef951b939a8124ed12ecf07329
177-
f76d08be13e9a61a377a85e2fb63f4c5435d40f8feb3e12eb05905edb8cdea89
178-
key-threshold: 3
179-
active-repositories: hackage.haskell.org, head.hackage.ghc.haskell.org:override
180-
EOF
181-
fi
182169
cat >> $CABAL_CONFIG <<EOF
183170
program-default-options
184171
ghc-options: $GHCJOBS +RTS -M3G -RTS
@@ -230,9 +217,6 @@ jobs:
230217
echo " ghc-options: -Werror=missing-methods" >> cabal.project
231218
cat >> cabal.project <<EOF
232219
EOF
233-
if $HEADHACKAGE; then
234-
echo "allow-newer: $($HCPKG list --simple-output | sed -E 's/([a-zA-Z-]+)-[0-9.]+/*:\1,/g')" >> cabal.project
235-
fi
236220
$HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(agda-stdlib-utils)$/; }' >> cabal.project.local
237221
cat cabal.project
238222
cat cabal.project.local

0 commit comments

Comments
 (0)