Skip to content

Commit 30ebdc5

Browse files
arnoudvanderleerarnoudvanderleer
authored
Merge branch 'master' into functor-currying
2 parents ff28278 + 3cdee34 commit 30ebdc5

File tree

101 files changed

+6854
-5269
lines changed

Some content is hidden

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

101 files changed

+6854
-5269
lines changed

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -431,3 +431,4 @@ CONTRIBUTORS.md
431431
MAINTAINERS.md
432432
/website/css/Agda-highlight.css
433433
/website/images/agda_dependency_graph.svg
434+
/website/images/agda_dependency_graph_legend.html

‎.pre-commit-config.yaml

Lines changed: 35 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,17 @@ repos:
9090
pass_filenames: false
9191
require_serial: true
9292

93+
# ! Experimental hook
94+
# - id: spaces-convention
95+
# name: Check Agda code block spaces convention
96+
# entry: scripts/spaces_convention.py
97+
# language: python
98+
# always_run: true
99+
# verbose: true
100+
# files: ^src\/.+\.lagda\.md$
101+
# types_or: [markdown, text]
102+
# require_serial: false
103+
93104
- repo: https://github.com/pre-commit/pre-commit-hooks
94105
rev: v3.2.0
95106
hooks:
@@ -110,14 +121,27 @@ repos:
110121
name: CSS, JS, YAML and Markdown (no codeblocks) formatting
111122
types_or: [css, javascript, yaml, markdown]
112123

113-
# Experimental hooks
114-
115-
# - id: spaces-convention
116-
# name: Check Agda code block spaces convention
117-
# entry: scripts/spaces_convention.py
118-
# language: python
119-
# always_run: true
120-
# verbose: true
121-
# files: ^src\/.+\.lagda\.md$
122-
# types_or: [markdown, text]
123-
# require_serial: false
124+
- repo: https://github.com/FlamingTempura/bibtex-tidy
125+
rev: v1.14.0
126+
hooks:
127+
- id: bibtex-tidy
128+
name: BibTeX formatting
129+
args:
130+
[
131+
'--modify',
132+
'--align=14',
133+
'--space=2',
134+
'--blank-lines',
135+
'--sort',
136+
'--trailing-commas',
137+
'--no-escape',
138+
'--numeric',
139+
'--months',
140+
'--numeric',
141+
'--duplicates=key,doi,abstract',
142+
'--sort-fields=title,shorttitle,author,year,month,day,date,journal,fjournal,shortjournal,booktitle,location,on,publisher,address,series,volume,number,pages,doi,isbn,issn,eprint,eprinttype,archiveprefix,eprintclass,primaryclass,url,urldate,copyright,category,note,metadata',
143+
'--encode-urls',
144+
'--tidy-comments',
145+
'--no-remove-empty-fields',
146+
'--remove-dupe-fields',
147+
]

‎.vscode/settings.json

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,8 @@
5252

5353
// File type specific
5454
"files.associations": {
55-
"*.lock": "json"
55+
"*.lock": "json",
56+
"*.bib": "bibtex"
5657
},
5758

5859
"[agda]": {
@@ -110,5 +111,12 @@
110111
"editor.formatOnSave": false,
111112
"editor.formatOnType": false,
112113
"editor.formatOnPaste": false
114+
},
115+
116+
"[bibtex]": {
117+
"editor.formatOnSave": false,
118+
"editor.formatOnType": false,
119+
"editor.formatOnPaste": false,
120+
"editor.defaultFormatter": null
113121
}
114122
}

‎ART.md

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,13 @@
22

