Citation instructions

[L-TChen]

GitHub has a built-in citation support. By placing the CITATION.cff file in the root of repostitory, GitHub will add a widget to the sidebar like this

The file format is here

It will be time-saving if it is clear how to cite Agda, so the remaing question is ... to agree on how Agda should be cited.

I draft one based on "Elaborating dependent (co)pattern matching: No pattern left behind" to kick off a discussion.

[L-TChen]

For the demonstration purpose, I pushed the above file to my fork: https://github.com/L-TChen/agda so that you can see how it works on GitHub.

[gallais]

Related discussions:

coq/coq#5766 (Suggests Zenodo as a DOI provider)
agda/agda-stdlib#1833 (Suggests a JOSS publication for the software itself)

[nad]

For your demo I get the following BibTeX file:

@software{Agda_development_team_Agda_2_6_2_2_20230105_documentation,
author = {Agda development team},
title = {{Agda 2.6.2.2.20230105 documentation}},
url = {https://agda.readthedocs.io/en/v2.6.2.2.20230105/},
version = {2.6.2.2.20230105}
}

Is the idea to cite the software or its documentation?

For the documentation I think it makes sense to cite the user manual. The title of the user manual (the PDF file) is currently "Agda User Manual, Release 2.6.4", and the author is "The Agda Team". However, I don't think we should recommend people to cite an unreleased user manual.

Something like the following BibTeX entry might be suitable for citing the Agda 2.6.2 documentation:

@Manual{Agda_manual:2_6_2,
  title =   {Agda User Manual, Release 2.6.2},
  author =  {{The Agda Team}},
  year =    {2021},
  url =     {https://agda.readthedocs.io/_/downloads/en/v2.6.2/pdf/},
  urldate = {2023-01-18}
}

[andreasabel]

I think we should utilize the GitHub Releases feature also for the regular Agda releases (not just nightly) and then one could cite the release rather than the documentation. Maybe we can get the help of Wen @wenkokke to get proper releases (with binaries) here.

[wenkokke]

If I can use setup-agda for this, I could probably set this up pretty easily.

[L-TChen]

Based on @andreasabel's suggestion, I update the CITATION.cff so that GitHub now produces

@software{The_Agda_Team_Agda,
author = {The Agda Team},
title = {{Agda}},
url = {https://agda.readthedocs.io/en/v2.6.3/index.html},
version = {2.6.3}
}

For every release, one only needs to update the version (by releash.sh?). We may also want to include the citation instruction in the documentation.

[andreasabel]

LGTM (modulo I don't know what cff is).

[L-TChen]

LGTM (modulo I don't know what cff is).

lol

Right, if the citation format is agreed, then I will update the documentation and related scripts later (within this PR).

[nad]

If we link to the documentation, then I think we should use the user manual's title, and not "Agda" (and @manual rather than @software). For some reason the PDF file and the collection of HTML files use different titles. I think this should be fixed.

I believe that BibTeX interprets {The Agda Team} as the first name The Agda and the last name Team. One can prevent this by using {{The Agda Team}}. I already used this format in the BibTeX entry that I gave above, which could be updated for Agda 2.6.3.

[L-TChen]

I think it is more reasonable to cite the software instead of the documentation, see here for reasons. As pointed by @gallais, it is possible to mint a DOI for software and archive source code in an open repository like Zenodo (supported by the EU and now used by many conferences including ICFP for artefact evaluation).

Using CITATION.cff is not necessary at all. It is just to make life easier. As pointed by @nad, the implementation of the renderer is incorrect: I put “The Agda Team” as the family name, but the generated value is {The Agda Team} that will be treated by BibTeX as “Team, The Agda”.

Having a consistent citation format should make forward citation search easier. I find it difficult to find where Agda was used. If there is a DOI, then it should help Google Scholar or other analytic tools to locate.

Although I still do not know the best practice to cite a software like Agda, I’d like to propose the following:

1. Mint a conceptual DOI referring to all versions of Agda by releasing the initial version to Zenodo and mint a specific DOI for every release.
2. Instruct people to use the conceptual DOI but use the field version to specify the version. The citation may look like

The Agda Team. Agda (Version 2.6.3) [Computer software]. https://doi.org/xxx.yyy/zenodo.zzz

One may also include a link to the documentation.

4. For convenience, provide a bibtex entry directly or via CITATION.cff if GitHub fixes the aboive issue.

There are tools to convert a .cff file to a bibtex entry or other format, so it should be possible to update the citation instruction everywhere automatically.

[nad]

I think it is more reasonable to cite the software instead of the documentation

That depends on what the purpose of the citation is. Sometimes one may want to refer to the software, but sometimes one may want to, say, cite a passage in the user manual.

[Trebor-Huang]

We can always just add citation instructions to readthedocs. For the repo I think the purpose is just to cite the software.

[andreasabel]

I would think we should merge this PR rather than close it. We can continue the bikeshedding even after this has been merged. Having this PR in one form or the other is better than having nothing.

[andreasabel]

This file needs to be added to the change-version script:

agda/src/release-tools/change-version.bash

Lines 11 to 12 in 2816d75

	files+='Agda.cabal '
	files+='doc/user-manual/conf.py '

And to the exclude list in src/github/workflows/test.yml .

[wenkokke]

I think it is more reasonable to cite the software instead of the documentation, see here for reasons. As pointed by @gallais, it is possible to mint a DOI for software and archive source code in an open repository like Zenodo (supported by the EU and now used by many conferences including ICFP for artefact evaluation).

Using CITATION.cff is not necessary at all. It is just to make life easier. As pointed by @nad, the implementation of the renderer is incorrect: I put “The Agda Team” as the family name, but the generated value is {The Agda Team} that will be treated by BibTeX as “Team, The Agda”.

Having a consistent citation format should make forward citation search easier. I find it difficult to find where Agda was used. If there is a DOI, then it should help Google Scholar or other analytic tools to locate.

Although I still do not know the best practice to cite a software like Agda, I’d like to propose the following:

1. Mint a conceptual DOI referring to all versions of Agda by releasing the initial version to Zenodo and mint a specific DOI for every release.

2. Instruct people to use the conceptual DOI but use the field version to specify the version. The citation may look like

The Agda Team. Agda (Version 2.6.3) [Computer software]. https://doi.org/xxx.yyy/zenodo.zzz

One may also include a link to the documentation.

4. For convenience, provide a bibtex entry directly or via CITATION.cff if GitHub fixes the aboive issue.

There are tools to convert a .cff file to a bibtex entry or other format, so it should be possible to update the citation instruction everywhere automatically.

Following the specification, the Agda team should be cited as an entity rather than a person, so:

authors:
- name: "The Agda Team"

[wenkokke]

Reading the specification, we should have the primary citation be for the software, but we could add a citation for the manual as a related work under the references key.

[L-TChen]

Following the specification, the Agda team should be cited as an entity rather than a person, so:

authors:
- name: "The Agda Team"

Thanks! It does give the required BibTex entry as follows.

@software{The_Agda_Team_Agda,
author = {{The Agda Team}},
title = {{Agda}},
url = {https://agda.readthedocs.io/},
version = {2.6.5}
}

[L-TChen]

This file needs to be added to the change-version script:

agda/src/release-tools/change-version.bash

Lines 11 to 12 in 2816d75

	files+='Agda.cabal '
	files+='doc/user-manual/conf.py '

And to the exclude list in src/github/workflows/test.yml .

@andreasabel Yes, done. [ I don’t know why the requested change has not been marked resolved by GitHub … ]

[andreasabel]

Please also update

agda/doc/user-manual/conf.py

Line 24 in d959b19

author = u'The Agda Team'