33
<div align="center" style="margin: 2em 0;">
44
<figure>
5-
<img src="website/images/agda_dependency_graph.svg" alt="A dependency graph of the library, color coded by field. Fredrik Bakke. 2025 - perpetuity" width="95%" style="border-radius: 10px;">
6-
<figcaption>A dependency graph of the library, color coded by field. Fredrik Bakke. 2025 - perpetuity</figcaption>
5+
<img src="website/images/agda_dependency_graph.svg" alt="A dependency graph of the library, color coded by namespace. Fredrik Bakke. 2025 — perpetuity" width="95%" style="border-radius: 10px;">
6+
<br>
7+
<span>
8+
{{#include website/images/agda_dependency_graph_legend.html}}
9+
</span>
10+
<figcaption>A dependency graph of the library, color coded by namespace. Fredrik Bakke. 2025 — perpetuity</figcaption>
11+
712
</figure>
813
</div>
914

‎CITING-SOURCES.md

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
# Citing sources
22

33
All of the references and sources of the agda-unimath library are managed in a
4-
[BibLaTeX](https://www.ctan.org/pkg/biblatex) file `references.bib`, and we have
5-
a custom set of macros to work with them.
4+
[BibLaTeX](https://www.ctan.org/pkg/biblatex) file
5+
[`references.bib`](https://github.com/UniMath/agda-unimath/blob/master/references.bib),
6+
and we have a custom set of macros to work with them.
67

78
The macros are as follows:
89

@@ -31,13 +32,12 @@ not available, please define them as empty fields. E.g. `publisher = {},`.
3132

3233
If you are unsure about how to structure your BibLaTeX entry, it may be useful
3334
to know that the references are checked by the `linkcheck` GitHub workflow, so
34-
when you post your pull request to agda-unimath you can refer to the CI for
35-
possible issues.
35+
when you post your pull request to the agda-unimath repository you can refer to
36+
the CI for possible issues.
3637

3738
**Note:** If the citation label of your reference is not being generated
38-
properly, we support a custom `citeas` field that can be used to overwrite it.
39-
For instance, _Homotopy Type Theory: Univalent Foundations of Mathematics_
40-
should be cited as {{#cite UF13}}, and to make it so we have set
41-
`citeas = {UF13}` for its BibLaTeX entry. Keep in mind that if the citation
42-
label is not being generated properly, then it is likely that the author list is
43-
not being parsed properly either.
39+
properly, we support a custom `citeas` field that overwrites it. For instance,
40+
_Homotopy Type Theory: Univalent Foundations of Mathematics_ should be cited as
41+
{{#cite UF13}}, and to make it so we have set `citeas = {UF13}` for its BibLaTeX
42+
entry. Keep in mind that if the citation label is not being generated properly,
43+
then it is likely that the author list is not being parsed properly either.

‎CONTRIBUTING.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,10 @@ pre-commit tool and just not stage that file.
100100
formatting for these file types, so you should not worry about formatting such
101101
files.
102102

103+
- **BibTeX formatting:** Formats the
104+
[`references.bib`](https://github.com/UniMath/agda-unimath/blob/master/references.bib)
105+
file using [`bibtex-tidy`](https://github.com/FlamingTempura/bibtex-tidy).
106+
103107
## The `make website` tool
104108

105109
After you complete the `make pre-commit` process, you can run `make website` to

‎CONTRIBUTORS.toml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -263,3 +263,8 @@ displayName = "Evan Cavallo"
263263
usernames = [ "Evan Cavallo" ]
264264
github = "ecavallo"
265265
homepage = "https://ecavallo.net/"
266+
267+
[[contributors]]
268+
displayName = "Arnoud van der Leer"
269+
usernames = [ "Arnoud van der Leer" ]
270+
github = "arnoudvanderleer"

‎Makefile

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -145,12 +145,13 @@ CONTRIBUTORS.md: ${AGDAFILES} ${CONTRIBUTORS_FILE} ./scripts/generate_contributo
145145
website/css/Agda-highlight.css: ./scripts/generate_agda_css.py ./theme/catppuccin.css
146146
@python3 ./scripts/generate_agda_css.py
147147

148-
website/images/agda_dependency_graph.svg: ${AGDAFILES}
148+
website/images/agda_dependency_graph.svg website/images/agda_dependency_graph_legend.html &: ${AGDAFILES}
149149
@python3 ./scripts/generate_dependency_graph_rendering.py website/images/agda_dependency_graph svg || true
150150

151151
.PHONY: website-prepare
152152
website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md \
153-
./website/css/Agda-highlight.css ./website/images/agda_dependency_graph.svg
153+
./website/css/Agda-highlight.css ./website/images/agda_dependency_graph.svg \
154+
./website/images/agda_dependency_graph_legend.html
154155
@cp $(METAFILES) ./docs/
155156
@mkdir -p ./docs/website
156157
@cp -r ./website/images ./docs/website/

0 commit comments

Comments
 (0)